## Types are ## Brunerie globular weak -groupoids #### Younesse Kaddar ##### Supervised by: ###### Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus Nottingham University, June-July 2017

### Work Environment ____ ### I. Motivations ### II. Weak -groupoids ### III. Categories with Families \& Brunerie weak -groupoids ### IV. Agda implementation \& Conclusion

### I. Motivations

#### A. What is wrong with set theory In set theory: <p align="center"></p>

1. Poorness of the very notion of set:

• far-fetched definitions
• reasoning up to isomorphism made difficult
2. Non-constructive

## I.B - Vladimir Voevodsky’s new foundational program (2006/2009) • Mistake in one of his papers

• Modern mathematical proofs: too complex to be reliably checked by humans
• ⟶ Since then, has been championing computer proof assistants
> **Univalent Foundations / Homotopy Type Theory**: > > new constructive foundations for mathematics based on *Per Martin-Löf’s dependent type theory*. The functional programming language / proof assistant **Agda**: based on dependent type theory. ## Martin-Löf’s Dependent Type Theory (MLTT)… in a nutshell

__

1) A **foundational framework** for mathematics 2) A **programming language** - more expressive than simply-typed -calculus (the "idealized" version of simply-typed functional programming languages such as OCaml)

In Type theory: - contexts (denoted by the letters - types () - terms () - substitutions (). and a collection of **inference rules** to form new types/terms. > **Types** can depend on values

### Contexts

A context :

: is a list (of assumptions) <p align="center"><img src=”https://latex.codecogs.com/gif.latex?\, \\ x_1 : A_1, \, x_2:A_2(x_1) \, \ldots, \, x_n:A_n(x_1, \ldots, x_{n-1}) \\A_i(x_1, \ldots, x_{i-1})x_1, \ldots, x_{i-1}A_1(x_1), \ldots, A_{i-1}(x_1, \ldots, x_{i-2})np𝕂p^nV𝕂Γn, p, 𝕂V\Gamma \vdash a {:} AaAΓ| and are definitionally/judgmentally equal objects of type in __<div class="fragment fade-down" data-fragment-index="1">Types play the role of- sets- <span class="fragment fade-down" data-fragment-index="2">… as well as logical propositions!</span><div class="fragment fade-down" data-fragment-index="3"><br />> **The Curry-Howard correspondence**:>> proving a mathematical statement in Type Theory>> ⟺> > providing an element of its corresponding type.</div></div><!– slide data-transition:"concave" data-transition-speed:"slow" vertical:true data-background-image:dark-background.jpg –><div class="text-align: left">### The Curry-Howard correspondence: Example<br />**$\Pi$-types (dependent products)**:: the types of functions whose result depends on the argument> e.g. functions such that for each ##### *Via the Curry-Howard correspondence*:dependent products express universal quantification, such as”/></p>∀x ∈ A, B(x)<p align="center"></p>∀x, y ∈ ℕ, x + y = y + x<p align="center"></p>f : \prod\limits{x: ℕ} \prod\limits_{y: ℕ} x + y = y + x<p align="center"><img src=”https://latex.codecogs.com/gif.latex?>> such that, for instance, is evidence that .</div><!– slide data-transition:"concave" data-transition-speed:"slow" vertical:true data-background-image:dark-background.jpg –>-types:: **existential quantification** represented as an indexed pair, where the type of the second component depends on the first.>”/></p>(a,b):\Sigma {(x:A)}B(x)<p align="center"><img src=”https://latex.codecogs.com/gif.latex?>> ⟺>> and .Proof assistants make use of the Curry-Howard correspondence.__<div class="fragment fade-down" data-fragment-index="1" style="text-align:left">#### Examples of dependent types- : type of -tuples:”/></p>(a_1, \ldots, a_n) : A^n<p align="center"><img src=”https://latex.codecogs.com/gif.latex?where .- For all natural number , (proofs that is even)- For all natural numbers : (evidence that is greater than )</div><!– slide data-transition:"concave" data-transition-speed:"slow" vertical:true data-background-image:dark-background.jpg –>### Substitutions / Context MorphismsA substitution :: a list of terms”/></p>σ ≝ (t_1, \ldots, t_n)<p align="center"></p> \begin{aligned} Δ &\vdash t_1 :A_1
Δ &\vdash t_2 :A_1(t_2)
\vdots
Δ &\vdash t_n : A_n(t_1,t_2,\dots, t
{n-1}) \end{aligned}

<img src="https://latex.codecogs.com/gif.latex?_____*Notation*: applied in is written (free variables substituted by their corresponding term in ), idem for types.> - > - >>"/>

\begin{aligned} Δ &\vdash q : ℕ
Δ &\vdash q :{\rm Prime}
Δ &\vdash 𝕃 :{\rm Field} \, q^q
Δ &\vdash A : 𝕃-{\rm Algebra} \end{aligned}

\frac{\Gamma \vdash A \hspace{1em} \Gamma \vdash a {:} A \hspace{1em} \Gamma \vdash a’ {:} A} {\Gamma \vdash a ≃A a’}<p align="center"></p>\frac{\Gamma \vdash A \hspace{1em} \Gamma \vdash a {:} A} {\Gamma \vdash \refl {:} a ≃_A a}<p align="center"></p>\frac{ \Gamma \vdash x:A \hspace{1em} \Gamma, y: A, p: x ≃_A y \vdash P(y, p) \hspace{1em} \Gamma \vdash d {:} P(x, \refl_x)} { \Gamma, y: A, p: x ≃_A y \vdash \J(y, p, d) {:} P(y, p)}<p align="center"></p>\J(x, \refl_x, d) ≡ d {:} P(x, \refl_x)<p align="center"><img src=”https://latex.codecogs.com/gif.latex?<!– slide data-transition:"convex" data-transition-speed:"slow" –>### I.C. Homotopy Type Theory<img alt="Homotopy" src="HomotopySmall.gif" style="float:left"/><div style="text-align:left; padding-left: 300px">In homotopy theory, two paths are said to be homotopic if one can be "continuously deformed" into the other.In homotopy type theory (a new flavour of MLTT):</div>- a <span class="fragment highlight-red" data-fragment-index="1">type </span> is *abstractly* seen as a <span class="fragment highlight-red" data-fragment-index="1">topological space</span> whose points are its objects - if , represents the <span class="fragment highlight-blue" data-fragment-index="2">paths</span> from (start point) to (end point). - given two parallel paths , a path corresponds to a <span class="fragment highlight-blue" data-fragment-index="3">homotopy/2-path</span> between and . - is the type of <span class="fragment highlight-blue" data-fragment-index="4">3-paths</span>, and so on…<div class="xypic-block" style="height:400px; width:600px; float:left"><img src="xy_1.svg" style="border:none" /></div>The tower comprised of these paths, paths of paths, paths of paths of paths, … arising from forms an -groupoid<!– slide vertical:true data-transition:"convex" data-transition-speed:"slow" data-background-image:"outburst.png" –>## The Univalence Axiom> Univalence Axiom in Voevodsky’s univalent program:>> : equality of types is (weakly) equivalent to equivalence⟶ This axiom is not constructive *per se*> Eliminating univalence is a holy grail… and formalizing a weak -groupoid model of Type Theory inside Type Theory might pave the way for it!<!– slide data-transition:"convex" data-transition-speed:"slow" –>## II. Weak -groupoids#### Comparison of structures and laws of different algebraic structures&nbsp; | Monoids | Categories | Higher Categories | Strict -Groupoids-|-|-|-|-Carrier set/Underlying set | Sets | Multigraphs | Globular Sets | Globular SetsStructure | Binary operation, Neutral element | Composition, Identity morphisms | Compositions, Identity morphisms | Compositions, Identity morphisms, Inverse elementsLaws | Associativity, Unit law | Associativity, Unit law | Associativity, Unit law, Interchange law | Associativity, Unit law, Interchange law, Inverse law<!– slide vertical:true data-transition:"convex" data-transition-speed:"slow" –>A globular set:: is a family of sets $(G_n){n∈ℕ}$ and functions $s_n, t_n: G_n ⟶ G_{n-1}$ (which stand for source and target respectively) such that, for all :”/></p> \begin{cases} s_{n-1} \circ s_n = s_{n-1} \circ t_n &
t_{n-1} \circ s_n = t_{n-1} \circ t_n \end{cases} \qquad\textit{(subscripts in will be omitted)}

<img src="https://latex.codecogs.com/gif.latex?### Intuition<div class="xypic-block" style="height:400px; width:600px; float:right"><img src="xy_2.svg" /></div>- the points $\bullet$ are members of $G_0$- $a, b∈ G_1$- $θ ∈ G_2$- $s(θ) ≝ a$- $t(θ) ≝ b$ *i.e.*: > All sources and their corresponding targets are parallel.For all $n∈ℕ^\ast, \; a, b:G_{n-1}$, The elements of $G_n$ are called *$n$-arrows*.<!-- slide vertical:true data-transition:"zoom" data-transition-speed:"slow" -->### Laws and Structure of -groupoids| **Strict** -groupoids| **Weak** -groupoids|-|-usual pattern: structures (compositions, identity elements, inverse elements) and laws (associativity, interchange law, identity law, inverse law) | **nothing but structure**. Laws and structures with regard to elements of $G_n$ now become elements of $G_{n+1}$._______### Strict $𝜔$-groupoidsLet $G ≝ \bigsqcup\limits_{n≥0} G_n$ be a **strict** $𝜔$-groupoid.<div style="text-align:left">Dimension skips:: If $i > j > k ∈ ℕ, \; \; x, x' : G_k, \; f, f' : G_j(x, x')$ and $𝛼 : G_i(f, f')$, then $𝛼$ can be seen as $k$-arrow of $G_k(x, x')$<span class="xypic-block" style="height:400px; width:600px; float:right;"><img src="xy_3.svg" style="height:400px; width:600px; float:right;"/></span>*Indeed*: for all $n∈ℕ^\ast$ and $f_1, \ldots, f_n ∈ \lbrace s, t \rbrace$: \[ \begin{cases} s \; f_1 \; \ldots \; f_n = s \\ t \; f_1 \; \ldots \; f_n = t \end{cases}"/>

⟶ only the leftmost composition matters.

</div>

### Structure of

Identity: <p align="center"></p>
Inverse: <p align="center"></p>

There are different types of compositions in : .

Let .

Horizontal Composition (along the -arrows) Vertical Composition (along the -arrows)
<p align="center"></p> <p align="center"><img src=”https://latex.codecogs.com/gif.latex?\; \\ \scol^n_n: \prod\limits_{x, x': G_0}\prod\limits_{f, f', f'': G_i(x, x')} \\ G_n(f, f') × G_n(f', f'') ⟶ G_n(f, f'') \\<img src=”https://latex.codecogs.com/gif.latex?$"/></p>\; \\ \cfrac{𝛼:G_i(x, x')\qquad 𝛼': G_i(x', x'')}{𝛼 \scol_i^n 𝛼': G_i(x, x'')} \\$”/> <p align="center"><img src=”https://latex.codecogs.com/gif.latex?\; \\ \cfrac{𝛼:G_n(f, f') \qquad 𝛼': G_n(f', f'')}{𝛼 \scol_n^n 𝛼': G_n(f, f'')} \\<img src=”https://latex.codecogs.com/gif.latex?\$   &lt;br &#x2F;&gt;&lt;div class=&quot;xypic-block&quot; style=&quot;height:400px; width:600px&quot;&gt;&lt;img src=&quot;xy_4.svg&quot; style=&quot;height:400px; width:600px&quot;&#x2F;&gt;&lt;&#x2F;div&gt; &lt;br &#x2F;&gt;&lt;div class=&quot;xypic-block&quot; style=&quot;height:400px; width:600px&quot;&gt;&lt;img src=&quot;xy_5.svg&quot; style=&quot;height:400px; width:600px&quot;&#x2F;&gt;&lt;&#x2F;div&gt; &lt;!– slide vertical:true data-transition:&quot;convex&quot; data-transition-speed:&quot;slow&quot; –&gt;### Laws of &#x5C;(G_n&#x5C;)     - -Identity (&#x5C;(i&#x5C;)): &#x5C;(x:G_i&#x5C;) &lt;div class=&quot;xypic-block&quot; style=&quot;height:200px; width:600px&quot;&gt;&lt;img src=&quot;xy_identity.svg&quot; style=&quot;height:200px; width:600px&quot;&#x2F;&gt;&lt;&#x2F;div&gt;Composition (&#x5C;(i &lt; j&#x5C;)): the points &#x5C;(x, x&#x27;, x&#x27;&#x27; : G_i&#x5C;), the simple arrows &#x5C;(f, g : G_j&#x5C;) &lt;br &#x2F;&gt;&lt;div class=&quot;xypic-block&quot; style=&quot;height:150px; width:600px&quot;&gt;&lt;img src=&quot;xy_composition.svg&quot; style=&quot;height:150px; width:600px&quot; &#x2F;&gt;&lt;&#x2F;div&gt;Identity Laws (&#x5C;(i&lt;j&#x5C;)): the points &#x5C;(x, x&#x27; : G_i&#x5C;), the simple arrow &#x5C;(f : G_j&#x5C;) Left: &lt;div class=&quot;xypic-block&quot; style=&quot;height:400px; width:600px&quot;&gt;&lt;img src=&quot;xy_identity_law.svg&quot; style=&quot;height:400px; width:600px&quot;&#x2F;&gt;&lt;&#x2F;div&gt; Right: idem&lt;!– slide vertical:true data-transition:&quot;convex&quot; data-transition-speed:&quot;slow&quot; –&gt;Associativity law (&#x5C;(i &lt; j&#x5C;)): the points &#x5C;(x, x&#x27;, x&#x27;&#x27;, x&#x27;&#x27;&#x27; : G_i&#x5C;), the simple arrows &#x5C;(f, g, h : G_j&#x5C;)&lt;div class=&quot;xypic-block&quot; style=&quot;height:350px; width:700px; margin:auto&quot;&gt;&lt;img src=&quot;xy_assoc.svg&quot; style=&quot;height:350px; width:700px&quot;&#x2F;&gt;&lt;&#x2F;div&gt;__Interchange law (&#x5C;(i &lt; j &lt; k&#x5C;)): the points &#x5C;(x, x&#x27;, x&#x27;&#x27; : G_i&#x5C;), the simple arrows &#x5C;(f, f&#x27;, f&#x27;&#x27;, g, g&#x27;, g&#x27;&#x27; : G_j&#x5C;), the double arrows &#x5C;(𝛼, 𝛼&#x27;, 𝛽, 𝛽&#x27; : G_k&#x5C;)&lt;div class=&quot;xypic-block&quot; style=&quot;height:600px; width:700px; margin:auto&quot;&gt;&lt;img src=&quot;xy_interchange.svg&quot; style=&quot;height:600px; width:700px&quot;&#x2F;&gt;&lt;&#x2F;div&gt;&lt;!– slide vertical:true data-transition:&quot;zoom&quot; data-transition-speed:&quot;slow&quot; –&gt;## Weak &#x5C;(𝜔&#x5C;)-groupoids: handmade partial construction### &#x5C;(G_1&#x5C;)- *Identity*: &#x5C;[{&#x5C;rm id}^1 (&#x5C; ) : &#x5C;prod&#x5C;limits_{a: G_0} G_1(a, a)"/></p>- Inverse: <p align="center"><img src="https://latex.codecogs.com/gif.latex?{&#x5C;rm inv}^1 (&#x5C;_ , &#x5C;_ ) : &#x5C;prod&#x5C;limits_{a, b: G_0} G_1(a, b) ⟶ G_1(b, a)"/></p>- Composition: <p align="center"><img src="https://latex.codecogs.com/gif.latex?&#x5C;scol^11 (&#x5C; , &#x5C;_ , &#x5C;_ ) : &#x5C;prod&#x5C;limits_{a, b, c: G_0} G_1(a, b) × G_1(b, c) ⟶ G_1(a, c)"/></p>### \(G_2”/>
• Identity: <p align="center"></p>
• Inverse: <p align="center"></p> • Horizontal Composition (along the -arrows): • Vertical Composition (along the -arrows):

• Associativity along the -arrows}: <p align="center"></p>

