---

Step * 1 of Lemma type-function-eta


1. A : Type
2. B : per-function(A;a.Type)
3. C : per-function(A;a.Type)
4. B = C ∈ per-function(A;a.Type)
⊢ (λx.(B x)) = (λx.(C x)) ∈ per-function(A;a.Type)
BY
{ TACTIC:(PointwiseFunctionality 2 THEN PointwiseFunctionality 5) }

1
1. A : Type
2. a : Base
3. b : Base
4. c : a = b ∈ per-function(A;a.Type)
5. a1 : Base
6. b1 : Base
7. c1 : a1 = b1 ∈ per-function(A;a.Type)
8. a = a1 ∈ per-function(A;a.Type)
⊢ (λx.(a x)) = (λx.(a1 x)) ∈ per-function(A;a.Type)

2
1. A : Type
2. a : Base
3. b : Base
4. c : a = b ∈ per-function(A;a.Type)
5. a1 : Base
6. b1 : Base
7. c1 : a1 = b1 ∈ per-function(A;a.Type)
8. a = a1 ∈ per-function(A;a.Type)
⊢ ((λx.(a x)) = (λx.(a1 x)) ∈ per-function(A;a.Type)) = ((λx.(a x)) = (λx.(b1 x)) ∈ per-function(A;a.Type)) ∈ 𝕌'

3
1. A : Type
2. a : Base
3. b : Base
4. c : a = b ∈ per-function(A;a.Type)
5. a1 : Base
6. b1 : Base
7. c1 : a1 = b1 ∈ per-function(A;a.Type)
8. a = a1 ∈ per-function(A;a.Type)
⊢ ((λx.(a x)) = (λx.(a1 x)) ∈ per-function(A;a.Type)) = ((λx.(b x)) = (λx.(a1 x)) ∈ per-function(A;a.Type)) ∈ 𝕌'

4
1. A : Type
2. a : Base
3. b : Base
4. c : a = b ∈ per-function(A;a.Type)
5. a1 : Base
6. b1 : Base
7. c1 : a1 = b1 ∈ per-function(A;a.Type)
8. a = a1 ∈ per-function(A;a.Type)
⊢ (((λx.(a x)) = (λx.(a1 x)) ∈ per-function(A;a.Type)) = ((λx.(b x)) = (λx.(a1 x)) ∈ per-function(A;a.Type)) ∈ 𝕌')
= (((λx.(a x)) = (λx.(b1 x)) ∈ per-function(A;a.Type)) = ((λx.(b x)) = (λx.(b1 x)) ∈ per-function(A;a.Type)) ∈ 𝕌')
∈ 𝕌{i 2}

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  per-function(A;a.Type)
3.  C  :  per-function(A;a.Type)
4.  B  =  C
\mvdash{}  (\mlambda{}x.(B  x))  =  (\mlambda{}x.(C  x))


By

---

Latex:
TACTIC:(PointwiseFunctionality  2  THEN  PointwiseFunctionality  5)

---

Home Index