Step
*
2
1
1
1
2
1
of Lemma
csm-cubical-identity
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
6. ∀I:Cname List. ∀a:X(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a))
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a)))
8. a : {X ⊢ _:<A1, A2>}
9. b : {X ⊢ _:<A1, A2>}
10. X ⊢ <A1, A2>
11. Delta ⊢ (<A1, A2>)s
12. I : Cname List
13. J : Cname List
14. f : name-morph(I;J)
15. a1 : Delta(I)
16. z : {z:Cname| ¬(z ∈ I)}
17. u2 : named-path(X;<A1, A2>;a;b;I;(s)a1;z)
18. z1 : {z:Cname| ¬(z ∈ I)}
19. u3 : <A1, A2>(iota(z1)((s)a1))
20. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z1;u3)
21. (u2 iota(z)((s)a1) rename-one-name(z;z1)) = u3 ∈ <A1, A2>(iota(z1)((s)a1))
⊢ (u2 iota(z)((s)a1) f[z:=fresh-cname(J)])
= (u3 iota(z1)(a1) f[z1:=fresh-cname(J)])
∈ <A1, A2>(iota(fresh-cname(J))((s)f(a1)))
BY
{ ((Subst' <λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)> ~ (<A1, A2>)s 0 THENA (RepUR ``csm-ap-type`` 0 THEN Auto))
THEN RevHypSubst (-1) 0
) }
1
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
6. ∀I:Cname List. ∀a:X(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a))
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a)))
8. a : {X ⊢ _:<A1, A2>}
9. b : {X ⊢ _:<A1, A2>}
10. X ⊢ <A1, A2>
11. Delta ⊢ (<A1, A2>)s
12. I : Cname List
13. J : Cname List
14. f : name-morph(I;J)
15. a1 : Delta(I)
16. z : {z:Cname| ¬(z ∈ I)}
17. u2 : named-path(X;<A1, A2>;a;b;I;(s)a1;z)
18. z1 : {z:Cname| ¬(z ∈ I)}
19. u3 : <A1, A2>(iota(z1)((s)a1))
20. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z1;u3)
21. (u2 iota(z)((s)a1) rename-one-name(z;z1)) = u3 ∈ <A1, A2>(iota(z1)((s)a1))
⊢ (u2 iota(z)((s)a1) f[z:=fresh-cname(J)])
= ((u2 iota(z)((s)a1) rename-one-name(z;z1)) iota(z1)(a1) f[z1:=fresh-cname(J)])
∈ <A1, A2>(iota(fresh-cname(J))((s)f(a1)))
2
.....wf.....
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
6. ∀I:Cname List. ∀a:X(I). ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a))
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a)))
8. a : {X ⊢ _:<A1, A2>}
9. b : {X ⊢ _:<A1, A2>}
10. X ⊢ <A1, A2>
11. Delta ⊢ (<A1, A2>)s
12. I : Cname List
13. J : Cname List
14. f : name-morph(I;J)
15. a1 : Delta(I)
16. z : {z:Cname| ¬(z ∈ I)}
17. u2 : named-path(X;<A1, A2>;a;b;I;(s)a1;z)
18. z1 : {z:Cname| ¬(z ∈ I)}
19. u3 : <A1, A2>(iota(z1)((s)a1))
20. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z1;u3)
21. (u2 iota(z)((s)a1) rename-one-name(z;z1)) = u3 ∈ <A1, A2>(iota(z1)((s)a1))
22. z2 : <A1, A2>(iota(z1)((s)a1))
⊢ (u2 iota(z)((s)a1) f[z:=fresh-cname(J)])
= (z2 iota(z1)(a1) f[z1:=fresh-cname(J)])
∈ <A1, A2>(iota(fresh-cname(J))((s)f(a1))) ∈ ℙ
Latex:
Latex:
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta {}\mrightarrow{} X
4. A1 : I:(Cname List) {}\mrightarrow{} X(I) {}\mrightarrow{} Type
5. A2 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} a:X(I) {}\mrightarrow{} (A1 I a) {}\mrightarrow{} (A1 J f(a))
6. \mforall{}I:Cname List. \mforall{}a:X(I). \mforall{}u:A1 I a. ((A2 I I 1 a u) = u)
7. \mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K). \mforall{}a:X(I). \mforall{}u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)))
8. a : \{X \mvdash{} \_:<A1, A2>\}
9. b : \{X \mvdash{} \_:<A1, A2>\}
10. X \mvdash{} <A1, A2>
11. Delta \mvdash{} (<A1, A2>)s
12. I : Cname List
13. J : Cname List
14. f : name-morph(I;J)
15. a1 : Delta(I)
16. z : \{z:Cname| \mneg{}(z \mmember{} I)\}
17. u2 : named-path(X;<A1, A2>a;b;I;(s)a1;z)
18. z1 : \{z:Cname| \mneg{}(z \mmember{} I)\}
19. u3 : <A1, A2>(iota(z1)((s)a1))
20. name-path-endpoints(X;<A1, A2>a;b;I;(s)a1;z1;u3)
21. (u2 iota(z)((s)a1) rename-one-name(z;z1)) = u3
\mvdash{} (u2 iota(z)((s)a1) f[z:=fresh-cname(J)]) = (u3 iota(z1)(a1) f[z1:=fresh-cname(J)])
By
Latex:
((Subst' <\mlambda{}I,a. (A1 I (s)a), \mlambda{}I,J,f,a,u. (A2 I J f (s)a u)> \msim{} (<A1, A2>)s 0 THENA (RepUR ``csm-ap-ty\000Cpe`` 0 THEN Auto))
THEN RevHypSubst (-1) 0
)
Home
Index