jcreed blog > One More Type in the Tiny Type Theory

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 } \]