Project topics and materials
Get Complete Project Material File(s) Now! »
The Grothendieck-Maltsiniotis definition of !-categories
This entire section is a quick presentation of the definition of weak !-categories given by Maltsin-iotis [54], relying on the ideas for defining weak !-groupoids introduced by Grothendieck [39]. The aim is to introduce the notions that the type theory CaTT relies on, as well as the notations we will use for these notions. For a more in-depth study of this definition, one can refer to the original article by Maltsiniotis [54] or by a full account of this definition by Ara [4]
The category of globes and globular sets.
Similar to how the regular categories are supported by graphs, !-categories are supported by a structure called globular sets. These are generalization of graphs that do not only include vertices and arrows, but also arrows between the arrows (2-cells), arrows between the 2-cells (3-cells) and so on. A convenient way to define the category of globular set is as a presheaf category. The category of globes. We denote G the category whose objects are the natural numbers 0, 1, . . . and whose morphisms are generated by the graph.
Globular extensions
In the following, we consider a category C equipped with a functor F : G ! C, such a functor is called a globular structure on C. In this case, we denote Dn the object F (n) of C, and we still denote n and ⌧n the images by F of the morphisms n and ⌧n. When there is no ambiguity, we may write and ⌧ , leaving the index implicit, moreover, we write also (resp. ⌧ ) to indicate a composite of maps of the form (resp. ⌧ ). Dually, for a category C, a functor F : GOP ! C is called a coglobular structure, and we denote respectively by Dn, @n+ and @n+ the images by F of [n], n and ⌧n. We thus always denote and ⌧ families of maps satisfying the coglobular relations and @ and @+ families of maps satisfying the globular relations. Globular sums. In the category C equipped with a globular structure, a globular sum is a colimit of a diagram of the form.
Weak !-categories
The notion of a globular theory formalizes a theory in the globular sets, for which the operations we introduce may have generalized arities that have all the shapes allowed by the pasting schemes. For instance, consider the following pasting scheme C that we describe as a diagram and as a globular sum together with a globular theory C in which there is a morphism µ : C ! D1. Then a functor : COP ! SET induces a coglobular structure on SET, which is the same as a globular set X; suppose that F preserves the globular products of COP for this coglobular structure. The functor then sends the morphism µ onto an operation m : X(1) ⇥X(0) X(1) ! X(1), that is given two 1-cells f, g 2 X(1) such that @+(f ) = @ (g), the operation m gives a 1-cell m(f, g) 2 X(1).
Moreover, the interaction of µ with and ⌧ in C specify the source and target of the cell obtained by applying m. This shows that a globular theory expresses a notion of theory allowing the inputs to have shapes specified by the pasting schemes. This situation is analogue to Lawvere theories: The objects are freely generated by a class of colimits (sums for Lawvere theories, globular sums for globular theories), the additional morphisms define operations, and the equality between the morphisms give axioms. Weak !-categories fall precisely under this scope, and thus can be defined as a particular globular theory. Admissible pairs of arrows. Let G ! C be a globular extension, two arrows f, g : Di ! X in C are said to be parallel when f i = g i f ⌧i = g ⌧i If C is a globular theory, then a morphism f of C is said to be algebraic, when for every de-composition f = gf 0, with g globular, then g is an identity. Intuitively, an algebraic morphism is a morphism f : Di ! X of C that is “full” on its source, i.e., it cannot be decomposed as f 0 : Di ! X 0 followed by an inclusion X0 ,! X They are the primitive morphisms of the form Di ! X, in the sense all the other morphisms of this form are obtained as an inclusion of an algebraic morphism. A pair of parallel arrows f, g : Di ! X is called an admissible pair if either both f and g are algebraic, or there exists a decomposition f = X f 0 and g = ⌧X g0, with f 0 and g0 algebraic. A lift for an admissible pair f, g : Di ! X is a morphism h : Di+1 ! X such that Dually, in a coglobular theory C, an arrow is said to be coalgebraic if its opposite is algebraic in the globular theory COP , and a pair of arrows is called a coadmissible pair if the opposite pair is admissible in COP .
Table of contents :
1 Introduction to type theory
1.1 Introduction to type theories
1.1.1 Conventions and notations
1.1.2 Cut-full type theory
1.1.3 Cut-free type theory
1.1.4 Categorical structure of a type theory
1.2 Semantics of type theory
1.2.1 Categories with families
1.2.2 Most general unifiers
1.2.3 Categorical notions of theories
2 A type theory for globular !-categories
2.1 The Grothendieck-Maltsiniotis definition of !-categories
2.1.1 The category of globes and globular sets
2.1.2 Globular extensions
2.1.3 Weak !-categories
2.1.4 Identities and compositions
2.2 A type theory for globular sets
2.2.1 The type theory GSeTT
2.2.2 Formalization
2.2.3 Yoneda embedding and nerve functor
2.2.4 The syntactic category SGSeTT
2.2.5 Models of SGSeTT
2.2.6 Coglobular structure on categories with families
2.3 Pasting schemes as contexts
2.3.1 Ps-contexts
2.3.2 Ps-contexts are normalized pasting schemes
2.3.3 The relation /
2.4 A type theory for globular weak !-categories
2.4.1 Type theory
2.4.2 Some examples of derivations
2.4.3 Syntactic properties
2.5 The syntactic category of CaTT
2.5.1 The category of ps-contexts with coherences
2.5.2 Kan extensions and density
2.5.3 A characterization of substitutions
2.5.4 SCaTT as a free completion
2.5.5 Functors preserving globular products
2.6 Models of CaTT
2.6.1 The syntactic category
2.6.2 Towards a structure with weak functors
3 Practical use and partial automation
3.1 Implementation
3.1.1 Syntax
3.1.2 Declaration
3.1.3 Implicit arguments
3.1.4 An extensive example: the Eckmann-Hilton morphism
3.2 Suspension
3.2.1 Example of suspensions
3.2.2 Suspension of ps-contexts
3.2.3 Suspension for the theory CaTT
3.2.4 Implementation of the suspension
3.3 Degree of a term
3.3.1 Definition of the degree
3.3.2 Terms of degree 0
3.3.3 Degree and invertibility
3.3.4 Degree for automation
3.4 Functorialization
3.4.1 Functorialization of contexts
3.4.2 Functorialization of a maximal variable in a ps-context
3.4.3 Functorialization of a term
3.4.4 Implementation and restrictions
3.5 The category SPS,1
3.5.1 Equivalence between the rules (coh) and (coh’)
3.5.2 The category SPS,1 and the cat-coherator
4 A type theoretic framework for monads with arities
4.1 A framework for globular type theories
4.1.1 Presentation of the framework
4.1.2 Properties
4.1.3 Non-free globular type theories
4.2 Free category with families over a direct category
4.2.1 Type theory associated to a direct category
4.2.2 The syntactic category STI
4.2.3 Examples
4.3 I-type theories
4.3.1 Properties
4.4 I-contextual categories
4.4.1 I-contextual categories
4.4.2 Monads with arities
4.4.3 Equivalence
4.4.4 Interpretation of our work
5 Monoidal weak !-categories
5.1 Monoidal and multiply monoidal weak !-categories
5.1.1 Delooping of a monoidal category
5.1.2 k-tuply monoidal categories
5.2 Type theory for monoidal weak !-category
5.2.1 The theory MCaTT
5.2.2 Properties of the desuspension
5.2.3 Reduced suspension
5.2.4 Interaction between desuspension and reduced suspension
5.2.5 Models of the type theory MCaTT
5.2.6 Interpretation
5.3 An alternative presentation of MCaTT
5.3.1 A framework for type theories with local exchange
5.3.2 Monoidal ps-contexts
5.3.3 Folding and flattening
5.3.4 Equivalence between MCaTT and MCaTT0
5.3.5 Examples of derivations
5.4 Towards k-tuply monoidal weak !-category
6 Cubical weak !-categories
6.1 Type theory for pre-cubical sets
6.1.1 The category of pre-cubical sets
6.1.2 Type theory for pre-cubical sets
6.1.3 Functorialization in the theory T⇤
6.1.4 Extrusion of a variable
6.2 Type theory for cubical !-categories
6.2.1 Ps-contexts
6.2.2 Examples of derivation
6.2.3 Comparison with cubical type theory
6.3 Pre-cubical weak ! category
6.3.1 Monoidal structure of pre-cubical Sets
6.3.2 Cubical extensions
6.3.3 Cubical Cat-coherator
6.3.4 Coherator of the theory CaTT⇤
A Presentation of the type theories
A.1 The type theory GSeTT
A.2 The type theory CaTT
A.3 The theory MCaTT
A.4 The theory MCaTT0
A.5 The theory T⇤
A.6 The theory CaTT⇤
B Summary of the formalized results
B.1 Formalized results for the theory GSeTT
B.2 Formalized results for globular type theories
B.3 Formalized results for the theory CaTT .
