Step
*
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)))
∧ (∀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))))
7. a : {X ⊢ _:<A1, A2>}
8. b : {X ⊢ _:<A1, A2>}
9. X ⊢ <A1, A2>
10. Delta ⊢ (<A1, A2>)s
11. I : Cname List
12. J : Cname List
13. f : name-morph(I;J)
14. a1 : Delta(I)
15. u : I-path(X;<A1, A2>;a;b;I;(s)a1)
16. u1 : I-path(X;<A1, A2>;a;b;I;(s)a1)
17. path-eq(X;<A1, A2>;I;(s)a1;u;u1)
⊢ I-path-morph(X;<A1, A2>;I;J;f;(s)a1;u) = I-path-morph(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;I;J;f;a\000C1;u1) ∈ cubical-path(X;<A1, A2>;a;b;J;(s)f(a1))
BY
{ SubsumeC ⌜I-path(X;<A1, A2>;a;b;J;(s)f(a1))⌝⋅ }
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)))
∧ (∀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))))
7. a : {X ⊢ _:<A1, A2>}
8. b : {X ⊢ _:<A1, A2>}
9. X ⊢ <A1, A2>
10. Delta ⊢ (<A1, A2>)s
11. I : Cname List
12. J : Cname List
13. f : name-morph(I;J)
14. a1 : Delta(I)
15. u : I-path(X;<A1, A2>;a;b;I;(s)a1)
16. u1 : I-path(X;<A1, A2>;a;b;I;(s)a1)
17. path-eq(X;<A1, A2>;I;(s)a1;u;u1)
⊢ I-path-morph(X;<A1, A2>;I;J;f;(s)a1;u) = I-path-morph(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;I;J;f;a\000C1;u1) ∈ I-path(X;<A1, A2>;a;b;J;(s)f(a1))
2
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)))
∧ (∀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))))
7. a : {X ⊢ _:<A1, A2>}
8. b : {X ⊢ _:<A1, A2>}
9. X ⊢ <A1, A2>
10. Delta ⊢ (<A1, A2>)s
11. I : Cname List
12. J : Cname List
13. f : name-morph(I;J)
14. a1 : Delta(I)
15. u : I-path(X;<A1, A2>;a;b;I;(s)a1)
16. u1 : I-path(X;<A1, A2>;a;b;I;(s)a1)
17. path-eq(X;<A1, A2>;I;(s)a1;u;u1)
18. I-path-morph(X;<A1, A2>;I;J;f;(s)a1;u) = I-path-morph(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;I;J;f\000C;a1;u1) ∈ I-path(X;<A1, A2>;a;b;J;(s)f(a1))
⊢ I-path(X;<A1, A2>;a;b;J;(s)f(a1)) ⊆r cubical-path(X;<A1, A2>;a;b;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))
\mwedge{} (\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))))
7. a : \{X \mvdash{} \_:<A1, A2>\}
8. b : \{X \mvdash{} \_:<A1, A2>\}
9. X \mvdash{} <A1, A2>
10. Delta \mvdash{} (<A1, A2>)s
11. I : Cname List
12. J : Cname List
13. f : name-morph(I;J)
14. a1 : Delta(I)
15. u : I-path(X;<A1, A2>a;b;I;(s)a1)
16. u1 : I-path(X;<A1, A2>a;b;I;(s)a1)
17. path-eq(X;<A1, A2>I;(s)a1;u;u1)
\mvdash{} I-path-morph(X;<A1, A2>I;J;f;(s)a1;u) = I-path-morph(Delta;<\mlambda{}I,a. (A1 I (s)a), \mlambda{}I,J,f,a,u. (A2 I \000CJ f (s)a u)>I;J;f;a1;u1)
By
Latex:
SubsumeC \mkleeneopen{}I-path(X;<A1, A2>a;b;J;(s)f(a1))\mkleeneclose{}\mcdot{}
Home
Index