A Proof-Irrelevant Tiny Object

Motivation

I was enjoying reading Mitchell Riley's "A Type Theory with a Tiny Object" the other day.

It describes a type theory where you have a type $\T$ where you get a sequence of three adjoint functors: \[ (\T \x \dash) \adjoint (\T \to \dash) \adjoint \sqrt{}\] It's kind of unusual in general that a type $\T$ should have a right adjoint to its function space like this; it's sometimes called an Amazing Right Adjoint.

Presheaf Category over the Arrow

I started wondering what would happen to the syntax of the type theory if we examined a special case of this situation; in particular the very special case where we're imagining the "intended model" being $\mathsf{Type}^{\bullet \to \bullet}$ and $\T$ is specifically the functor $0 \to 1$.

Mostly I was wondering; would it get simpler and nicer somehow?

In this setting, we're living inside a "big" type theory where every type is a function $f : A \to B$ from one "ordinary" type to another. Since $\T = 0 \to 1$, we can explicitly compute some of these functors:

The functor $\T \x \dash$ takes $f : A \to B$ to

the unique arrow $0 \to B$.

The functor $\T \to \dash$ takes $f : A \to B$ to

the identity $B \to B$.

The functor $\sqrt{}$ takes $f : A \to B$ to

the identity $A \to A$.

and in this special case there's an additional right adjoint to $\sqrt{}$, call it $U$;

The functor $U$ takes $f : A \to B$ to

the unique arrow $A \to 1$.

which makes for a very pleasing sequence of four adjoint functors.

Also in this setting $\T$ is a "mere proposition", i.e. its terms are "proof irrelevant". Any two functions into $\T$ are equal, despite it not being the terminal object of its category. So this is quite a special case!

Proof Irrelevance

Setting aside the functors $\sqrt{}$ and $U$, we can start exploring how Riley's system would react to just forcing $\T$ to be proof irrelevant. I think we can dispense with most of the context-locking mechanisms, and just keep track of whether each hypothesis "is locked" or not independently.

As a general warning, the following bit of the story is pretty sketchy and extremely mutually recursive and full of forward references.

In fact, what I want to do is start with the idea that there are two distinct languages syntactically, one of which is the "main" type theory, and another one is the shadow of that theory after we've assumed at least some term of type $\T$ exists. This "reduced" or "erased" type theory is going to look pretty much like ordinary dependent type theory, \[\begin{array}{rlcl} \textrm{Erased Contexts} & \Gamma_0 &\cc=& \cdot \celse \Gamma_0, x : A_0 \\ \textrm{Erased Types} & A_0 &\cc=& \cdots \\ \textrm{Erased Terms} & M_0 &\cc=& \cdots \end{array}\] and then the "main" type theory we care about has some extra features on top of normal dependent type theory: \[\begin{array}{rlcl} \textrm{Contexts} & \Gamma &\cc=& \cdot \celse \Gamma, x : A \celse \Gamma, x :: A_0 \\ \textrm{Types} & A &\cc=& \cdots \celse \T \\ \textrm{Terms} & M &\cc=& \cdots \end{array}\] This new context former $x :: A_0$ is analogous to the locking that Riley is doing; intuitively a variable $x :: A_0$ has a type something like $\T \to A_0$. It's "locked behind" needing to provide a term of type $\T$. This is how we should eventually be able to give formation and introduction rules for $\sqrt{}$, by judgmentally applying its left adjoint $\T \to \dash$ to the context.

But before we even get to that point, we can think about how to even set up the context formation rule for $x :: A_0$. We posit: \[{\vdash \Gamma\ \ms{ctx} \qquad \Gamma^0 \vdash A_0 : \ms{type} \over \vdash (\Gamma, x \cc A_0)\ \ms{ctx}}\] Using an operation $\Gamma \mapsto \Gamma^0$ that we haven't defined yet, whose purpose is to take a "main" $\Gamma$ to an erased one. The idea is that to the extent that $x :: A_0$ is like $x : \T \to A_0$, the context in which $A_0$ makes sense is $\Gamma$ extended with a term of type $\T$, i.e. something like $\Gamma, t : \T$. This is morally what $\Gamma^0$ is supposed to be: the moment we assume a term of type $\T$ exists, various of things collapse. For example, assumptions $x :: A_0$ become ordinary assumptions $x : A_0$, because the obligation to come up with a term of type $\T$ to unlock them is now satisfied.

Here's a definition of a few of the more interesting cases of erasure:

