---

Step * of Lemma cubical-path-same-name

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].
  (((fst(p)) = (fst(q)) ∈ Cname) ⇒ (p = q ∈ cubical-path(X;A;a;b;I;alpha)) ⇒ (p = q ∈ I-path(X;A;a;b;I;alpha)))
BY
{ (Auto THEN Try ((DoSubsume THEN Auto THEN Unfold `cubical-path` 0 THEN BLemma `subtype_quotient` THEN Auto))) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. p : I-path(X;A;a;b;I;alpha)
8. q : I-path(X;A;a;b;I;alpha)
9. (fst(p)) = (fst(q)) ∈ Cname
10. p = q ∈ cubical-path(X;A;a;b;I;alpha)
⊢ p = q ∈ I-path(X;A;a;b;I;alpha)

---

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)].
    (((fst(p))  =  (fst(q)))  {}\mRightarrow{}  (p  =  q)  {}\mRightarrow{}  (p  =  q))


By

---

Latex:
(Auto
  THEN  Try  ((DoSubsume
                        THEN  Auto
                        THEN  Unfold  `cubical-path`  0
                        THEN  BLemma  `subtype\_quotient`
                        THEN  Auto))
  )

---

Home Index