\( \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\uHom}{\,\underline{\!Hom\!}\,} \DeclareMathOperator{\Mor}{Mor} \DeclareMathOperator{\Map}{Map} \DeclareMathOperator{\map}{map} \DeclareMathOperator*{\colim}{colim} \DeclareMathOperator{\id}{id} \DeclareMathOperator{\Id}{Id} \DeclareMathOperator{\Ob}{Ob} \DeclareMathOperator{\comp}{comp} \DeclareMathOperator{\Fun}{Fun} \DeclareMathOperator{\true}{true} \DeclareMathOperator{\Sub}{Sub} \DeclareMathOperator{\Lan}{Lan} \DeclareMathOperator{\Ran}{Ran} \DeclareMathOperator{\PSh}{PSh} \DeclareMathOperator{\Sh}{Sh} \DeclareMathOperator{\Sp}{Sp} \DeclareMathOperator{\Glue}{Glue} \DeclareMathOperator{\Res}{Res} \DeclareMathOperator{\End}{End} \DeclareMathOperator{\oneim}{1im} \DeclareMathOperator{\twoim}{2im} \DeclareMathOperator{\charr}{char} \DeclareMathOperator{\Spec}{Spec} \newcommand{\ProFinSet}{\mathrm{ProFinSet}} \newcommand{\sSet}{\mathrm{sSet}} \newcommand{\Top}{\mathrm{Top}} \newcommand{\deltacat}{\boldsymbol{\Delta}} \newcommand{\Cat}{\mathrm{Cat}} \newcommand{\Set}{\mathrm{Set}} \newcommand{\Ring}{\mathrm{Ring}} \newcommand{\CatMon}{\mathrm{CatMon}} \newcommand{\Cof}{\mathrm{Cof}} \newcommand{\Fib}{\mathrm{Fib}} \newcommand{\Frm}{\mathrm{Frm}} \newcommand{\Loc}{\mathrm{Loc}}\)

Homotopy Type Theory

Table of Contents

1. Rules of Homotopy Type Theory

A type is fully determined by the ways of constructing a term of it. Hence we should think of the type \( T \) being freely generated by its finitely many construction rules \( C_1, \dots, C_n \), ie there are no additional elements of \( T \) that can’t be constructed using the rules \( C_1, \dots, C_n \) and there are no additional equalities between elements of \( T \) that are not determined by the rules \( C_1, \dots, C_n \). For example the truth type \( \top \) is specified by one rule: \( * : \top \). Hence there really is only one term in \( \top \). But what does this mean? It means that the proposition \( \forall x : \top, x = * \) is true, but interpreted as the correct (internal) proposition in (homotopy) type theory, ie the type \( \prod x : \top, x = * \) is true which means we can construct a term \( f \) in it. The term is simply constructed by \( f * = refl_x \)

Author: Frederik Gebert

Created: 2025-02-10 Mon 21:45