homotopy type theory

homotopy type

univalence, function extensionality, internal logic of an (∞,1)-topos

cohesive homotopy type theory

directed homotopy type theory

HoTT methods for homotopy theorists