#### “Laws” that have become structure

• Left identity “law”: <p align="center"></p>

• Right identity “law”: <p align="center"></p>

• Left inverse “law”: <p align="center"></p>

• Right inverse “law”: <p align="center"></p>

### , and so on…

At level , in addition, we have to take into account

• the interchange law between the 2-arrows and the 1-arrows: <p align="center"></p>

• the different compositions

• the associativity along the -arrows: <p align="center"></p>

• etc…

But that’s not it!

### Coherence laws in :

Equations between elements of have been replaced by new 2-arrows.

But one also requires that these 2-arrows satisfy some new equations (represented by new 3-arrows) of their own, called coherence laws!

For instance, there are 5 ways to parenthesize the composition of 4 1-arrows in , which are related as follows: We impose a coherence law - the \emph{pentagon identity} - (which becomes a new 3-arrow), stating that all these ways are identical (up to a 3-arrow).

Analogously, another coherence law says that composing with the left identity then with the right identity and composing with the right identity then with the left one are the same thing.

## II. Brunerie Type Theory

Brunerie type theory :

where (which stands for is contractible) is inductively defined as follows:

### The intuition behind is that

• the elements of the base type correspond to the elements of the set of the underlying globular set of the weak -groupoid.

• if the elements of are the 1-arrows of

