---

Step * of Lemma equal-I-paths

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].
  p = q ∈ I-path(X;A;a;b;I;alpha) 
  supposing ((fst(p)) = (fst(q)) ∈ Cname) ∧ ((snd(p)) = (snd(q)) ∈ A(iota(fst(p))(alpha)))
BY
{ (Intros
   THEN (D -3 THEN D -2)
   THEN All Reduce
   THEN RepUR ``I-path`` 0
   THEN EqCD
   THEN Auto
   THEN BLemma `equal-named-paths`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].
\mforall{}[p,q:I-path(X;A;a;b;I;alpha)].
    p  =  q  supposing  ((fst(p))  =  (fst(q)))  \mwedge{}  ((snd(p))  =  (snd(q)))


By

---

Latex:
(Intros
  THEN  (D  -3  THEN  D  -2)
  THEN  All  Reduce
  THEN  RepUR  ``I-path``  0
  THEN  EqCD
  THEN  Auto
  THEN  BLemma  `equal-named-paths`
  THEN  Auto)

---

Home Index