---

Step * 1 1 3 2 1 1 of Lemma I-path-morph-id


1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. alpha : X(I)
7. z : Cname
8. ¬(z ∈ I)
9. w2 : named-path(X;A;a;b;I;alpha;z)
10. z1 : Cname
11. ¬(z1 ∈ I)
12. w3 : named-path(X;A;a;b;I;alpha;z1)
13. (w2 iota(z)(alpha) rename-one-name(z;z1)) = w3 ∈ A(iota(z1)(alpha))
14. v : Cname
15. ¬(v ∈ I)
16. ((w2 iota(z)(alpha) 1[z:=v]) 1[z:=v](iota(z)(alpha)) rename-one-name(v;z1))
= (w2 iota(z)(alpha) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(alpha)))
17. A(iota(z1)(alpha)) = A(rename-one-name(z;z1)(iota(z)(alpha))) ∈ Type
⊢ rename-one-name(z;z1) = 1[z:=z1] ∈ name-morph([z / I];[z1 / I])
BY
{ (BLemma `rename-one-extend-id` THEN Auto) }

---

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.  z  :  Cname
8.  \mneg{}(z  \mmember{}  I)
9.  w2  :  named-path(X;A;a;b;I;alpha;z)
10.  z1  :  Cname
11.  \mneg{}(z1  \mmember{}  I)
12.  w3  :  named-path(X;A;a;b;I;alpha;z1)
13.  (w2  iota(z)(alpha)  rename-one-name(z;z1))  =  w3
14.  v  :  Cname
15.  \mneg{}(v  \mmember{}  I)
16.  ((w2  iota(z)(alpha)  1[z:=v])  1[z:=v](iota(z)(alpha))  rename-one-name(v;z1))
=  (w2  iota(z)(alpha)  (1[z:=v]  o  rename-one-name(v;z1)))
17.  A(iota(z1)(alpha))  =  A(rename-one-name(z;z1)(iota(z)(alpha)))
\mvdash{}  rename-one-name(z;z1)  =  1[z:=z1]


By

---

Latex:
(BLemma  `rename-one-extend-id`  THEN  Auto)

---

Home Index