4
$\begingroup$

I've started to read Egbert Rijke's HoTT lecture notes which can be found here.

In the first lecture, some inference rules and structural rules are given, and in Exercise 1.1 it is asked to derive following term conversion rule using the rules given before:

If $\Gamma \vdash A\equiv A'$ type and $\Gamma \vdash a:A$, then $\Gamma \vdash a:A'$.

I'm not sure how can prove it formally. Here is my attempt:

Since $A\equiv A'$ in the context $\Gamma$, we have $\Gamma \vdash A'$. Using the variable rule, we gave $\Gamma, x:A' \vdash x:A'$ (1). Using the symmetry of judgmental equality of types, we have $\Gamma \vdash A'\equiv A$ (2). Using the conversion rule with generic judgment A/A' on (2) and (1), we obtain $\Gamma, x:A \vdash x:A'$ (3). Now, from (3) and $\Gamma \vdash a:A$, using substitution rule, we conclude $\Gamma \vdash a:A'$.

I'm not so familiar with the notation, so it can be written better. I hope, nevertheless, it makes sense to a reader. If someone gives a feedback or correction, it would be helpful.

$\endgroup$

1 Answer 1

2
$\begingroup$

That looks right.

However, I have to say this exercise looks bizarre to me. Note that Rijke's "variable conversion rule" can also be derived from the term conversion rule together with substitution, so we might as well have taken the term conversion rule as the primitive one instead of the variable conversion rule. This is what's is done in nearly all presentations of dependent type theory that I've seen; I don't know why Rijke did it a different way.

$\endgroup$
1
  • $\begingroup$ I think this is just an exercise to get used to make derivations using the structural rules. $\endgroup$
    – phdstudent
    Mar 12, 2021 at 19:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .