[Nottingham Internship] Recursors put to the category theory test

5 minute read

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!

\[\newcommand{\rec}{\mathop{\rm rec}\nolimits} \newcommand{\ind}{\mathop{\rm ind}\nolimits} \newcommand{\inl}{\mathop{\rm inl}\nolimits} \newcommand{\inr}{\mathop{\rm inr}\nolimits} \newcommand{\Hom}{\mathop{\rm Hom}\nolimits}\]

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:

\[𝒞_{A,B}\Big((C, f), \; (D, g)\Big) ≝ \Hom_{𝒞_{A,B}} \Big((C, f), \; (D, g) \Big)\]

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:

\[\rec_{A×B}(C, f, \_ ):𝒞_{A,B}\Big((A×B, ( \_ , \_ ) ), \; (C, f)\Big)\] 
  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$:

\[\rec_{A×B}(C, f, (a, b)) ≡ f \; a \; b: C\]

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:

\[∀a: A,\; b: B, \; \rec_{A×B}(C, f,(a, b)) ≡ g((a, b)) \\ ⟹ \rec_{A×B}(C, f, \_ ) ≡ g\]

By the way:

\[\rec_{A×B}: \prod\limits_{C: {\cal U}} (A ⟶ B ⟶ C) ⟶ A×B ⟶ C\]

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

\[X: B' ⟶ Set\]

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

\[X: B' ⟶ {\cal U}\]

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$:

\[s((a,\, b)) ≡ \big((a, b)\;, \, \underbrace{f_2 \; a \; b}_{\rlap{≡ \; \underbrace{s_2}_{: \; \prod\limits_{p: A×B} C(p)} ((a, \, b))\,: \, C((a,b))}} \big): E\]

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:

\[\ind_{A×B}(C, \, f_2, \, \_ ): \prod\limits_{p: A×B} C(p)\]

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