---

Step * 1 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. 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)
BY
{ (Unfold `I-path` 0
   THEN EqCD
   THEN Auto
   THEN BLemma `equal-named-paths`
   THEN Auto
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
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))
⊢ p1 = (p1 iota(z1)(alpha) rename-one-name(z1;z1)) ∈ A(iota(z1)(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.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
7.  alpha  :  X(I)
8.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  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
12.  (p1  iota(z1)(alpha)  rename-one-name(z1;z1))  =  q1
\mvdash{}  <z1,  p1>  =  <z1,  q1>


By

---

Latex:
(Unfold  `I-path`  0
  THEN  EqCD
  THEN  Auto
  THEN  BLemma  `equal-named-paths`
  THEN  Auto
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index