---

Step * 2 2 of Lemma cubical-type-ap-rename-one-equal


1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. x : Cname
5. y : Cname
6. a : X([x / I])
7. u : A(a)
8. v : A(a)
9. ¬(y ∈ I)
10. ¬(x ∈ I)
11. (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a))
12. (rename-one-name(x;y) o rename-one-name(y;x)) = 1 ∈ name-morph([x / I];[x / I])
13. ((u a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x))
= ((v a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x))
∈ A(a)
⊢ u = v ∈ A(a)
BY
{ ((NthHypEq  (-1) THEN EqCD) THEN Auto) }

1
.....subterm..... T:t
2:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. x : Cname
5. y : Cname
6. a : X([x / I])
7. u : A(a)
8. v : A(a)
9. ¬(y ∈ I)
10. ¬(x ∈ I)
11. (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a))
12. (rename-one-name(x;y) o rename-one-name(y;x)) = 1 ∈ name-morph([x / I];[x / I])
13. ((u a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x))
= ((v a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x))
∈ A(a)
⊢ u = ((u a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x)) ∈ A(a)

2
.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. x : Cname
5. y : Cname
6. a : X([x / I])
7. u : A(a)
8. v : A(a)
9. ¬(y ∈ I)
10. ¬(x ∈ I)
11. (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a))
12. (rename-one-name(x;y) o rename-one-name(y;x)) = 1 ∈ name-morph([x / I];[x / I])
13. ((u a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x))
= ((v a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x))
∈ A(a)
⊢ v = ((v a rename-one-name(x;y)) rename-one-name(x;y)(a) rename-one-name(y;x)) ∈ A(a)

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  I  :  Cname  List
4.  x  :  Cname
5.  y  :  Cname
6.  a  :  X([x  /  I])
7.  u  :  A(a)
8.  v  :  A(a)
9.  \mneg{}(y  \mmember{}  I)
10.  \mneg{}(x  \mmember{}  I)
11.  (u  a  rename-one-name(x;y))  =  (v  a  rename-one-name(x;y))
12.  (rename-one-name(x;y)  o  rename-one-name(y;x))  =  1
13.  ((u  a  rename-one-name(x;y))  rename-one-name(x;y)(a)  rename-one-name(y;x))
=  ((v  a  rename-one-name(x;y))  rename-one-name(x;y)(a)  rename-one-name(y;x))
\mvdash{}  u  =  v


By

---

Latex:
((NthHypEq    (-1)  THEN  EqCD)  THEN  Auto)

---

Home Index