---

Step * of Lemma csm-I-path

No Annotations
∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:Delta(I).
  (I-path(Delta;(A)s;(a)s;(b)s;I;alpha) = I-path(X;A;a;b;I;(s)alpha) ∈ Type)
BY
{ (Auto THEN RepUR ``I-path`` 0 THEN EqCD THEN Auto) }

1
.....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

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Delta:CubicalSet.  \mforall{}s:Delta  {}\mrightarrow{}  X.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.  \mforall{}I:Cname  List.  \mforall{}alpha:Delta(I).
    (I-path(Delta;(A)s;(a)s;(b)s;I;alpha)  =  I-path(X;A;a;b;I;(s)alpha))


By

---

Latex:
(Auto  THEN  RepUR  ``I-path``  0  THEN  EqCD  THEN  Auto)

---

Home Index