---

Step * of Lemma I-path-morph-id

∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:X(I). ∀w:cubical-path(X;A;a;b;I;alpha).
  (I-path-morph(X;A;I;I;1;alpha;w) = w ∈ cubical-path(X;A;a;b;I;alpha))
BY
{ (Auto THEN quotD (-1) THEN D -3 THEN D -2 THEN Reduce 0 THEN EqTypeCD THEN Auto) }

1
.....antecedent..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. z : {z:Cname| ¬(z ∈ I)} 
8. w2 : named-path(X;A;a;b;I;alpha;z)
9. z1 : {z:Cname| ¬(z ∈ I)} 
10. w3 : named-path(X;A;a;b;I;alpha;z1)
11. path-eq(X;A;I;alpha;<z, w2>;<z1, w3>)
⊢ path-eq(X;A;I;alpha;I-path-morph(X;A;I;I;1;alpha;<z, w2>);<z1, w3>)

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.  \mforall{}I:Cname  List.  \mforall{}alpha:X(I).
\mforall{}w:cubical-path(X;A;a;b;I;alpha).
    (I-path-morph(X;A;I;I;1;alpha;w)  =  w)


By

---

Latex:
(Auto  THEN  quotD  (-1)  THEN  D  -3  THEN  D  -2  THEN  Reduce  0  THEN  EqTypeCD  THEN  Auto)

---

Home Index