Homotopy Type Theory

---

Homotopy Type Theory is a new branch of mathematics that combines aspects of several different fields in a very cool manner. It is based on the recently discovered connections between Homotopy Theory and Type Theory. Homotopy Theory is an outgrowth of Algebraic Topology, homological algebra with relation to higher Category Theory; while Type theory is a branch of mathematical logic and theoretical computer science.

HoTT suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of objects of mathematics - and convenient machine implementations, which can serve as a practical aid to the working mathematician. This is the Univalent Foundations program.

---

Notes

Martin Löf’s Type Theory

• Type Theory vs Set Theory
  • Type Theoretic Rosetta Stone
  • Specifying a Type
• Function Type
• Universes
• Dependent Function Type
• Product Type
• Dependent Pair Types
  • Semi Groups in Types Theory
  • Type Theoretic Axiom of Choice
• Sum Types
• Boolean Type
• Natural Numbers
  • Addition is Associative
  • Peano Axioms and Type Theory
• Identity Type
  • Path Induction
  • Based Path Induction

Homotopy Type Theory

• Identity is an Equivalence
  • Types are Higher Groupoids
• Loop Space
  • Pointed Type
  • Eckmann-Hilton
• Functions as Functors
  • Transport
• Homotopy
• Functions as Equivalences

Higher Groupoid Structure of Type Formers

• Higher Groupoid Structure of Cartesian Product
• Higher Groupoid Structure of Sigma Type
• Higher Groupoid Structure of Unit Type
• Higher Groupoid Structure of Pi Type
  • Transport over a function between families
• Univalence
• Higher Groupoid Structure of Identity Types
  • Transports in a Family of Paths
• Higher Groupoids Structure of Coproducts
• Higher Groupoid Structure of Natural Numbers
• Equivalence of more complicated structures - Semi-groups
  • Equality of Semigroups
• Products respect Universal Properties
• Sigma Types respect Universal Properties

Sets and Propositions

• Sets in Type Theory
• Double Negation Does Not Cancel
• Mere Propositions
  • Mere Propositions are Sets
  • Propositional Truncation
  • Law of Excluded Middle
• Sub-Types
• Propositional Resizing
• Some Type Formers respect Mere Propositions
• A better Axiom of Choice for Type Theory
• The Principle of Unique Choice
• Contractible Types
  • Some Contractible Types

Equivalences

• Quasi-inverse is not a Mere Proposition
  • Lemma 1 for Quasi-inverse is not a Mere Proposition
  • Lemma 2 for Quasi-inverse is not a Mere Proposition
• Half Adjoint Equivalences
  • Both Directions of Half Adjoints are Logically Equivalent
  • Fibers
    • Fibers of Half Adjoint Equivalences are Contractible
  • Left and Right Inverses
  • Coherence Types for Equivalences
  • Half Adjoint Equivalences are Mere Propositions
• Bi-invertible Maps
• Contractible Fibers
• Surjections and Embeddings
• Surjection and Embedding are equivalent to Equivalences
• Retracts
  • Retract of an Equivalence is an Equivalence
• Total Spaces
  • A Fiberwise Transformation is an Equivalence if its Total is an Equivalence
• Fiber of first projection of Sigma Types
  • Sum of all Fibers of a Function is the Domain
• Sum off all Functions from all types are equivalent to a type family
• Object Classifiers
• Weak Function Extensionality
  • Functions types to isomorphic types are isomorphic
  • Univalence Implies Weak Function Extensionality
  • Univalence Implies Function Extensionality

Inductive Types

• Inductive Types
  • Uniqueness of functions created using induction principle
• Similar description of inductive types lead to equal types
• W-Types
  • Examples for W-Types
  • Double on Natural Numbers using W-Types
• Inductive Types are Initial Algebras
  • Type of Natural Number Algebra
    • N is the initial object in the category of N-Algebras
  • Type of W-Algebras
    • W-Types are the initial element in the category of W-Algebras
• Homotopy Inductive Types
  • Some ways to Characterize Homotopy W types
• Some Generalization of Inductive Datatypes
  • Identity Types form an Inductive Family
• Pointed Predicates and maps
• Identity System at a point
• Identity System
• Equivalence Induction

Higher Inductive Types

• Higher Inductive Types
• Rules for Higher Inductive Types
• Interval
  • Interval is Contractible
• Circle
  • Loop is not refl
  • There is a non-trivial proof for reflexivity of equality in Circle
  • Universe with circle is not a groupoid
• Sphere
• Suspensions (HoTT)
  • Suspension of Boolean Type is Circle

---

MOCs

• Category Theory
• Set Theory
• Logic
• Topology

---

References