• if and , the elements of are those of

• and so on…

a context will be depicted as A context is contractible if it can be “reduced to a point”, by contracting along the arrows.

### Example

• the context is contractible • but the context is not: because of the hole between and (we cannot contract and ).

But if the hole between and is filled by a 2-arrow, like in then it becomes contractible.

Example: the associativity law along the -arrows.

Let and First, how to define composition along the -arrows?

As

• the context is contractible
• and (since )

can be defined in as

Idem for the other compositions.

Now, there exists a <p align="center"></p>

in , since is contractible and )!

## III. Categories with Families

a category is given by:

• Structure:

• Objects: a class of objects, denoted

• Arrows: for each pair of objects , a “collection” of arrows (or morphisms) from to denoted by , or .

For each ,

• is denoted by or
• is the domain of , its codomain

• Composition: for each pair of morphisms and , a composite arrow (and )

• Identity: for each object , an identity morphism
• Laws:

• Associativity of composition: for each , <p align="center"></p>
• Unit law: for each ,

### Dual Category

The dual category of a category :

: has the same objects as , and all of its arrows are “turned around”: <p align="center"></p>

### Functors

Let be two categories.

a (covariant) functor from to is a mapping such that:

• for each object in , is an object in

• for each morphism in , (also written ) is a morphism from to in

