One More Type in the Tiny Type Theory(jcreedcmu.github.io)

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

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 …