## 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)

HoTT book authors

  • 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*.

Agda logo   The functional programming language / proof assistant **Agda**: based on dependent type theory. Agda code

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 .