One More Type in the Tiny Type Theory

jcreed blog > 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 \[...

One More Type in the Tiny Type Theory

Related Articles

The Newest Instagram "Exploit" Is the Goofiest I've Seen

Apple WWDC 2026 Livestream

Claude Fable 5

US Government directive to suspend access to Fable 5 and Mythos 5

It's Not Just X. It's Y