Showing changes from revision #14 to #15:
Added | Removed | Changed
\tableofcontents
\section{The continuum-flat axiom}
We begin by defining the abstract continuum to be an arbitrary commutative ring with characteristic 0: there are terms and and functions , , and , such that is an abelian group, is a commutative monoid, and distributes over .
has characteristic 0 if the unique ring homomorphism is an embedding of types.
Axiom then states that for every crisp type , is discrete if and only if the function is an equivalence of types.
Cohesive homotopy type theory with axiom is called -cohesive homotopy type theory.
\subsection{The shape of a type}
\subsection{Contractibility of the shape of the continuum}
\subsection{Compact connectedness of the continuum}
\section{The circle}
Let us define the square function on as a function with a dependent function
One definition of the abstract circle is the (homotopy) coequalizer of the function and the identity function
An equivalent definition of the abstract circle is the dependent sum type
\section{See also}
high school mathematics in cohesive homotopy type theory?
\section{References}
Mike Shulman, Brouwerβs fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)
Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)
Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)