Naturality for Higher Dimensional Path Types
We define a naturality construction for the operations of weak omega-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a …
Homotopy.io
We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories.
CaTT contexts are finite computads
Two novel descriptions of weak omega-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are …
Posetal Diagrams
We now have a wide range of proof assistants available for compositional reasoning in monoidal or higher categories which are free on some generating signature. However, none of …
