[Nottingham Internship] Recursors put to the category theory test
Everything I’m about to write has been explained to me by Paolo Capriotti: many thanks to him!
We’ve seen recursors and inductive constructors last time, whose aim was basically to form new types.
The overall general patterns, with respect to a new type $T$, were:

for recursors:
\prod\limits_{C: {\cal U}} \boxed{\vphantom{\prod}\; ? \;} ⟶ \Big(T ⟶ C \Big) 
for inductive constructors:
\prod\limits_{C: T ⟶ {\cal U}} \boxed{\vphantom{\prod}\; ? \;} ⟶ \prod\limits_{x:T} C(x)
NB: Besides, it can be noted that recursors were, in each case, special cases of induction where the family $C$ is constant.
Yeah, that’s all fine and dandy, but how are we supposed to construct those constructors, generally speaking? And where do they even come from?
Paolo called to the rescue!
When Category Theory enters the scene
In order to understand where the constructors come from, we’ll stick to one example: the product type.
Product Type: $A×B$
Let’s assume $A, B: {\cal U}$ are two fixed types, in what follows.
Let $𝒞_{A,B}$ be the category whose

Objects are of the form:
(C, f), \text{ where } C: {\cal U} \text{ and } f: A ⟶ B ⟶ C 
Morphisms/Arrows are:
𝒞_{A,B} ≝ \big\lbrace h: C ⟶ D \mid \text{ for all } a: A, b:B, \quad h(f \; a \; b) = g \; a \; b\big\rbrace
Notation:
Recursor
Axiom:
$𝒞_{A,B}$ has an initial object $(A×B, ( \_ , \_ ) )$, i.e.: for all object $(C, f)$, there exists a unique morphism in $𝒞_{A,B}\Big((A×B, ( \_ , \_ ) ), \; (C, f)\Big)$
Let’s call this unique morphism, by any chance:
digraph {
rankdir=LR;
subgraph cluster_0 {
label="𝒞"
"A×B, (_, _)" > "C, f"[label="rec(C,f)"];
"A×B, (_, _)" > "D, g"[label="rec(D,g)"];
}
}
That is, for all $a:A, \; b:B$:
which is the computation/$𝛽$rule!
NB: In the general case, the recursor is required to be weakly initial, i.e. there’s no constraint of uniqueness. But in the case of product type, it happens to be initial (we have the uniqueness).
In the particular case of product type: the uniqueness principle/$𝜂$rule is enforced by the uniqueness hypothesis:
By the way:
which is exactly what we were after!
Induction
Preliminaries: fibrations
Before we adress the issue of inductive constructors, we shall dwell on the concept of fibrations.
Fibrations of sets
Let’s begin with fibrations of sets, to get a grasp of it.
 A fibration of sets:

it is just a function $p : E ⟶ B’$, usually represented (vertically) as
digraph { rankdir=TB; E > "B'"[label=" p"]; }
NB: $E$ stands for “étale” in French
What will particularly get our attention is what we call fibers:
 Fiber $X_b$:

A subset of $X_b ⊆ E$ which is an inverse image of a point $b ∈ B’$
digraph {
rankdir=TB;
subgraph cluster_0 {
label="E";
style="rounded";
dummy1 [style=invis]
X_b[shape=egg, style=filled];
dummy2 [style=invis]
}
subgraph cluster_1 {
label=" B'";
style=rounded;
dummy4 [style=invis];
b[shape=point xlabel="b "];
dummy5 [style=invis];
}
X_b > b[label=" p", color="black:black"];
}
So all the fibers form a family
But upon considering the family, the key point is that, instead of talking of the class of all sets, all the information lies in two simple sets and a function.
And reciprocally, if we’re given a family $(X_b)_{b∈B’}$ of disjoint sets, a fibration of sets can be retrieved, with

