Formalizing colimits in Cat

DOI10.4230/LIPICS.ITP.2025.20MaRDI QIDQ7323669zbMATH OpenFDO

Authors Mario Carneiro, Emily Riehl

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.20

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A stable \(\infty\)-category of Lagrangian cobordisms
• A universal characterization of higher algebraic K-theory
• Adjoint triangles
• An Interpolation Theorem for Adjoint Functors
• Category theory in context
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Elements of -category theory
• Experience implementing a performant category-theory library in Coq
• HOL Light: An Overview
• scientific article; zbMATH DE number 1375542 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 575948 (Why is no real title available?)
• scientific article; zbMATH DE number 626734 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Simplicial homotopy theory
• Towards a readable formalisation of category theory
• Univalent categories and the Rezk completion

This page was built for publication: Formalizing colimits in \(\mathcal{C}\)at

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323669)