Step
*
1
4
of Lemma
type-function-eta
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}
BY
{ ((EqCD THEN Auto)
THEN (EqCD THEN All (Fold `type-function`))
THEN Try ((At ⌜𝕌'⌝PerEqCD⋅
THEN Try (Fold `per-function` 0)
THEN Reduce 0
THEN Auto
THEN D 0
THEN Reduce 0
THEN Auto
THEN Fold `tf-apply` 0
THEN RenameVar `z' (-3)
THEN (Assert z ∈ A BY
Auto)
THEN EqCD
THEN Auto))
THEN Auto) }
Latex:
Latex:
1. A : Type
2. a : Base
3. b : Base
4. c : a = b
5. a1 : Base
6. b1 : Base
7. c1 : a1 = b1
8. a = a1
\mvdash{} (((\mlambda{}x.(a x)) = (\mlambda{}x.(a1 x))) = ((\mlambda{}x.(b x)) = (\mlambda{}x.(a1 x))))
= (((\mlambda{}x.(a x)) = (\mlambda{}x.(b1 x))) = ((\mlambda{}x.(b x)) = (\mlambda{}x.(b1 x))))
By
Latex:
((EqCD THEN Auto)
THEN (EqCD THEN All (Fold `type-function`))
THEN Try ((At \mkleeneopen{}\mBbbU{}'\mkleeneclose{}PerEqCD\mcdot{}
THEN Try (Fold `per-function` 0)
THEN Reduce 0
THEN Auto
THEN D 0
THEN Reduce 0
THEN Auto
THEN Fold `tf-apply` 0
THEN RenameVar `z' (-3)
THEN (Assert z \mmember{} A BY
Auto)
THEN EqCD
THEN Auto))
THEN Auto)
Home
Index