• Preservation of composition: for all morphisms in .

• Preservation of identity: for each object in

### Initial and terminal objects

An object (resp. ) in a category is initial (resp. terminal):

: if for every object , there exists a unique arrow from to (resp. from to ).

### Slice and coslice categories

Let be a category and an object of .

The slice category is described as follows:

• An object of is a pair where and in .
• An arrow of from to is an arrow such that

The coslice category is the dual category of .

### Category of elements

Let be a functor.

The category of elements is described as follows:

• An object of is a pair where and .
• An arrow of from to is an arrow such that

a Category with Families (abbreviated CwF) is given by:

• a category , with a terminal object (the empty context)
• a functor <p align="center"></p>
• a functor from the category of elements of : <p align="center"></p>

• Universal property of context extension: for each , the following functor from the slice category <p align="center"></p>

is represented by an object , which roughly means that:

for each context morphism and type , there is a “natural” (it does not depend on the variable ) isomorphism:

A Brunerie CwF (resp. CwF with base-typed intensional identity) is a CwF which “respects” the inference rules of Brunerie type theory (resp. of type theory comprised of the “base type rule” and intensional identity).

The category of Brunerie CwFs: (resp. ) has an initial object (resp. ).

A Brunerie globular weak -groupoid is a weak CwF-morphism from to

To show that types form Brunerie globular weak -groupoids, we proceed by demonstrating that there exist CwF-morphisms

whose composition constitute the Brunerie globular weak -groupoid associated with the terms of a given type . 