---

Step * 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. a@0 : Delta(I)
14. I-path(X;<A1, A2>;a;b;I;(s)a@0) = I-path(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;(a)s;(b)s;I;a@0) ∈\000C Type
15. p : I-path(X;<A1, A2>;a;b;I;(s)a@0)
16. q : I-path(X;<A1, A2>;a;b;I;(s)a@0)
⊢ path-eq(X;<A1, A2>;I;(s)a@0;p;q) = path-eq(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;I;a@0;p;q) ∈ ℙ
BY
{ TACTIC:(D -2 THEN D -1 THEN RepUR ``path-eq`` 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. a@0 : Delta(I)
14. I-path(X;<A1, A2>;a;b;I;(s)a@0) = I-path(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;(a)s;(b)s;I;a@0) ∈\000C Type
15. z : {z:Cname| ¬(z ∈ I)} 
16. p1 : named-path(X;<A1, A2>;a;b;I;(s)a@0;z)
17. z1 : {z:Cname| ¬(z ∈ I)} 
18. q1 : named-path(X;<A1, A2>;a;b;I;(s)a@0;z1)
⊢ ((p1 iota(z)((s)a@0) rename-one-name(z;z1)) = q1 ∈ <A1, A2>(iota(z1)((s)a@0)))
= ((p1 iota(z)(a@0) rename-one-name(z;z1)) = q1 ∈ <λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>(iota(z1)(a@0)))
∈ ℙ

---

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.  a@0  :  Delta(I)
14.  I-path(X;<A1,  A2>a;b;I;(s)a@0)  =  I-path(Delta;<\mlambda{}I,a.  (A1  I  (s)a),  \mlambda{}I,J,f,a,u.  (A2  I  J  f  (s)a  u)\000C>(a)s;(b)s;I;a@0)
15.  p  :  I-path(X;<A1,  A2>a;b;I;(s)a@0)
16.  q  :  I-path(X;<A1,  A2>a;b;I;(s)a@0)
\mvdash{}  path-eq(X;<A1,  A2>I;(s)a@0;p;q)  =  path-eq(Delta;<\mlambda{}I,a.  (A1  I  (s)a),  \mlambda{}I,J,f,a,u.  (A2  I  J  f  (s)a  u)\000C>I;a@0;p;q)


By

---

Latex:
TACTIC:(D  -2  THEN  D  -1  THEN  RepUR  ``path-eq``  0)

---

Home Index