---

Step * 2 of Lemma path-eq-equiv


1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. z1 : Cname
8. ¬(z1 ∈ I)
9. a1 : named-path(X;A;a;b;I;alpha;z1)
10. z : Cname
11. ¬(z ∈ I)
12. b2 : named-path(X;A;a;b;I;alpha;z)
13. (a1 iota(z1)(alpha) rename-one-name(z1;z)) = b2 ∈ A(iota(z)(alpha))
⊢ (b2 iota(z)(alpha) rename-one-name(z;z1)) = a1 ∈ A(iota(z1)(alpha))
BY
{ (StrongRevHypSubst (-1) (0) THENA 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. z1 : Cname
8. ¬(z1 ∈ I)
9. a1 : named-path(X;A;a;b;I;alpha;z1)
10. z : Cname
11. ¬(z ∈ I)
12. b2 : named-path(X;A;a;b;I;alpha;z)
13. (a1 iota(z1)(alpha) rename-one-name(z1;z)) = b2 ∈ A(iota(z)(alpha))
⊢ ((a1 iota(z1)(alpha) rename-one-name(z1;z)) iota(z)(alpha) rename-one-name(z;z1)) = a1 ∈ A(iota(z1)(alpha))

2
.....subterm..... T:t
4:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. z1 : Cname
8. ¬(z1 ∈ I)
9. a1 : named-path(X;A;a;b;I;alpha;z1)
10. z : Cname
11. ¬(z ∈ I)
12. b2 : named-path(X;A;a;b;I;alpha;z)
13. (a1 iota(z1)(alpha) rename-one-name(z1;z)) = b2 ∈ A(iota(z)(alpha))
14. z2 : A(iota(z)(alpha))
15. z2 = (a1 iota(z1)(alpha) rename-one-name(z1;z)) ∈ A(iota(z)(alpha))
⊢ (iota(z) o rename-one-name(z;z1)) = iota(z1) ∈ name-morph(I;[z1 / I])

---

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.  z1  :  Cname
8.  \mneg{}(z1  \mmember{}  I)
9.  a1  :  named-path(X;A;a;b;I;alpha;z1)
10.  z  :  Cname
11.  \mneg{}(z  \mmember{}  I)
12.  b2  :  named-path(X;A;a;b;I;alpha;z)
13.  (a1  iota(z1)(alpha)  rename-one-name(z1;z))  =  b2
\mvdash{}  (b2  iota(z)(alpha)  rename-one-name(z;z1))  =  a1


By

---

Latex:
(StrongRevHypSubst  (-1)  (0)  THENA  Auto)

---

Home Index