---

Step * 1 of Lemma csm-I-path

.....subterm..... T:t
2:n
1. X : CubicalSet@i'
2. Delta : CubicalSet@i'
3. s : Delta ⟶ X@i'
4. A : {X ⊢ _}@i'
5. a : {X ⊢ _:A}@i
6. b : {X ⊢ _:A}@i
7. I : Cname List@i
8. alpha : Delta(I)@i
9. z : {z:Cname| ¬(z ∈ I)} 
⊢ named-path(Delta;(A)s;(a)s;(b)s;I;alpha;z) = named-path(X;A;a;b;I;(s)alpha;z) ∈ Type
BY
{ TACTIC:((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) }

1
1. X : CubicalSet@i'
2. Delta : CubicalSet@i'
3. s : Delta ⟶ X@i'
4. A1 : I:(Cname List) ⟶ X(I) ⟶ Type@i'
5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))@i'
6. let A,F = <A1, A2> 
   in (∀I:Cname List. ∀a:X(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
      ∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A I a.
           ((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K (f o g)(a))))
7. a : {X ⊢ _:<A1, A2>}@i
8. b : {X ⊢ _:<A1, A2>}@i
9. I : Cname List@i
10. alpha : Delta(I)@i
11. z : {z:Cname| ¬(z ∈ I)} 
12. X ⊢ <A1, A2>
13. Delta ⊢ (<A1, A2>)s
⊢ named-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;alpha;z) = named-path(X;<A1, A2>;a;b;I\000C;(s)alpha;z) ∈ Type

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  CubicalSet@i'
2.  Delta  :  CubicalSet@i'
3.  s  :  Delta  {}\mrightarrow{}  X@i'
4.  A  :  \{X  \mvdash{}  \_\}@i'
5.  a  :  \{X  \mvdash{}  \_:A\}@i
6.  b  :  \{X  \mvdash{}  \_:A\}@i
7.  I  :  Cname  List@i
8.  alpha  :  Delta(I)@i
9.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
\mvdash{}  named-path(Delta;(A)s;(a)s;(b)s;I;alpha;z)  =  named-path(X;A;a;b;I;(s)alpha;z)


By

---

Latex:
TACTIC:((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)

---

Home Index