E ≝ \bigsqcup\limits_{b∈B'} X_b

p ≝ E ⟶ B', X_b \ni x \mapsto b
digraph {
rankdir=TB;
"E ≝ ⨆ X_b" > "B'"[label=" p"];
}
Fibrations of types
Back to types. This time, let’s suppose we’re given a family
Similarly, with

E :≡ \sum\limits_{b: B'} X_b

p :≡ (b, e) \mapsto b : E ⟶ B'
then
digraph {
rankdir=TB;
"E" > "B'"[label=" p"];
}
is a fibration associated with $X$
Fibration in $𝒞_{A, B}$
digraph {
rankdir=TB;
"(E, f)" > "(B', g)"[label=" 𝜋"];
}
is a fibration in $𝒞_{A, B}$ iff $𝜋: 𝒞_{A, B}\Big(\big(E, f\big), \big(B’, g\big)\Big)$ and
digraph {
rankdir=TB;
E > "B'"[label=" 𝜋"];
}
is a fibration
Towards the inductive constructor
 A section $s:𝒞_{A, B}\Big(\big(D, g\big), \big(C, f\big)\Big)$ of $𝜋: 𝒞_{A, B}\Big(\big(C, f\big), \big(D, g\big)\Big)$:

it is a right inverse of $𝜋$, i.e. $𝜋 \circ s = id_{(C, f)}$
In what follows, let
 $C : A×B ⟶ {\cal U}$
 $E :≡ \sum\limits_{p: A×B} C(p)$
Now the fun begins: let’s assume that
for each fibration $𝜋: 𝒞_{A, B}\Big(\big(E, f\big), \big(A×B, (\_ , \_ )\big)\Big)$ associated with $C$, there exists a section $s: 𝒞_{A, B}\Big(\big(A×B, (\_ , \_ )\big), \big(E, f\big)\Big)$ of $𝜋$
digraph {
rankdir=TB;
"(E, f)" > "(A×B, (_, _))"[label=" 𝜋"];
"(A×B, (_, _))" > "(E, f)"[label=" s"];
}
NB: with the notations of the section “Fibration of types”, we have now $B’ ≝ A×B$, and $X ≝ C$.
Let $𝜋: 𝒞_{A, B}\Big(\big(E, f\big), \big(A×B, (\_ , \_ )\big)\Big)$ be a fibration associated with $C$.
Hence:

$𝜋$ is a fibration associated with $C$:
\text{for all } \; p: A×B, \; c: C(p), \quad 𝜋((p, c)) :≡ p 
$𝜋$ is a morphism:
𝜋(f \; a \; b) ≡ (a, b)
Let $s ≝ (s_1, s_2)$, then:

$\underbrace{𝜋}_{\rlap{\text{first projection}}} \circ \, s ≡ id_{A×B}$:
s_1 ≡ id_{A×B} 
$s$ is a morphism:
s((a, b)) ≡ f \; a \; b :≡ (f_1 \; a \; b, \; f_2 \; a \; b): E
Thus, for all $a: A, \; b:B$:
As $s_2$ depends only on $C: {\cal U}$ and $f_2: \prod\limits_{x: A} \prod\limits_{y: B} C((x, y))$, it can be written as:
As a result:
\ind_{A×B}: \prod\limits_{C: A×B ⟶ {\cal U}} \bigg( \prod\limits_{x: A}\prod\limits_{y: B} C((x,y)) \bigg) ⟶ \prod\limits_{p: A×B} C(p)and
\ind_{A×B}(C, f_2, (a,b)) = f_2 \; a \; b
which is exactly what we wanted!
The same goes for the reverse: if you assume that you are given the inductive constructor, you can likewise show that each fibration $𝜋: 𝒞_{A, B}\Big(\big(E, f\big), \big(A×B, (\_ , \_ )\big)\Big)$ associated with $C$ has a section $s: 𝒞_{A, B}\Big(\big(A×B, (\_ , \_ )\big), \big(E, f\big)\Big)$.
Leave a comment