Step
*
of Lemma
path-eq-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).
    path-eq(X;A;I;alpha;p;q) 
⇐⇒ p = q ∈ I-path(X;A;a;b;I;alpha) supposing (fst(p)) = (fst(q)) ∈ Cname
BY
{ 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. path-eq(X;A;I;alpha;p;q)
⊢ p = q ∈ I-path(X;A;a;b;I;alpha)
2
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 ∈ I-path(X;A;a;b;I;alpha)
⊢ path-eq(X;A;I;alpha;p;q)
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).    path-eq(X;A;I;alpha;p;q)  \mLeftarrow{}{}\mRightarrow{}  p  =  q  supposing  (fst(p))  =  (fst(q))
By
Latex:
Auto
Home
Index