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（作为一种具有可判定类型检查的类型论证明助理）促使我们运用更多理论，或帮助我们更清晰地理解理论的经验。