$(\Gamma, x : A)^0 = (\Gamma^0, x : A^0)$
$(\Gamma, x \cc A_0)^0 = (\Gamma^0, x : A_0)$
$(x\llbracket t \rrbracket)^0 = x$
$(x)^0 = x$

This mentions a term former we haven't discussed yet. There is a special term former for locked variables, whose typing rule is: \[{\Gamma \vdash t : \T \qquad x \cc A_0 \in \Gamma \over \Gamma \vdash x\llbracket t \rrbracket : A_0[t \star \Gamma]}\] We can 'unlock' locked variables by actually providing a term of type $\T$. We impose definitional proof irrelevance of these terms: $x\llbracket t \rrbracket \equiv x\llbracket t' \rrbracket$ for all $t, t'$. This evidence is in fact erased by the erasure we defined immediately above.

The Rehydrating Substitution

The immediately preceding variable typing rule introduces another piece of syntax, $[t \star \Gamma]$, which corresponds to a substitution principle that can hoist expressions (terms, types, contexts) from erased back to unerased, provided a term $t$. As a term function, this consists mostly of boring homomorphism cases like \[ (M N)[t\star \Gamma] = M[t\star \Gamma]\ N[t\star \Gamma])\] \[ (\lambda x . M)[t\star \Gamma] = \lambda x . (M[t\star \Gamma])\]

The most interesting cases are when the subject of the substitution is a variable: \[x[t \star \Gamma] = \begin{cases} x & \text{if } x : A \in \Gamma \\ x\llbracket t \rrbracket & \text{if } x \cc A \in \Gamma \end{cases}\] What's happening here is that if $x$ was a locked variable originally, we put back in the "key" term $t$.

Correctness Lemmas

Having defined a bunch of things mutually recursively, let's now try to prove some of them make sense.

Lemma: Rehydrating substitution followed by erasure is the identity.
$A_0 \equiv (A_0[t \star \Gamma])^0$
$M_0 \equiv (M[t \star \Gamma])^0$

Proof:
The interesting case is the variable. Suppose $M_0 = x$ for $x ::A_0 \in \Gamma$. Then $ M[t \star \Gamma] = x\llbracket t \rrbracket$ and $(M[t \star \Gamma])^0 = x$ as required. $\cqed$

Lemma: Erasure followed by the rehydrating substitution is the identity. Suppose we have a term $\Gamma \vdash t : \T$. Then:
if $\Gamma \vdash A : \ms{type}$, then $A \equiv A^0[t \star \Gamma]$
if $\Gamma \vdash M : A$, then $M \equiv M^0[t \star \Gamma]$

Proof:
The interesting case is the variable. Suppose $M = x\llbracket t' \rrbracket$ and $\Gamma = \Gamma_1, x \cc A_0, \Gamma_2$. Then we have \[{\Gamma \vdash t' : \T \qquad x \cc A_0 \in \Gamma \over \Gamma \vdash x\llbracket t' \rrbracket : A_0[t \star \Gamma]}\] We observe that the erasure is $M^0 = x$, and the erasure followed by rehydrating is $M^0[t \star \Gamma] = x[t \star \Gamma] = x\llbracket t \rrbracket$. So our obligation is to prove $x\llbracket t' \rrbracket \equiv x\llbracket t \rrbracket$, but this is true by the definitional proof irrelevance we postulated. $\cqed$

Lemma: The rehydrating substitution is well-typed. \[{\Gamma \vdash t : \T \qquad \Gamma^0 \vdash A_0 : \ms{type} \over \Gamma \vdash A_0[t \star \Gamma] : \ms{type}}\] \[{\Gamma \vdash t : \T \qquad \Gamma^0 \vdash M_0 : A_0 \over \Gamma \vdash M_0[t \star \Gamma] : A_0[t \star \Gamma]}\]
Proof:
Again the variable cases are the interesting ones.

Suppose $M_0 = x$ and $\Gamma = \Gamma_1, x \cc A_0, \Gamma_2$. Then we have

$\Gamma \vdash t : \T \qquad \Gamma_1^0, x \cc A_0, \Gamma_2^0 \vdash x : A_0$

and we're trying to show

$\Gamma_1, x \cc A_0, \Gamma_2 \vdash x\llbracket t \rrbracket : A_0[t \star \Gamma]$

This follows immediately from the variable rule.

Suppose instead that $M_0 = x$ for $\Gamma = \Gamma_1, x : A, \Gamma_2$. Then we have

$\Gamma \vdash t : \T \qquad \Gamma_1^0, x : A^0, \Gamma_2^0 \vdash x : A^0$

