We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a type-theoretic proof assistant with decidable typechecking) made us use more theory or helped us to see theory more clearly.

翻译：我们讨论了在基于证明助手Coq的UniMath库中，关于语法与语义机械化工作的一些方面。我们聚焦于这样的经验：Coq（作为一种可判定类型检查的类型论证明助手）如何促使我们运用更多理论，或帮助我们更清晰地理解理论。