---

Step * 1 of Lemma path-eq-same-name


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)
BY
{ (DVar `p' THEN DVar `q' THEN RepUR ``path-eq`` -1 THEN Reduce (-2) THEN Eliminate ⌜z⌝⋅) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. z1 : {z:Cname| ¬(z ∈ I)} 
7. alpha : X(I)
8. z : {z:Cname| ¬(z ∈ I)} 
9. p1 : named-path(X;A;a;b;I;alpha;z1)
10. q1 : named-path(X;A;a;b;I;alpha;z1)
11. z = z1 ∈ Cname
12. (p1 iota(z1)(alpha) rename-one-name(z1;z1)) = q1 ∈ A(iota(z1)(alpha))
⊢ <z1, p1> = <z1, q1> ∈ I-path(X;A;a;b;I;alpha)

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_: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))
10.  path-eq(X;A;I;alpha;p;q)
\mvdash{}  p  =  q


By

---

Latex:
(DVar  `p'  THEN  DVar  `q'  THEN  RepUR  ``path-eq``  -1  THEN  Reduce  (-2)  THEN  Eliminate  \mkleeneopen{}z\mkleeneclose{}\mcdot{})

---

Home Index