and we must show

$\Gamma \vdash x : A^0[t \star \Gamma]$

For this it suffices to show $A \equiv A^0[t \star \Gamma]$, which we have by the previous lemma. $\cqed$

Lemma: Erasure is well-typed.
Proof:

if $\vdash \Gamma\ \ms{ctx}$, then $\vdash \Gamma^0\ \ms{ctx}$
if $\Gamma \vdash A : \ms{type}$, then $\Gamma^0 \vdash A^0 : \ms{type}$
if $\Gamma \vdash M : A$, then $\Gamma^0 \vdash M^0 : A^0$

Suppose we have

\[{\vdash \Gamma\ \ms{ctx} \qquad \Gamma^0 \vdash A_0 : \ms{type} \over \vdash (\Gamma, x \cc A_0)\ \ms{ctx}}\]

then we can show

\[{\vdash \Gamma^0\ \ms{ctx} \qquad \Gamma^0 \vdash A_0 : \ms{type} \over \vdash (\Gamma^0, x : A_0)\ \ms{ctx}}\]

Suppose $\Gamma = \Gamma_1, x :: A_0, \Gamma_2$, and $M = x\llbracket t\rrbracket$. Then we have \[{\Gamma \vdash t : \T \qquad x \cc A_0 \in \Gamma \over \Gamma \vdash x\llbracket t \rrbracket : A_0[t \star \Gamma]}\]

and we need to show $\Gamma^0 \vdash x : (A_0[t \star \Gamma])^0$, so we need $x : (A_0[t \star \Gamma])^0 \in \Gamma^0$, hence we need $(A_0[t \star \Gamma])^0 \equiv A_0$, but we have this by earlier lemma. $\cqed$

Defining the lock operation

Now I want to define an operation $\Gamma^🔒$ that takes a $\Gamma$ and makes everything in it locked behind the $::$ context-former. We define it as follows:

$(\cdot)^🔒 = \cdot$
$(\Gamma, x : A)^🔒 = (\Gamma^🔒, x \cc A^0)$
$(\Gamma, x \cc A_0)^🔒 = (\Gamma^🔒, x \cc A_0)$

If a hypothesis is already locked, don't do anything. Otherwise, lock it and erase the type.

Lemma: Locking then erasing is the same thing as erasing. \[(\Gamma^🔒)^0 \equiv \Gamma^0\]
Proof:

Case: Suppose we have $(\Gamma, x : A)$. \[((\Gamma, x : A)^🔒)^0 = (\Gamma^🔒, x \cc A^0)^0 = ((\Gamma^🔒)^0, x : A^0)\] \[ = (\Gamma^0, x : A^0) = (\Gamma, x : A)^0 \]

Case:Suppose we have $(\Gamma, x \cc A_0)$. \[((\Gamma, x \cc A_0)^🔒)^0 = (\Gamma^🔒, x \cc A_0)^0 = ((\Gamma^🔒)^0, x : A_0)\] \[ = (\Gamma^0, x : A_0) = (\Gamma, x :: A_0)^0 \]

Lemma: Locking is well-typed. If $\vdash \Gamma\ \ms{ctx}$, then $\vdash \Gamma^🔒\ \ms{ctx}$.
Proof:

Case: Suppose we have

\[{\vdash \Gamma\ \ms{ctx} \qquad \Gamma \vdash A : \ms{type} \over \vdash (\Gamma, x : A)\ \ms{ctx}}\]

then use the i.h. to get $\vdash \Gamma^🔒\ \ms{ctx}$, and the well-typedness of erasure to get $\Gamma^0 \vdash A^0 : \ms{type}$ and apply the previous lemma and the rule \[{\vdash \Gamma^🔒\ \ms{ctx} \qquad (\Gamma^🔒)^0 \vdash A^0 : \ms{type} \over \vdash (\Gamma^🔒, x \cc A^0)\ \ms{ctx}}\]

Case: Suppose we have

\[{\vdash \Gamma\ \ms{ctx} \qquad \Gamma^0 \vdash A_0 : \ms{type} \over \vdash (\Gamma, x \cc A_0)\ \ms{ctx}}\]

then use the i.h. to get $\vdash \Gamma^🔒\ \ms{ctx}$, and use the previous lemma and rule \[{\vdash \Gamma^🔒\ \ms{ctx} \qquad(\Gamma^🔒)^0 \vdash A_0 : \ms{type} \over \vdash (\Gamma^🔒, x \cc A_0)\ \ms{ctx}}\]

to finish. $\cqed$