scientific article; zbMATH DE number 7756113

DOI10.4230/lipics.types.2019.8MaRDI QIDQ6079238

Unnamed Author

Publication date: 27 October 2023

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

monoidal categoriescoherencegroupoidshomotopy type theoryCoqformalisationhigher inductive types

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Homotopy type theory in Lean
• On MacLane's conditions for coherence of natural associativities, commutativities, etc
• Weak omega-categories from intensional type theory
• Types are weak ω -groupoids
• A Cubical Approach to Synthetic Homotopy Theory
• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics