context irrelevance of defeq

Stream: general

[Reid Barton]

Does Lean have the following metatheoretic property:
If $\Gamma \vdash a : A$ and $\Gamma \vdash b : A$ and $\Gamma, \Delta \vdash a \equiv b$ (defeq), then $\Gamma \vdash a \equiv b$.
Also, is there an established name for this property?

[Mario Carneiro]

I'm pretty sure the answer is yes, but I don't think if explicitly shows up in the thesis

[Mario Carneiro]

If $\Delta$ is inhabited, you can prove it by substitution

[Mario Carneiro]

It's also equivalent to the following statement about typing: If $\Gamma,\Delta\vdash e:A$ and $FV(e)\subseteq\Gamma$, then $\Gamma\vdash e:A$

[Reid Barton]

(do you also need $FV(A) \subseteq \Gamma$ or does it follow?)

[Mario Carneiro]

Another good question in the same area. Obviously the "natural type" of $e$ does not have any free variables not in $e$ itself, but it is possible for defeq terms to have different sets of free variables because of proof irrelevance.

For example, consider the proofs $A:U\vdash refl\;A: A = A$ and $A:U,h:\bot\vdash rec_{\bot}\; (A=A)\; h:A=A$. By proof irrelevance, these two are defeq in the context $A:U,h:\bot$. So you could have $A:U,x:A,h:\bot\vdash x: cast (rec_{\bot}\; (A=A)\; h) A$ (where the cast is defeq to $A$).

[Reid Barton]

Now that you say that, isn't a more down to earth version something like $A : U, x : A, B : U \vdash x : \mathrm{const}_A(B)$, where $\mathrm{const_A}(t) = A$ for all $t$