---

Step * of Lemma csm-cubical-identity

∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}.
  (((Id_A a b))s
  = (Id_(A)s (a)s (b)s)
  ∈ (A:I:(Cname List) ⟶ Delta(I) ⟶ Type × (I:(Cname List)
                                            ⟶ J:(Cname List)
                                            ⟶ f:name-morph(I;J)
                                            ⟶ a:Delta(I)
                                            ⟶ (A I a)
                                            ⟶ (A J f(a)))))
BY
{ (Auto
   THEN (Assert X ⊢ A BY
               Auto)
   THEN (Assert Delta ⊢ (A)s BY
               Auto)
   THEN RepeatFor 2 (DVar `A')
   THEN RepUR ``csm-ap-type cubical-identity`` 0
   THEN MemCD
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (((EqCD THEN Reduce 0) THENA Auto))
   THEN Try (RepeatFor 3 (((EqCD THEN Reduce 0) THENA Auto)))
   THEN All Reduce) }

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. a@0 : Delta(I)
⊢ cubical-path(X;<A1, A2>;a;b;I;(s)a@0) = cubical-path(Delta;<λI,a. (A1 I (s)a), λI,J,f,a,u. (A2 I J f (s)a u)>;(a)s;(b)\000Cs;I;a@0) ∈ Type

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 : cubical-path(X;<A1, A2>;a;b;I;(s)a1)
⊢ 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;u) ∈ cubical-path(X;<A1, A2>;a;b;J;(s)f(a1))

---

Latex:

---

Latex:
\mforall{}X,Delta:CubicalSet.  \mforall{}s:Delta  {}\mrightarrow{}  X.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.
    (((Id\_A  a  b))s  =  (Id\_(A)s  (a)s  (b)s))


By

---

Latex:
(Auto
  THEN  (Assert  X  \mvdash{}  A  BY
                          Auto)
  THEN  (Assert  Delta  \mvdash{}  (A)s  BY
                          Auto)
  THEN  RepeatFor  2  (DVar  `A')
  THEN  RepUR  ``csm-ap-type  cubical-identity``  0
  THEN  MemCD
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (((EqCD  THEN  Reduce  0)  THENA  Auto))
  THEN  Try  (RepeatFor  3  (((EqCD  THEN  Reduce  0)  THENA  Auto)))
  THEN  All  Reduce)

---

Home Index