## Stream: general

### Topic: context irrelevance of defeq

#### Reid Barton (Feb 28 2020 at 15:31):

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 (Feb 28 2020 at 21:32):

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

#### Mario Carneiro (Feb 28 2020 at 21:32):

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

#### Mario Carneiro (Feb 28 2020 at 22:32):

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 (Feb 29 2020 at 01:04):

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

#### Mario Carneiro (Feb 29 2020 at 03:04):

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 (Feb 29 2020 at 14:30):

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$

Last updated: Dec 20 2023 at 11:08 UTC