[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] I think we should forget about the syntactic rules completely and just describe everything in terms of universal properties (i.e. homotopy initiality and homotopy terminality): After we have defined dependent function types and dependent sum types as negative types, and after we have defined identity types on a type $A$ to be a reflexive graph on $A$, then we could define contractibility and the uniqueness quantifier, and use that to express homotopy initiality and terminality of objects: * identity types on $A$ are the initial reflexive graph on a type $A$ * natural numbers are the initial type with an element and an endofunction * sum types are the initial cospan * dependent sum types over a type family indexed by type $A$ are the initial wide cospan indexed by $A$ There are too many models of type theory * There are the Martin-Löf type theories where identity types are defined positively using induction principles * There are the (non-modal) cubical type theories where identity types are defined negatively using functions from an interval type * There are the observational type theories where identity types are defined from other identity types * There are the dependent type theories which use recursion (and uniquness) principles instead of induction principles, which makes it a lot more like infinity-topos theory. category: redirected to nlab