Construction of the circle in \textit{UniMath}

DOI10.1016/j.jpaa.2021.106687OpenAlexW3144774570MaRDI QIDQ2031555

Ulrik Buchholtz, Marc Bezem, Daniel R. Grayson, Michael Shulman

Publication date: 9 June 2021

Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1910.01856

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Uses Software

• UniMath

Cites Work

• C-system of a module over a \(Jf\)-relative monad
• Higher Inductive Types as Homotopy-Initial Algebras
• Products of families of types and (Pi,lambda)-structures on C-systems
• C-systems defined by universe categories: presheaves
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• Subsystems and regular quotients of C-systems
• A C-system defined by a universe category
• Semantics of higher inductive types
• The law of excluded middle in the simplicial model of type theory
• Cellular Cohomology in Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• The univalence axiom for elegant Reedy presheaves

This page was built for publication: Construction of the circle in \textit{UniMath}