One More Type in the Tiny Type Theory
Continuing with the previous post, I can
define one more type constructor that I suspect to be important for constructing the backward direction of
\[\surd \rtype \cong (A : \T \to \rtype) \x (t : \T) (B : A\ t) \to \rtype \]
For that we would need to construct a genuine $\rtype$ in a context that looks like
\[ A \div \rtype, B \div A \to \rtype \]
Type Former
So my guess is we want a somewhat $\Sigma$-like type former, call it $\gg$ for "glue":
\[
\Gamma, \star \prov A : \rtype \qquad \Gamma^\oplus, \star, x : A \prov B : \rtype
\over
\Gamma \prov \gg(x : A). B : \rtype
\]
It glues together two types, one of which carries "downstairs" information, namely $A$, and the other lives "upstairs", namely "B". The interpretation of this back into
ordinary type theory is:
$(\gg(x : A). B)^* = A^*$
$\sem {\gg(x : A). B}(M^*) = [M^*/x^*]B^*$
Why are these well-typed? By induction hypothesis applying the translation
$\dash^*$ to the premises, we'd have
\[\Gamma^* \prov A^* : \rtype \tag{*}\]
\[(\Gamma^\oplus)^*, x^* : A^* \prov B^* : \rtype\]
We can reason that $(\Gamma^\oplus)^*$ is the same thing as $\sem \Gamma$, so we have
\[\sem \Gamma, x^* : A^* \prov B^* : \rtype\tag{**}\]
Showing
\[ \Gamma^* \prov (\gg(x : A). B)^* : \rtype\]
is just $(*)$, and then the obligation
\[ \sem \Gamma, y^* : (\gg(x : A). B)^* \prov \sem{\gg(x : A). B}(y^*) : \rtype\]
reduces to
\[ \sem \Gamma, y^* : A^* \prov [y^*/x^*] B^* : \rtype\]
and this is $(**)$ up to $\alpha$-equivalence.
Term Formers
Here's how I think we introduce $\gg$:
\[
\Gamma, \star \prov M : A \qquad \Gamma^\oplus, \star \prov N : [M/x]B
\over
\Gamma \prov \pair M N : \gg(x : A). B
\]
Here's how I think we eliminate $\gg$:
\[
{\Gamma \prov M : \gg(x : A). B
\over
\Gamma, \star \prov M\tri 1 : A}
\qquad
{\Gamma \prov M : \gg(x : A). B
\over
\Gamma^\oplus, \star \prov M\tri 2 : [M\tri 1/x]B}
\]
We say that these interpret as follows:
$(\pair M N)^* = M^*$
$\sem {\pair M N}^* = N^*$
$( M\tri 1)^* = M^*$
$\sem{M\tri 1} = \babort(☠)$
$( M\tri 2)^* = \sem M$
$\sem{M\tri 2} = \babort(☠)$
Let's check that these interpretations are well-typed.
Introduction
Applying $\dash^*$ to the premises we get
\[\Gamma^* \prov M^* : A^*\]
\[\sem \Gamma \prov N^* : [M^*/x^*]B^*\]
Applying $\sem\dash$ gives us nothing useful because $\star$ is present.
Downstairs we need
\[\Gamma^* \prov (\pair M N)^* : (\gg(x : A). B)^*\]
which computes to
\[\Gamma^* \prov M^* : A^*\]
which we have. Upstairs we need
\[\sem\Gamma \prov \sem{\pair M N} : \sem{\gg(x : A). B}((\pair M N)^*)\]
which computes to
\[\sem\Gamma \prov N^* : [M^*/x^*]B^*\]
which we also have.
First Projection
I.h. for $\dash^*$ on the premise gives
\[\Gamma^* \prov M^* : A^*\]
We need
\[(\Gamma^* \prov (M\tri 1)^* : A^* ) = (\Gamma^* \prov M^* : A^*)\]
and
\[(\sem{\Gamma, \star} \prov \sem{M\tri 1} : \sem A((M\tri 1)^*)) =
(\sem \Gamma,☠ : 0 \prov \babort(☠) : \sem A(M^*))\]
so we're good.
Second Projection
I.h. for $\sem\dash$ on the premise gives
\[\sem \Gamma \prov \sem M : \sem{\gg(x : A). B}(M^*) \]
in other words
\[\sem \Gamma \prov \sem M : [M^*/x^*]B^* \]
We need
\[((\Gamma^\oplus, \star)^* \prov (M\tri 2)^* : ([M\tri 1/x]B)^* ) =
(\sem \Gamma \prov \sem M : [M^*/x^*]B^* ) \]
and
\[(\sem{\Gamma^\oplus, \star} \prov \sem{M\tri 2} : \sem{[M\tri 1/x]B}((M\tri 2)^*) ) =
(\sem{\Gamma}, ☠ : 0 \prov \babort (☠) : \sem{[M\tri 1/x]B}((M\tri 2)^*) ) \]
so we're good.
$\blat$ is a special case of $\gg$
I claim that $\blat A$ is equivalent to the type
\[ \gg (x : 1) . \surd A\]
It is correct semantically:
\[ (\blat A)^* = 1 = ( \gg (x : 1) . \surd A)^*\]
\[ \sem{\blat A}(\_) = (a^* : A^*) \x \sem A(a^*) = (\surd A)^* = \sem{ \gg (x : 1).\surd A}(\_)\]
Or perhaps I should say 'subsumed by' since I'm suspicious that $\blat$ perhaps "doesn't have enough
inference rules", but I think I can implement the $\blat A$ inference rules using those of $\gg$.
So I might as well throw away $\blat$. Specifically, I can implement as derived rules:
\[
{
\Gamma^\oplus \prov M : A
\over
\Gamma \prov \pair {\langle\rangle} {\mathbf{in}_\surd\ M} : \gg (x:1).\surd A
}
\]
to replace $\mathbf{in}_\blat$, and
\[
{
\Gamma^\ominus \prov M : \gg (x:1).\surd A
\over
\Gamma \prov \mathbf{el}_\surd( M\tri 2) : A
}
\]
In the second rule, I'm using weakening to get from $\Gamma^\ominus$ to $\Gamma$. Actually
I could have actually asserted the stronger
\[
{
\Gamma^\ominus \prov M : \gg (x:1).\surd A
\over
\Gamma^\ominus \prov \mathbf{el}_\surd( M\tri 2) : A
}
\]
This is still kosher semantically. We have from applying the $\sem \dash$ i.h. to the premise
the fact that
\[ \Gamma^* \prov \sem M : (a^* : A^*) \x \sem A(a^*) \tag{*}\]
and we must show in the goal
\[ \Gamma^* \prov (\mathbf{el}_\surd( M\tri 2))^* : A^*\]
\[ \Gamma^* \prov \sem{\mathbf{el}_\surd( M\tri 2)} : \sem A((\mathbf{el}_\surd( M\tri 2))^*) \]
But we compute
\[ (\mathbf{el}_\surd( M\tri 2))^* = (M\tri 2)^*.1 = \sem M.1 \]
\[ \sem {\mathbf{el}_\surd( M\tri 2)} = (M\tri 2)^*.2 = \sem M.2\]
so our goals become
\[ \Gamma^* \prov \sem M.1 : A^*\]
\[ \Gamma^* \prov \sem M.2 : \sem A(\sem M.1) \]
which fall directly out of $(*)$.
Proving $\blat 0 \prov \T$
I want to return to the challenge of proving $\blat 0 \prov \T$ now.
With the above unpacking of $\blat$, this becomes
\[\gg(x:1).\surd 0 \prov \T\]
Let's take a look at pairing
\[
\Gamma, \star \prov M : B\qquad \Gamma^\oplus \prov N : B \qquad \Gamma^\oplus, \star \prov M \equiv N : B
\over
\Gamma \prov \langle\!\langle M, N\rangle\!\rangle : B
\]
and special case it to
\[
\Gamma, \star \prov \star : \T\qquad \Gamma^\oplus \prov N : \T \qquad \Gamma^\oplus, \star \prov M \equiv N : \T
\over
\Gamma \prov \langle\!\langle \star, N\rangle\!\rangle : \T
\]
This suggests we might want a new rule for $\T$, something like
\[
\Gamma^\oplus \prov M : \T
\over
\Gamma \prov {\triangle}M : \T\]
But actually maybe what we should do is strengthen the $\T$-elim rule a little bit.
What if we add promotion to the first premise of the elim rule like so:
\[
{
\Gamma^\oplus \prov M : \T \qquad \Gamma, \star \prov N : A
\over
\Gamma \prov \blet \star = M \bin N : A}
\]
This still seems semantically kosher, because all we're really changing is the
information we get from the first premise in the "downstairs" case from
$\Gamma^* \prov M^* : 1$ to $\sem \Gamma \prov M^* : 1$. But this information
is trivial anyway, and we never use it in the proof of the soundness of the rule!
So we can say ${\triangle}$ is just a macro for $\blet \star = \dash \bin \star$,
which is almost but not quite a trivial $\eta$-expansion because of the context promotion.
Then we can prove:
\[
\dfrac
{
\dfrac
{
\dfrac
{
\dfrac
{
y : \gg(x : 1). \surd 0 \prov y : \gg(x : 1). \surd 0
}{
y :: \gg(x : 1). \surd 0, \star \prov y\tri 2 : \surd 0
}}{
y :: \gg(x : 1). \surd 0 \prov \mathbf{el}_\surd\ ( y\tri 2) : 0
}}{
y :: \gg(x : 1). \surd 0 \prov \babort(\mathbf{el}_\surd\ ( y\tri 2)) : \T
}}{
y : \gg(x : 1). \surd 0 \prov {\triangle}(\babort(\mathbf{el}_\surd\ ( y\tri 2))) : \T
}
\]
A Guess for the Universe Isomorphism
I'd like to make
\[\surd \rtype \cong (A : \T \to \rtype) \x (t : \T) (a : A\ t) \to \rtype \]
so I attempt
\[\mathsf{fore}_1 : \surd \rtype \to \T \to \rtype \]
\[\mathsf{fore}_1\ C\ t = \mathbf{el}_\surd\ C \]
\[\mathsf{fore}_2 : \surd \rtype \to (t : \T) (a : \mathsf{fore}_1\ C\ t) \to \rtype \]
\[\mathsf{fore}_2\ C = {\lambda t.\lambda a. (a' : \surd (\mathbf{el}_\surd C)) \x (\mathbf{el}_\surd\ a' \equiv a) } \]
\[\mathsf{fore} : \surd \rtype \to (A : \T \to \rtype) \x (t : \T) (a : A\ t) \to \rtype \]
\[\mathsf{fore}\ C = \pair { \mathsf{fore}_1\ C } { \mathsf{fore}_2\ C }\]
\[\mathsf{back} : (A : \T \to \rtype) (B : (t : \T) (a : A\ t) \to \rtype )\to \surd \rtype \]
\[\mathsf{back}\ A\ B = \mathbf{in}_\surd\ (\gg(a : A\ \star).(B\ \star\ a)) \]
We can be careful and check that $\mathsf{fore}_2$ is really a type:
\[
\dfrac
{
\dfrac
{
\dfrac{
\dfrac{}
{
C \div \surd \rtype, \star \prov C :
\rtype
}
}
{
C \div \surd \rtype \prov \mathbf{el}_\surd C :
\rtype
}
}
{
\cdots \prov \surd (\mathbf{el}_\surd C) :
\rtype
}
\quad
\dfrac{
\dfrac{
\dfrac{}
{
\cdots, \star \prov a' : \surd(\mathsf{fore}_1\ C\ t)
}
}
{
\cdots \prov \mathbf{el}_\surd\ a' : \mathsf{fore}_1\ C\ t
}
\quad
\dfrac{}
{
\cdots \prov a : \mathsf{fore}_1\ C\ t
}
}
{
\cdots, a' : \surd (\mathbf{el}_\surd C) \prov \mathbf{el}_\surd\ a' \equiv a :
\rtype
}
}
{
C : \surd \rtype, t : \T, a : \mathsf{fore}_1\ C\ t \prov (a' : \surd (\mathbf{el}_\surd C)) \x (\mathbf{el}_\surd\ a' \equiv a) :
\rtype
}
\]
Let's try to see if anything interesting happens when we do some round-trips.
The computation of $\mathsf{back}$ of $\mathsf{fore}$ gives:
\[\mathsf{back}\ (\mathsf{fore}_1\ C)\ (\mathsf{fore}_2\ C) \]
\[= \mathbf{in}_\surd\ (\gg(a : \mathsf{fore}_1\ C\ \star).(\mathsf{fore}_2\ C\ \star\ a)) \]
\[= \mathbf{in}_\surd\ (\gg(a : \mathbf{el}_\surd\ C).( (a' : \surd (\mathbf{el}_\surd C)) \x (\mathbf{el}_\surd\ a' \equiv a) ) \]
so we'd want to show this is equal to $C$ at $\surd \rtype$. Although I can rely on univalence to tell me what
equality of types means, I need to pin down what equality at $\surd$ means! Maybe there's some kind of extensionality; that
all I need is equality under eliminations.
Is this equality plausible semantically? If I hit with $\dash^*$ I get
\[(\mathbf{in}_\surd\ (\gg(a : \mathbf{el}_\surd\ C).( (a' : \surd (\mathbf{el}_\surd C)) \x (\mathbf{el}_\surd\ a' \equiv a) ))^* \]
\[= \pair{X^*}{ \sem X} \]
for
\[ X = \gg(a : \mathbf{el}_\surd\ C).( (a' : \surd (\mathbf{el}_\surd C)) \x (\mathbf{el}_\surd\ a' \equiv a) ) \]
and I'd find (using some very sketchy reasoning at certain steps, but I think this is still vaguely plausible. I need
to be more careful reasoning about universes and elements, I think)
\[ \pair{X^*}{ \sem X} = \pair {(\mathbf{el}_\surd\ C)^*} {\lambda a^* : (\mathbf{el}_\surd\ C)^* . (a' : \surd (\mathbf{el}_\surd C)) \x (\mathbf{el}_\surd\ a' \equiv a)^* }\]
\[ = \pair {C^*.1} {\lambda a^* : (C^*.1) . ((a' : \surd (\mathbf{el}_\surd C)) \x (\mathbf{el}_\surd\ a' \equiv a))^* }\]
\[ = \pair {C^*.1} {\lambda a^* : (C^*.1) . ({a'}^* : (\surd (\mathbf{el}_\surd C))^*) \x (\mathbf{el}_\surd\ a' \equiv a)^* }\]
\[ = \pair {C^*.1} {\lambda a^* : (C^*.1) . ({a'}^* : (\surd (\mathbf{el}_\surd C))^*) \x ({a'}^*.1 \equiv a^*) }\]
\[ = \pair {C^*.1} {\lambda a^* : (C^*.1) . ({a'}^* : (y^* : (\mathbf{el}_\surd C)^*) \x \sem{\mathbf{el}_\surd C}(y^*)) \x ({a'}^*.1 \equiv a^*) }\]
\[ = \pair {C^*.1} {\lambda a^* : (C^*.1) . ({a'}^* : (y^* : C^*.1) \x C^*.2\ y^*) \x ({a'}^*.1 \equiv a^*) }\]
\[ = \pair {C^*.1} {\lambda a^* : (C^*.1) . ( C^*.2\ a^*) }\]
\[ = \pair {C^*.1} {C^*.2 }\]
\[ = C\]
Let's try the other direction. Assume $A : \T \to \rtype$ and $B : (t : \T)(a : A\ t) \to \rtype$.
We expect $\mathsf{fore}_1\ (\mathsf{back}\ A\ B)\ t = A\ t$ so we compute
\[ \mathsf{fore}_1\ (\mathsf{back}\ A\ B)\ t = \mathbf{el}_\surd\ (\mathsf{back}\ A\ B) \]
\[= \mathbf{el}_\surd\ (\mathbf{in}_\surd\ (\gg(a : A\ \star).(B\ \star\ a))) \]
\[= \gg(a : A\ \star).(B\ \star\ a) \]
At let's now compare semantics. We have a $t : \T$ present, so we only need to check the base, not the relation,
for we can use $\sem \T(\_) = 0$ to abort. And indeed we have
\[ (\gg(a : A\ \star).(B\ \star\ a))^* = (A\ \star)^* = A^*\ \langle\rangle = (A\ t)^*\]
We expect $\mathsf{fore}_2\ (\mathsf{back}\ A\ B)\ t\ a = B\ t\ a$ so we compute:
\[\mathsf{fore}_2\ (\mathsf{back}\ A\ B)\ t\ a = { (a' : \surd (\mathbf{el}_\surd (\mathsf{back}\ A\ B))) \x (\mathbf{el}_\surd\ a' \equiv a) } \]
\[ = { (a' : \surd (\mathbf{el}_\surd (\mathbf{in}_\surd\ (\gg(a : A\ \star).(B\ \star\ a))))) \x (\mathbf{el}_\surd\ a' \equiv a) } \]
\[ = { (a' : \surd (\gg(a : A\ \star).(B\ \star\ a))) \x (\mathbf{el}_\surd\ a' \equiv a) } \]
Ok, let's try to compute the semantics of this then.
\[ ( (a' : \surd (\gg(a : A\ \star).(B\ \star\ a))) \x (\mathbf{el}_\surd\ a' \equiv a) )^* \]
\[= ( ({a'}^* : (y^* : (\gg(a : A\ \star).(B\ \star\ a))^* \x \sem{\gg(a : A\ \star).(B\ \star\ a)}(y^*))) \x ({a'}^*.1 \equiv a^*) \]
\[= ({a'}^* : (y^* : A^*\ \langle\rangle) \x B^*\ \langle\rangle\ y^*) \x ({a'}^*.1 \equiv a^*) \]
\[= B^*\ \langle\rangle\ a^* = (B\ \star\ a)^*\]
So although I still would want to realize these type (and $\surd \rtype$) equations internally, it's very promising that
they make sense semantically.