Homotopy Type Theory: Univalent Foundations of Mathematics

algebraic assume axiom of choice cartesian product category theory Cauchy approximation Cauchy reals Cauchy sequences Chapter characterization Cited classical codomain colimits composite computation rule construct constructors contractible Corollary defining equations dependent function element equivalence equivalence relation example excluded middle Exercise fiber fibf(b fibration function extensionality function f function type functor 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 lim(x 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 refl refla reflx sequence set theory structure suffices to show Suppose surjective Theorem topological transport type family univalence univalence axiom univalent foundations universal property