Introduction
Category of conditional probabilities $𝒫$
-
objects: countably generated measurable spaces $(X, Σ_X)$
-
morphisms: Markov kernels \(T: \begin{cases} Σ_Y × X &⟶ [0, 1] \\ (B, x) &⟼ T(B \mid x) \end{cases}\) s.t.:
- $T_B ≝ T(B \mid \bullet): X ⟶ [0, 1]$ measurable $\quad ∀ B∈ Σ_Y$
-
$T_x ≝ T(\bullet \mid x): Σ_Y ⟶ ℬ([0, 1])$ perfect probability measure on $Y \quad ∀x∈X$
i.e. $∀ f: Y ⟶ ℝ$ measurable, $∃ E ⊆ f(Y)$ a Borel set s.t. \(T_x(f^{-1}(E)) = 1\)
-
composition of arrows $X \overset{T}{⟶} Y \overset{U}{⟶} Z$: \(U \circ T : \begin{cases} Σ_Z × X &⟶ [0, 1] \\ (C, x) &⟼ (U \circ T)(C \mid x) ≝ 𝔼_{T_x}(U_C) = \int_{y∈Y} U(C \mid y) \, {\rm d}T_x \end{cases}\)
Category of measurable spaces $\mathcal{Meas}$
-
objects: measurable spaces $(X, Σ_X)$
-
morphisms: measurable functions $f: X ⟶ Y$
where \(δ_f(B \mid x) ≝ \mathbb{1}_{f^{-1}(B)}(x): Σ_Y × X ⟶ [0, 1]\)
\[δ: \begin{cases} \mathcal{M_{cg}} &⟶ 𝒫 \\ (X, Σ_X) &⟼ (X, Σ_X)\\ f:X ⟶ Y &⟼ δ_f ≝ (B \mid x) ⟼ \mathbb{1}_{f^{-1}(B)}(x) \end{cases}\]is a functor
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
The functional programming language / proof assistant **Agda**: based on dependent type theory.
Martin-Löf’s Dependent Type Theory (MLTT)… in a nutshell
__
Contexts
- A context $Γ$:
-
is a list (of assumptions) \(\, \\ x_1 : A_1, \, x_2:A_2(x_1) \, \ldots, \, x_n:A_n(x_1, \ldots, x_{n-1}) \\\) of variables, such that each type $A_i(x_1, \ldots, x_{i-1})$ depends on variables $x_1, \ldots, x_{i-1}$ of earlier types $A_1(x_1), \ldots, A_{i-1}(x_1, \ldots, x_{i-2})$.
Types and Terms
Inference rules enable us to derive judgments of the form:
| Judgement | Interpreted as |
|---|---|
| $\Gamma \vdash a {:} A$ | $a$ is a term of type $A$ in the context $Γ$ |
| $\Gamma \vdash a ≡ b {:} A$ | $a$ and $b$ are definitionally/judgmentally equal objects of type $A$ in $Γ$ |
> **The Curry-Howard correspondence**: > > proving a mathematical statement in Type Theory > > ⟺ > > providing an element of its corresponding type.
**\(\Pi\)-types (dependent products)**: : the types of functions whose result depends on the argument > e.g. functions $f : (x:A) ⟶ B(x)$ such that $f(x): B(x)$ for each $x: A$ ##### *Via the Curry-Howard correspondence*: dependent products express universal quantification, such as $$∀x ∈ A, B(x)$$ _____ > *Ex*: A proof of > > $$∀x, y ∈ ℕ, x + y = y + x$$ > > is a dependent function of type > > $$f : \prod\limits_{x: ℕ} \prod\limits_{y: ℕ} x + y = y + x$$ > > such that, for instance, $f(1, 2)$ is evidence that $1 + 2 = 2 + 1$.
- $Σ$-types:
-
existential quantification represented as an indexed pair, where the type of the second component depends on the first.
\[(a,b):\Sigma _{(x:A)}B(x)\]⟺
$a:A$ and $b:B(a)$.
Proof assistants make use of the Curry-Howard correspondence.
Substitutions / Context Morphisms
- A substitution $σ: Δ ⟶ \overbrace{Γ}^{\rlap{≝\; x_1:A_1,\; x_2:A_2(x_1),\;\ldots,\; x_n:A_n(x_1, \ldots, x_{n-1})}}$:
-
a list of terms \(σ ≝ (t_1, \ldots, t_n)\) such that
Notation: $σ: Δ ⟶ Γ$ applied in $Γ ⊢ t: A$ is written $t[σ]$ (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}\]
- $Γ ≝ (n: ℕ, \; p:{\rm Prime}, \; 𝕂: {\rm Field} \, p^n, \; V: 𝕂\text{-}{\rm VectorSpace})$
- $Δ ≝ (q: {\rm PalindromicPrime}, 𝕃: {\rm TopologicalField} \, q^q, \; A : 𝕃\text{-}{\rm Algebra})$
Inference rules for Intensional equality
-
Formation: \(\frac{\Gamma \vdash A \hspace{1em} \Gamma \vdash a {:} A \hspace{1em} \Gamma \vdash a' {:} A} {\Gamma \vdash a ≃_A a'}\)
-
Introduction: \(\frac{\Gamma \vdash A \hspace{1em} \Gamma \vdash a {:} A} {\Gamma \vdash \refl {:} a ≃_A a}\)
-
Elimination: \(\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)}\)
-
Computation: \(\J(x, \refl_x, d) ≡ d {:} P(x, \refl_x)\)
I.C. Homotopy Type Theory
-
a type $A$ is abstractly seen as a topological space whose points are its objects
-
if $x, y: A$, $x ≃_A y$ represents the paths from $x$ (start point) to $y$ (end point).
-
given two parallel paths $p, q : x ≃A y$, a path $r : p ≃{x≃_A y} q$ corresponds to a homotopy/**2-path** between $p$ and $q$.
-
$r ≃{p ≃{x ≃_A y} q} s$ is the type of **3-paths**, and so on…
-
The tower comprised of these paths, paths of paths, paths of paths of paths, … arising from $A$ forms an $ω$-groupoid
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!
II. Weak $ω$-groupoids
Comparison of structures and laws of different algebraic structures
| Monoids | Categories | Higher Categories | Strict $𝜔$-Groupoids | |
|---|---|---|---|---|
| Carrier set/Underlying set | Sets | Multigraphs | Globular Sets | Globular Sets |
| Structure | Binary operation, Neutral element | Composition, Identity morphisms | Compositions, Identity morphisms | Compositions, Identity morphisms, Inverse elements |
| Laws | Associativity, Unit law | Associativity, Unit law | Associativity, Unit law, Interchange law | Associativity, Unit law, Interchange law, Inverse law |
- 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 $n∈ℕ$:
Intuition
- the points (\bullet) are members of (G_0)
- (a, b∈ G_1)
- (θ ∈ G_2)
- (s(θ) ≝ a)
- (t(θ) ≝ b)
$\begin{cases}
s(a) = s(b)
t(a) = t(b)
\end{cases}\quad$ i.e.: $\quad \begin{cases}
s(s (𝜃)) = s(t (𝜃))
t(s (𝜃)) = t(t (𝜃))
\end{cases}$
All sources and their corresponding targets are parallel.
For all (n∈ℕ^\ast, \; a, b:G_{n-1}), $G_n(a, b) ≝ \lbrace f∈G_n \mid s (f) = a \text{ and } t (f) = b\rbrace$
The elements of (G_n) are called (n)-arrows.
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 (𝜔)-groupoids
Let (G ≝ \bigsqcup\limits_{n≥0} G_n) be a strict (𝜔)-groupoid.
*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.
Structure of (G_n)
| Identity: | [{\rm id}^n (_ ) : \prod\limits_{a: G_{n-1}} G_n(a, a)] |
| Inverse: | [{\rm inv}^n (_ , _ ) : \prod\limits_{a, b: G_{n-1}} G_n(a, b) ⟶ G_n(b, a)] |
There are $n$ different types of compositions in (G_n): $\scol_1^n, \, \ldots, \, \scol_n^n$.
Let (1 ≤ i < n).
| Horizontal Composition (along the (i)-arrows) | Vertical Composition (along the (n)-arrows) | |
|---|---|---|
| \(\; \\ \scol^n_i: \prod\limits_{x, x', x'': G_0}\prod\limits_{\substack{f, f': G_i(x, x') \\ g, g': G_i(x', x'')}} \\ G_n(f, f') × G_n(g, g') ⟶ G_n(f \,\scol_i^i\, g, \, f' \scol_i^i g') \\\) | \(\; \\ \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'') \\\) | |
| \(\; \\ \cfrac{𝛼:G_i(x, x')\qquad 𝛼': G_i(x', x'')}{𝛼 \scol_i^n 𝛼': G_i(x, x'')} \\\) | \(\; \\ \cfrac{𝛼:G_n(f, f') \qquad 𝛼': G_n(f', f'')}{𝛼 \scol_n^n 𝛼': G_n(f, f'')} \\\) | |
<div class="xypic-block" style="height:400px; width:600px">  </div> |
<div class="xypic-block" style="height:400px; width:600px">  </div> |
Laws of (G_n)
| Identity ((i)): (x:G_i) | <div class="xypic-block" style="height:200px; width:600px"> </div> |
| Composition ((i < j)): the points (x, x’, x’’ : G_i), the simple arrows (f, g : G_j) | <div class="xypic-block" style="height:150px; width:600px">  </div> |
| Identity Laws ((i<j)): the points (x, x’ : G_i), the simple arrow (f : G_j) | Left: <div class="xypic-block" style="height:400px; width:600px"> </div> Right: idem |
Associativity law ((i < j)): the points (x, x’, x’’, x’’’ : G_i), the simple arrows (f, g, h : G_j)
Interchange law ((i < j < k)): the points (x, x’, x’’ : G_i), the simple arrows (f, f’, f’’, g, g’, g’’ : G_j), the double arrows (𝛼, 𝛼’, 𝛽, 𝛽’ : G_k)
Weak (𝜔)-groupoids: handmade partial construction
(G_1)
- Identity: [{\rm id}^1 (_ ) : \prod\limits_{a: G_0} G_1(a, a)]
- Inverse: [{\rm inv}^1 (_ , _ ) : \prod\limits_{a, b: G_0} G_1(a, b) ⟶ G_1(b, a)]
- Composition: [\scol^11 (_ , _ , _ ) : \prod\limits{a, b, c: G_0} G_1(a, b) × G_1(b, c) ⟶ G_1(a, c)]
(G_2)
- Identity: [{\rm id}^2 (_ ) : \prod\limits_{f: G_1} G_2(f, f)]
- Inverse: [{\rm inv}^2 (_ , _ ) : \prod\limits_{f, g: G_1} G_2(f, g) ⟶ G_2(g, f)]
- Horizontal Composition (along the (1)-arrows):
- Vertical Composition (along the (2)-arrows):
- Associativity along the (1)-arrows}: [𝛼^11 (_ , _ , _ ) : \prod\limits{x, x’, x’’, x’’’: G_0} \prod\limits_{\substack{f: G_1(x, x’) \ g: G_1(x’, x’’) \ h: G_1(x’’, x’’’)}} G_2((f \scol_1^1 g) \scol_1^1 h, \; f \scol_1^1 (g \scol_1^1 h))]
“Laws” that have become structure
-
Left identity “law”: [𝜆^1 (_ ) : \prod\limits_{f: G_1} G_2(({\rm id}^1_{s f} \scol_1^1 f), \; f)]
-
Right identity “law”: [𝜌^1 (_ ) : \prod\limits_{f: G_1} G_2((f \scol_1^1 {\rm id}^1_{t f}), \; f)]
-
Left inverse “law”: [l^1 (_ ) : \prod\limits_{f: G_1} G_2(({\rm inv}^1{sf, tf}(f) \scol_1^1 f), \; {\rm id}^1{t f})]
-
Right inverse “law”: [r^1 (_ ) : \prod\limits_{f: G_1} G_2((f \scol_1^1 {\rm inv}^1{sf, tf}(f)), \; {\rm id}^1{s f})]
(G_3), and so on…
At level (3), in addition, we have to take into account
-
the interchange law between the 2-arrows and the 1-arrows: [𝛼^12 : \prod\limits{x, x’: G_0} \prod\limits_{f, f’, f’’, f’’’: G_1(x, x’)} \prod\limits_{\substack{α: G_2(f, f’) \ β: G_2(f’, f’’) \ γ: G_2(f’’, f’’’)}} G_3((α \scol_2^2 β) \scol_2^2 γ, \; α \scol_2^2 (β \scol_2^2 γ))]
-
the different compositions (\scol_1^3, \scol_2^3, \scol_3^3)
-
the associativity along the (2)-arrows: [𝛼^12 : \prod\limits{x, x’: G_0} \prod\limits_{f, f’, f’’, f’’’: G_1(x, x’)} \prod\limits_{\substack{α: G_2(f, f’) \ β: G_2(f’, f’’) \ γ: G_2(f’’, f’’’)}} G_3((α \scol_2^2 β) \scol_2^2 γ, \; α \scol_2^2 (β \scol_2^2 γ))]
-
etc…
But that’s not it!
Coherence laws in $G_3$:
Equations between elements of $G_1$ 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 $G_1$, which are related as follows:
We impose a coherence law - the 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 (𝔹):
\[\begin{align*} \qquad&\cfrac{}{\bullet ⊢ \star}\quad\text{(Base type)}\\ \\ \qquad&\cfrac{Γ ⊢ x, y : A}{Γ \vdash x ≃ y}\quad\text{(Equality rule)}\\ \\ \qquad&\cfrac{\isContr Γ \qquad Γ ⊢ A}{Γ \vdash \coh_A^Γ : A}\quad\text{(Coherence rule)} \end{align*}\]where (\isContr) (which stands for is contractible) is inductively defined as follows:
\[\begin{align*} &\isContr (\bullet.\star) \\ &\cfrac{\isContr Δ \qquad Δ ⊢ x: A}{\isContr Δ.(y:A).(p: x≃y)} \end{align*}\]The intuition behind is that
-
the elements of the base type (\star) correspond to the elements of the set (G_0) of the underlying globular set of the weak (ω)-groupoid.
-
if (x, y: \star) the elements of (x ≃ y) are the 1-arrows of (G_1(x, y))
-
if (x, y: \star) and (f, g: x ≃ y), the elements of (f ≃ g) are those of (G_1(f, g))
-
and so on…
a context (Γ ≝ \bullet.(x \; y:\star).(f \; g : x ≃ y).(α : f ≃ g)) will be depicted as
A context is contractible if it can be “reduced to a point”, by contracting along the arrows.
Example
- the context (Γ ≝ \bullet.(x \; y \; z \; t:\star).(f : x ≃ y).(g : y ≃ z).(h : y ≃ t)) is contractible
- but the context (Γ’ ≝ \bullet.(x \; y \; z \; t:\star).(f : x ≃ y).(g : y ≃ z).(h \; i : y ≃ t)) is not:
because of the hole between (y) and (t) (we cannot contract (y) and (t)).
But if the hole between (y) and (t) is filled by a 2-arrow, like in (Γ’’ ≝ \bullet.(x \; y \; z \; t:\star).(f : x ≃ y).(g : y ≃ z).(h \; i : y ≃ t).(α ≃ h \; i))
then it becomes contractible.
Example: the associativity law along the (1)-arrows.
Let (x, y, z, t : \star, \; f : x≃y, \; g: y≃z, \; h: z≃t) and (Γ_{x, y, z, t} ≝ \bullet.(x \; y \; z \; t : \star).(f : x ≃ y).(g : y ≃ z).(h : z ≃ t))
First, how to define composition along the (1)-arrows?
As
- the context (Γ_{x, y, z, t}) is contractible
- and (Γ_{x, y, z, t} ⊢ x ≃ z) (since (Γ_{x, y, z, t} ⊢ x, z : \star))
(f \scol_1^1 g : x ≃ z) can be defined in (Γ_{x, y, z, t}) as (\coh_{x ≃ z}^{Γ_{x, y, z, t}})
Idem for the other compositions.
Now, there exists a [𝛼^1(f, g, h) : (f \scol_1^1 g) \scol_1^1 h ≃ f \scol_1^1 (g \scol_1^1 h)]
in (Γ_{x, y, z, t}), since (Γ_{x, y, z, t}) is contractible and (Γ_{x, y, z, t} ⊢ (f \scol_1^1 g) \scol_1^1 h ≃ f \scol_1^1 (g \scol_1^1 h)))!
III. Categories with Families
a category $𝒞$ is given by:
-
Structure:
-
Objects: a class of objects, denoted $\vert 𝒞 \vert$
-
Arrows: for each pair of objects $X, Y : \vert 𝒞\vert$, a “collection” of arrows (or morphisms) from $X$ to $Y$ denoted by $\Hom_𝒞(X, Y)$, or $𝒞(X, Y)$.
For each $f ∈ 𝒞(X, Y)$,
- $f ∈ 𝒞(X, Y)$ is denoted by $f: X ⟶ Y$ or $X \overset{f}{⟶} Y$
-
$X$ is the domain of $f$, $Y$ its codomain
-
Composition: for each pair of morphisms $f: X ⟶ Y$ and $g: Y ⟶ Z$, a composite arrow $g \circ f: A ⟶ C$ (and $f ; g : A ⟶ C$)
- Identity: for each object $A : \vert 𝒞 \vert$, an identity morphism $\id_X : A ⟶ A$
-
-
Laws:
- Associativity of composition: for each $f: X ⟶ Y, g: X ⟶ Z, h: Z ⟶ T$, \(f \circ (g \circ h) = (f \circ g) \circ h\)
- Unit law: for each $f: X ⟶ Y$, $\id_Y \circ f = f \circ \id_X$
Dual Category
- The dual category $𝒞^{op}$ of a category $𝒞$:
-
has the same objects as $𝒞$, and all of its arrows are “turned around”: \(f: X ⟶ Y \text{ in } 𝒞 ⟺ f^\ast: Y ⟶ X \text{ in } 𝒞^{op}\)
Functors
Let $𝒞, 𝒟$ be two categories.
a (covariant) functor $F: 𝒞 ⟶ 𝒟$ from $𝒞$ to $𝒟$ is a mapping such that:
-
for each object $X : \vert 𝒞 \vert$ in $𝒞$, $F(X)$ is an object in $𝒟$
-
for each morphism $f : X ⟶ Y$ in $𝒞$, $F(f) : F(X) ⟶ F(Y)$ (also written $Ff$) is a morphism from $F(X)$ to $F(Y)$ in $𝒟$
-
Preservation of composition: $F(g∘f)=F(g)∘F(f)$ for all morphisms $f:X ⟶ Y, \; g:Y ⟶ Z$ in $𝒞$.
-
Preservation of identity: $F(\id_X)=\id_{F(X)}$ for each object $X : \vert 𝒞 \vert$ in $𝒞$
Initial and terminal objects
- An object $\mathbb{0}$ (resp. $\mathbb{1}$) in a category $𝒞$ is initial (resp. terminal):
-
if for every object $X : \vert 𝒞\vert$, there exists a unique arrow from $\mathbb{0}$ to $X$ (resp. from $X$ to $\mathbb{1}$).
Slice and coslice categories
Let $𝒞$ be a category and $X : \vert 𝒞 \vert$ an object of $𝒞$.
The slice category $𝒞/X$ is described as follows:
- An object of $𝒞/X$ is a pair $(A, f)$ where $A : \vert 𝒞 \vert$ and $f : A ⟶ X$ in $𝒞$.
- An arrow of $𝒞/X$ from $(A, f)$ to $(B, g)$ is an arrow $h: A ⟶ B$ such that $f = g \circ h$
The coslice category $X\backslash 𝒞$ is the dual category of $𝒞/X$.
Category of elements
Let $F: 𝒞 ⟶ \Set$ be a functor.
The category of elements $\int^𝒞 F$ is described as follows:
- An object of $\int^𝒞 F$ is a pair $(A, a)$ where $A : \vert 𝒞 \vert$ and $a ∈ F(A)$.
- An arrow of $\int^𝒞 F$ from $(A, a)$ to $(B, b)$ is an arrow $h: A ⟶ B$ such that $Ff(a) = b$
a Category with Families (abbreviated CwF) is given by:
- a category (𝒞), with a terminal object (\bullet) (the empty context)
- a functor [\Ty : 𝒞^{\,\op} ⟶ \Set]
-
a functor from the category of elements of (\Ty): [\Tm : \bigg(\int_𝒞 \Ty \bigg)^{\,\op} ⟶ \Set]
-
Universal property of context extension: for each (Γ : 𝒞, \; A : \Ty (Γ)), the following functor from the slice category (𝒞/Γ) [\begin{cases} (𝒞/Γ)^{\op} &⟶ \Set
(Δ, σ) &⟼ \Tm\big(Δ, \Ty(σ)(A)\big) \end{cases}]is represented by an object ((Γ.A, π_A)), which roughly means that:
for each context morphism $σ : ∆ ⟶ Γ$ and type $A : \Ty(Γ)$, there is a “natural” (it does not depend on the variable $(Δ, σ)$) isomorphism:
\[\begin{aligned}[t] \Hom_{𝒞/Γ}((Δ, σ), (Γ.A, π_A)) & \qquad ≃ \qquad \Tm(Δ, \underbrace{\Ty(σ)(A)}_{\text{denoted by } A[σ]}) \end{aligned}\]
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: $\CwFB$ (resp. $\CwFId$) has an initial object $𝔹$ (resp. $𝕊^{\Id}_\star$).
A Brunerie globular weak $ω$-groupoid is a weak CwF-morphism from $𝔹$ to $\Set$
To show that types form Brunerie globular weak $ω$-groupoids, we proceed by demonstrating that there exist CwF-morphisms
\[𝔹 \overset{Φ}{⟶} 𝕊^{\Id}_\star \overset{F_A}{⟶} 𝕊 \overset{𝕊(\bullet, \_)}{⟶} \Set\]whose composition constitute the Brunerie globular weak $ω$-groupoid associated with the terms of a given type $A$.
