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