More Tiny Thoughts
I'm pretty happy with this line of thinking about internalized parametricity in a relatively lightweight modal type theory,
and consequently of course I start wondering if it's all been done already, like maybe it's
somehow latent in old Bernardy-Moulin work and I missed it$\ldots$ Dunno, wouldn't be the first time something like that's happened.
Anyway I find this particular presentation easy to wrap my head around, so that's something.
It looks like if you just set up the type theory in the right way,
which has a type operator $\pp_A M$ whose inhabitants are elements of the fiber of $\surd A$ lying over $M$,
you can simply code up isomorphisms that unpack the meaning of parametricity type-by-type:
\[ \pp_{A \to B}f \cong ((a : \lax A) (a' : \pp_A a) \to \pp_B(f\ (\elax a)))\]
expresses
a function is parametric if it maps parametric things to parametric things
and
\[ \pp_\rtype A \cong \lax (A \to \rtype) \]
expresses
a type is good to the extent that it is equipped with a unary relation
I find it quite pleasant that we don't have to axiomatize thes isomorphisms, and so we can compute with them.
Recap
I want to set up a type theory with four kinds of things going on in the context, normal assumptions $x : A$,
weak assumptions $x \div A$, strong assumptions $x :: A$, and a "key" $\star$ which may or may not be present in the context,
but which is propositional and has no interesting content. "Multiple copies" of $\star$ in the context are considered to be equivalent
to just one. $\Gamma^\oplus$ promotes all normal assumptions to strong (and makes any
sequent provable in $\Gamma^\oplus$ if $\star \in \Gamma$),
$\Gamma^\ominus$ demotes all normal assumptions to weak (and deletes the key, if any),
and both of them leave all other hypotheses alone. Normal and
strong variables are always usable, but weak variables are only usable if a key is currently in the context.
We can define a few modal operators $\lax$, $\surd$, and $\blat$, all special cases of things I found in the literature.
The operator $\surd$ is "box"-like, comonadic. We have $\surd A \prov A$ for example. The other two are "circle"-like, monadic. We have
$A \prov \lax A$ and $A \prov \blat A$, for example.
\[
{
\Gamma, \star \prov A : \rtype
\over
\Gamma \prov \lax A : \rtype
}
\qquad
{
\Gamma, \star \prov M : A
\over
\Gamma \prov \ilax\ M : \lax A
}
\qquad
{
\Gamma \prov M : \lax A \qquad \star \in \Gamma
\over
\Gamma \prov \elax\ M : A
}
\]
\[
{
\Gamma^\ominus \prov A : \rtype
\over
\Gamma \prov \surd A : \rtype
}
\qquad
{
\Gamma^\ominus \prov M : A
\over
\Gamma \prov \isurd\ M : \surd A
}
\qquad
{
\Gamma, \star \prov M : \surd A
\over
\Gamma \prov \esurd\ M : A
}
\]
\[
{
\Gamma^\oplus \prov A : \rtype
\over
\Gamma \prov \blat A : \rtype
}
\qquad
{
\Gamma^\oplus \prov M : A
\over
\Gamma \prov \iblat\ M : \blat A
}
\qquad
{
\Gamma^\ominus \prov M : \blat A
\over
\Gamma \prov \eblat\ M : A
}
\]
These are contrived to be in an adjoint sequence $\lax \dashv \surd \dashv \blat$.
Fiber Types
Much like it's useful to define a path type indexed by its endpoints, it looks like it simplifies
a lot of calculations if I explicitly define the type which is the fiber in $\surd A$ lying over a particular
point in $\lax A$ along the canonical map $\surd A \to \lax A$, which is given by
\[ x : \surd A \prov \ilax (\esurd x) : \lax A\]
We do this by defining a type $\pp_A M$, where $\pp$ is meant to evoke "parametric".
An inhabitant of $\pp_A M$ is a witness that $M$ is a "good", "parametric", "special", "in-the-relation" element of the type $A$.
\[
{
\Gamma^\ominus \prov A : \rtype\qquad \Gamma, \star \prov M : A
\over
\Gamma \prov \pp_A M : \rtype
}
\]
\[
{
\Gamma^\ominus \prov M : A
\over
\Gamma \prov \{ M\} : \pp_A M
}
\qquad
{
\Gamma, \star \prov M : A \qquad \Gamma^\oplus, \star \prov N : \pp_A M
\over
\Gamma \prov M \tri N : A
}
\]
Computation
The computation rules for this type are as follows. We have a $\beta$-law
\[ M \tri \{N\} \equiv_{\pp\beta } N \]
that says that intro followed by elim can be reduced.
And we have an $\eta$ law that says that any term $N$ of type $\pp_A M$ can be expanded:
\[ N \equiv_{\pp \eta} \{M \tri N\} \]
Furthermore, we say that whenever we have a term $M \tri N$ in a context where $\star$ exists, then
the eliminator reduces to its {\em first} component, and we call this "$\star$-reduction":
\[ \star \prov M \tri N \equiv_{\pp \star} M \]
Fiber types and $\surd$
The type $\pp_A M$ is equiexpressive with $\surd$; we can derive one from the other. Exercise: show that
for any $\Gamma^\ominus \prov A : \rtype$ and $\Gamma, h\prov M : A$ that
\[\pp_A M \cong (a : \surd A) \x (\esurd a \equiv M)\]
(a fiber is the total space restricted to the preimage of the basepoint)
\[\surd A \cong (x : \lax A) \x \pp_A (\elax x)\]
(the total space is the sum of all fibers)
However I think using the definitional fiber type saves me a bunch of headaches manipulating propositional equality.
A Theorem for Function Types
Now we can, in some sense, derive what the parametricity property is at function types, by coding up an explicit isomorphism.
Concretely, we claim we can write a program to inhabit
\[ \pp_{A \to B}f \cong ((a : \lax A) (a' : \pp_A a) \to \pp_B(f\ (\elax a)))\]
for any $\Gamma$ and $\Gamma, \star \prov A: \rtype$ and $\Gamma, \star \prov B : \rtype$ and $\Gamma, \star \prov f: A \to B$.
Let's unpack what this type is saying. We read $\lax$ (or, what's the same, existing in a context with $\star$ present)
as generally carrying the intuition of the adjectives "raw", "underlying".
For any $f$ a raw function $A$ to $B$, we claim two things are equivalent.
On the one hand, $\pp_{A \to B} f$ is to be read as "$f$ actually is a parametric function $A$ to $B$".
On the other hand, we have a more specific prescription of what it means for $f$ to be parametric: for any $a$ that
is an underlying value of type $A$, for any $a'$ that is a witness that $a$ is parametric, then $f$ applied to $a$
is parametric.
Forward Direction
$\mathsf{fore} : (f' : \pp_{A \to B}f ) (a : \lax A) (a' : \pp_A a) \to \pp_B(f\ (\elax a)) $
$\mathsf{fore}\ f'\ a\ a' = \{( f \tri f')\ (\elax a \tri a') \}$
To build this term we first descend through the $\pp$-introduction expression $\{ \dash\}$.
This makes our whole context temporarily inaccessible. However, in both of the arguments
of the $\pp$-eliminator $\tri$, we get back a key to unlock them, allowing us to refer
to underlying data like $f$ and $\elax a$, and attach parametricity witnesses $f'$ and $a'$ to them.
Backward Direction
$\mathsf{back} : (k : (a : \lax A) (a' : \pp_A (\elax a)) \to \pp_B(f\ (\elax a))) \to \pp_{A \to B}f $
$\mathsf{back} = \{ \lambda \bar a . (f\ \bar a \tri k\ (\ilax \bar a)\ \{\bar a\})\} $
To build this term we also start by descending through $\{\dash\}$ to build a parametricity witness.
Then we abstract over $\bar a : A$, followed by a parametricity elimination. The parametricity
fact we eliminate on comes from $k$. When we supply $k$ with $\ilax \bar a$ as its first argument, we get
\[ k\ (\ilax \bar a) : (a' : \pp_A (\elax (\ilax \bar a))) \to \pp_B(f\ (\elax (\ilax \bar a)))\]
which $\beta$-reduces to
\[ k\ (\ilax \bar a) : (a' : \pp_A \bar a) \to \pp_B(f\ \bar a)\]
The reason we can still access $\bar a$ inside $\{ \bar a\}$ (which expression supplies the $a'$ argument to $k$)
is that we actually have the strong hypothesis $\bar a :: A$ because the second argument to $\tri$ promotes
its context.
First Zigzag
We can check $\mathsf{fore} \o \mathsf{back}$ is the identity.
\[\begin{array}{l}
\mathsf{fore}\ (\mathsf{back}\ k) \ a\ a' \\
= \{( f \tri (\mathsf{back}\ k))\ (\elax a \tri a')\}\\
= \{( f \tri \{ \lambda \bar a . (f\ \bar a \tri k\ (\ilax \bar a)\ \{\bar a\})\})\ (\elax a \tri a')\}\\
\equiv_{\pp \beta} \{( \lambda \bar a . (f\ \bar a \tri k\ (\ilax \bar a)\ \{\bar a\}))\ (\elax a \tri a')\}\\
\equiv_{\to \beta} \{f\ \bar a \tri k\ (\ilax (\elax a \tri a'))\ \{(\elax a \tri a')\}\}\\
\equiv_{\pp \eta} k\ (\ilax (\elax a \tri a'))\ \{(\elax a \tri a')\}\\
\equiv_{\pp \eta} k\ (\ilax (\elax a \tri a'))\ a'\\
\equiv_{\pp \star} k\ (\ilax (\elax a ))\ a'\\
\equiv_{\lax \eta} k\ a\ a'\\
\end{array}\]
Second Zigzag
We can check $\mathsf{back} \o \mathsf{fore}$ is the identity.
\[\begin{array}{l}
\mathsf{back}\ (\lambda a.\lambda a'.\mathsf{fore}\ f'\ a\ a') \\
= \mathsf{back}\ (\lambda a.\lambda a'. \{( f \tri f')\ (\elax a \tri a') \}) \\
= \{ \lambda \bar a . (f\ \bar a \tri ((\lambda a.\lambda a'. \{( f \tri f')\ (\elax a \tri a') \}))\ (\ilax \bar a)\ \{\bar a\})\} \\
\equiv_{\to \beta} \{ \lambda \bar a . (f\ \bar a \tri \{( f \tri f')\ (\elax (\ilax \bar a) \tri \{\bar a\}) \} )\} \\
\equiv_{\pp \beta} \{ \lambda \bar a . ( ( f \tri f')\ (\elax (\ilax \bar a) \tri \{\bar a\}) )\} \\
\equiv_{\pp \beta} \{ \lambda \bar a . ( ( f \tri f')\ \bar a )\} \\
\equiv_{\to \eta} \{ f \tri f' \} \\
\equiv_{\pp \eta} f' \\
\end{array}\]
A (Sketch of a) Theorem for the Universe
Let's recall the glue type from last time
\[
\Gamma, \star \prov A : \rtype \qquad \Gamma^\oplus, \star, x : A \prov B : \rtype
\over
\Gamma \prov \gg(x : A). B : \rtype
\]
\[
\Gamma, \star \prov M : A \qquad \Gamma^\oplus, \star \prov N : [M/x]B
\over
\Gamma \prov \pair M N : \gg(x : A). B
\]
\[
{\Gamma \prov M : \gg(x : A). B
\over
\Gamma, \star \prov M. 1 : A}
\qquad
{\Gamma \prov M : \gg(x : A). B
\over
\Gamma^\oplus, \star \prov M. 2 : [M. 1/x]B}
\]
And try to show, for any $\Gamma, \star \prov A : \rtype$, that we have an isomorphism
\[ \pp_\rtype A \cong \lax (A \to \rtype) \]
Morally, this is saying:
"a witness that an inhabitant $A$ of $\rtype$ belongs to the parametricity relation is exactly a family $A \to\rtype$".
The maps are:
$\mathsf{fore} : (p : \pp_\rtype A) \to \lax ( A \to \rtype)$
$\mathsf{fore}\ p = \ilax (\lambda a . \pp_{A \tri p }( a))$
$\mathsf{back} : (R : \lax ( A \to \rtype)) \to \pp_\rtype( A) $
$\mathsf{back}\ R = \{ \gg (x : A) . (\elax R)\ x\} $
First Zigzag
We can check $\mathsf{fore} \o \mathsf{back}$ is the identity.
\[\begin{array}{l}
\mathsf{fore}\ (\mathsf{back}\ R) \\
= \mathsf{fore}\ (\{ \gg (x : A) . (\elax R)\ a\}) \\
= \ilax (\lambda a . \pp_{A \tri \{ \gg (x : A) . (\elax R)\ x\} }( a)) \\
= \ilax (\lambda a . \pp_{ \gg (x : A) . (\elax R)\ x }( a)) \\
\end{array}\]
We expect this to equal $R$, so by extensionality, it suffices to show
for every $a : A$ that
\[ (\elax R)\ a = \pp_{ \gg (x : A) . (\elax R)\ x }( a)\]
I think this can be done with univalence and
\[\begin{array}{l}
\mathsf{fore_1} : (\elax R)\ a \to \pp_{ \gg (x : A) . (\elax R)\ x }( a)\\
\mathsf{fore_1}\ z = \{\mpair a z\} \\
\mathsf{back_1} : \pp_{ \gg (x : A) . (\elax R)\ x }( a) \to (\elax R)\ a\\
\mathsf{back_1}\ w = (a \tri w).2
\end{array}\]
Second Zigzag
We can check $\mathsf{fore} \o \mathsf{back}$ is the identity.
\[\begin{array}{l}
\mathsf{back}\ (\mathsf{fore}\ p) \\
= \mathsf{back} (\ilax (\lambda a . \pp_{A \tri p }( a)))\\
= \{ \gg (x : A) . (\elax (\ilax (\lambda a . \pp_{A \tri p }( a))))\ x\} \\
\equiv_{\lax \eta } \{ \gg (x : A) . ( (\lambda a . \pp_{A \tri p }( a)))\ x\} \\
\equiv_{\to \beta } \{ \gg (x : A) . \pp_{A \tri p }( x)\} \\
\end{array}\]
I want this to be equal to $p : \pp_{\rtype} A$, so by extensionality, it would suffice to show
\[ A \tri p = \gg (x : A) . \pp_{A \tri p }( x)\]
I think this can be done with univalence and
\[\begin{array}{l}
\mathsf{fore_2} : A \tri p \to \gg (x : A) . \pp_{A \tri p }( x)\\
\mathsf{fore_2}\ z = \mpair{z}{\{z\}} \\
\mathsf{back_2} : (\gg (x : A) . \pp_{A \tri p }( x)) \to A \tri p \\
\mathsf{back_2}\ w = w.1 \tri w.2
\end{array}\]