Step
*
2
of Lemma
contraction-to-extend_wf
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. contraction-to-extend(Gamma;A;cA;ctr) ∈ extension-fun{j:l}(Gamma; A)
6. H : CubicalSet{j}
7. K : CubicalSet{j}
8. tau : K j⟶ H
9. sigma : H j⟶ Gamma
10. phi : {H ⊢ _:𝔽}
11. u : {H, phi ⊢ _:(A)sigma}
12. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
13. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
(contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
14. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
15. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
16. ∀x:{H, phi ⊢ _:(A)sigma}
((path-eta(contr-path((ctr)sigma;x)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
∧ ((path-eta(contr-path((ctr)sigma;x)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma})
∧ ((path-eta(contr-path((ctr)sigma;x)))[1(𝕀)] = x ∈ {H, phi ⊢ _:(A)sigma}))
17. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
18. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
19. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
20. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
21. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0)s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
22. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (contr-center((ctr)sigma))s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
⊢ (contraction-to-extend(Gamma;A;cA;ctr) H sigma phi u)tau
= (contraction-to-extend(Gamma;A;cA;ctr) K sigma o tau (phi)tau (u)tau)
∈ {K ⊢ _:((A)sigma)tau[(phi)tau |⟶ (u)tau]}
BY
{ EqTypeCD }
1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. contraction-to-extend(Gamma;A;cA;ctr) ∈ extension-fun{j:l}(Gamma; A)
6. H : CubicalSet{j}
7. K : CubicalSet{j}
8. tau : K j⟶ H
9. sigma : H j⟶ Gamma
10. phi : {H ⊢ _:𝔽}
11. u : {H, phi ⊢ _:(A)sigma}
12. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
13. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
(contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
14. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
15. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
16. ∀x:{H, phi ⊢ _:(A)sigma}
((path-eta(contr-path((ctr)sigma;x)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
∧ ((path-eta(contr-path((ctr)sigma;x)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma})
∧ ((path-eta(contr-path((ctr)sigma;x)))[1(𝕀)] = x ∈ {H, phi ⊢ _:(A)sigma}))
17. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
18. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
19. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
20. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
21. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0)s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
22. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (contr-center((ctr)sigma))s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
⊢ (contraction-to-extend(Gamma;A;cA;ctr) H sigma phi u)tau
= (contraction-to-extend(Gamma;A;cA;ctr) K sigma o tau (phi)tau (u)tau)
∈ {K ⊢ _:((A)sigma)tau}
2
.....set predicate.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. contraction-to-extend(Gamma;A;cA;ctr) ∈ extension-fun{j:l}(Gamma; A)
6. H : CubicalSet{j}
7. K : CubicalSet{j}
8. tau : K j⟶ H
9. sigma : H j⟶ Gamma
10. phi : {H ⊢ _:𝔽}
11. u : {H, phi ⊢ _:(A)sigma}
12. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
13. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
(contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
14. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
15. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
16. ∀x:{H, phi ⊢ _:(A)sigma}
((path-eta(contr-path((ctr)sigma;x)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
∧ ((path-eta(contr-path((ctr)sigma;x)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma})
∧ ((path-eta(contr-path((ctr)sigma;x)))[1(𝕀)] = x ∈ {H, phi ⊢ _:(A)sigma}))
17. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
18. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
19. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
20. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
21. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0)s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
22. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (contr-center((ctr)sigma))s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
⊢ (u)tau = (contraction-to-extend(Gamma;A;cA;ctr) H sigma phi u)tau ∈ {K, (phi)tau ⊢ _:((A)sigma)tau}
3
.....wf.....
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. contraction-to-extend(Gamma;A;cA;ctr) ∈ extension-fun{j:l}(Gamma; A)
6. H : CubicalSet{j}
7. K : CubicalSet{j}
8. tau : K j⟶ H
9. sigma : H j⟶ Gamma
10. phi : {H ⊢ _:𝔽}
11. u : {H, phi ⊢ _:(A)sigma}
12. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
13. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
(contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
14. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
15. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
16. ∀x:{H, phi ⊢ _:(A)sigma}
((path-eta(contr-path((ctr)sigma;x)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
∧ ((path-eta(contr-path((ctr)sigma;x)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma})
∧ ((path-eta(contr-path((ctr)sigma;x)))[1(𝕀)] = x ∈ {H, phi ⊢ _:(A)sigma}))
17. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
18. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
19. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
20. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
21. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0)s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
22. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
= comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (contr-center((ctr)sigma))s
∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
23. a : {K ⊢ _:((A)sigma)tau}
⊢ istype((u)tau = a ∈ {K, (phi)tau ⊢ _:((A)sigma)tau})
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. cA : Gamma \mvdash{} Compositon(A)
4. ctr : \{Gamma \mvdash{} \_:Contractible(A)\}
5. contraction-to-extend(Gamma;A;cA;ctr) \mmember{} extension-fun\{j:l\}(Gamma; A)
6. H : CubicalSet\{j\}
7. K : CubicalSet\{j\}
8. tau : K j{}\mrightarrow{} H
9. sigma : H j{}\mrightarrow{} Gamma
10. phi : \{H \mvdash{} \_:\mBbbF{}\}
11. u : \{H, phi \mvdash{} \_:(A)sigma\}
12. contr-center((ctr)sigma) \mmember{} \{H \mvdash{} \_:(A)sigma\}
13. \mforall{}[c:\{H, phi \mvdash{} \_:Contractible((A)sigma)\}]. \mforall{}[x:\{H, phi \mvdash{} \_:(A)sigma\}].
(contr-path(c;x) \mmember{} \{H, phi \mvdash{} \_:(Path\_(A)sigma contr-center(c) x)\})
14. \mforall{}[x:\{H, phi \mvdash{} \_:(A)sigma\}]
(contr-path((ctr)sigma;x) \mmember{} \{H, phi \mvdash{} \_:(Path\_(A)sigma contr-center((ctr)sigma) x)\})
15. \mforall{}[pth:\{H, phi \mvdash{} \_:Path((A)sigma)\}]. (path-eta(pth) \mmember{} \{H, phi.\mBbbI{} \mvdash{} \_:((A)sigma)p\})
16. \mforall{}x:\{H, phi \mvdash{} \_:(A)sigma\}
((path-eta(contr-path((ctr)sigma;x)) \mmember{} \{H, phi.\mBbbI{} \mvdash{} \_:((A)sigma)p\})
\mwedge{} ((path-eta(contr-path((ctr)sigma;x)))[0(\mBbbI{})] = contr-center((ctr)sigma))
\mwedge{} ((path-eta(contr-path((ctr)sigma;x)))[1(\mBbbI{})] = x))
17. path-eta(contr-path((ctr)sigma;u)) \mmember{} \{H, phi.\mBbbI{} \mvdash{} \_:((A)sigma)p\}
18. (path-eta(contr-path((ctr)sigma;u)))[0(\mBbbI{})] = contr-center((ctr)sigma)
19. (path-eta(contr-path((ctr)sigma;u)))[1(\mBbbI{})] = u
20. ((cA)sigma)p \mmember{} H.\mBbbI{} \mvdash{} Compositon(((A)sigma)p)
21. \mforall{}[a0:\{H \mvdash{} \_:(A)sigma[phi |{}\mrightarrow{} (path-eta(contr-path((ctr)sigma;u)))[0(\mBbbI{})]]\}]. \mforall{}[Delta:j\mvdash{}].
\mforall{}[s:Delta j{}\mrightarrow{} H].
((comp ((cA)sigma)p [phi \mvdash{}\mrightarrow{} path-eta(contr-path((ctr)sigma;u))] a0)s
= comp (((cA)sigma)p)s+ [(phi)s \mvdash{}\mrightarrow{} (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s)
22. \mforall{}[Delta:j\mvdash{}]. \mforall{}[s:Delta j{}\mrightarrow{} H].
((comp ((cA)sigma)p [phi \mvdash{}\mrightarrow{} path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
= comp (((cA)sigma)p)s+ [(phi)s \mvdash{}\mrightarrow{} (path-eta(contr-path((ctr)sigma;u)))s+]
(contr-center((ctr)sigma))s)
\mvdash{} (contraction-to-extend(Gamma;A;cA;ctr) H sigma phi u)tau
= (contraction-to-extend(Gamma;A;cA;ctr) K sigma o tau (phi)tau (u)tau)
By
Latex:
EqTypeCD
Home
Index