Homotopy Type Theory: Univalent Foundations of Mathematics

algebraic apply assume axiom of choice cartesian product category theory Cauchy approximation Cauchy reals Cauchy sequences Chapter characterization classical codomain colimits composite computation rule construct contractible coproduct Corollary Dedekind reals defining equations denote dependent function element equivalence relation example excluded middle Exercise fiber fibration function extensionality function f function type functor give given groupoid hence higher inductive types homotopy groups homotopy theory homotopy type theory identity types implies induction principle inductive definition inductive hypothesis inhabited instance inverse isomorphism judgmental equality Lemma logic mathematics merely exists morphisms n-connected n-truncated n-type natural numbers notation notion pair path induction precategory Proof Prop propositional truncation prove pushout quasi-inverse quotient rat(q rat(r real numbers recursion recursion principle refla reflx sequence set theory Similarly structure suffices to show Suppose surjective Theorem topological type family uniqueness principle univalence univalence axiom univalent foundations universal property