---

Step * 1 1 2 2 of Lemma I-path-morph-comp

.....subterm..... T:t
2:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a@0 : X(I)
11. z : {z:Cname| ¬(z ∈ I)} 
12. u2 : named-path(X;A;a;b;I;a@0;z)
13. z1 : {z:Cname| ¬(z ∈ I)} 
14. u3 : named-path(X;A;a;b;I;a@0;z1)
15. (u2 iota(z)(a@0) rename-one-name(z;z1)) = u3 ∈ A(iota(z1)(a@0))
16. v : Cname
17. ¬(v ∈ K)
18. v1 : Cname
19. ¬(v1 ∈ J)
20. z2 : A(iota(z1)(a@0))
⊢ ((u2 iota(z)(a@0) (f o g)[z:=v]) iota(v)((f o g)(a@0)) rename-one-name(v;v)) ∈ A(iota(v)((f o g)(a@0)))
BY
{ Assert ⌜rename-one-name(v;v)(iota(v)((f o g)(a@0))) = iota(v)((f o g)(a@0)) ∈ X([v / K])⌝⋅ }

1
.....assertion..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a@0 : X(I)
11. z : {z:Cname| ¬(z ∈ I)} 
12. u2 : named-path(X;A;a;b;I;a@0;z)
13. z1 : {z:Cname| ¬(z ∈ I)} 
14. u3 : named-path(X;A;a;b;I;a@0;z1)
15. (u2 iota(z)(a@0) rename-one-name(z;z1)) = u3 ∈ A(iota(z1)(a@0))
16. v : Cname
17. ¬(v ∈ K)
18. v1 : Cname
19. ¬(v1 ∈ J)
20. z2 : A(iota(z1)(a@0))
⊢ rename-one-name(v;v)(iota(v)((f o g)(a@0))) = iota(v)((f o g)(a@0)) ∈ X([v / K])

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a@0 : X(I)
11. z : {z:Cname| ¬(z ∈ I)} 
12. u2 : named-path(X;A;a;b;I;a@0;z)
13. z1 : {z:Cname| ¬(z ∈ I)} 
14. u3 : named-path(X;A;a;b;I;a@0;z1)
15. (u2 iota(z)(a@0) rename-one-name(z;z1)) = u3 ∈ A(iota(z1)(a@0))
16. v : Cname
17. ¬(v ∈ K)
18. v1 : Cname
19. ¬(v1 ∈ J)
20. z2 : A(iota(z1)(a@0))
21. rename-one-name(v;v)(iota(v)((f o g)(a@0))) = iota(v)((f o g)(a@0)) ∈ X([v / K])
⊢ ((u2 iota(z)(a@0) (f o g)[z:=v]) iota(v)((f o g)(a@0)) rename-one-name(v;v)) ∈ A(iota(v)((f o g)(a@0)))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  I  :  Cname  List
6.  J  :  Cname  List
7.  K  :  Cname  List
8.  f  :  name-morph(I;J)
9.  g  :  name-morph(J;K)
10.  a@0  :  X(I)
11.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
12.  u2  :  named-path(X;A;a;b;I;a@0;z)
13.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
14.  u3  :  named-path(X;A;a;b;I;a@0;z1)
15.  (u2  iota(z)(a@0)  rename-one-name(z;z1))  =  u3
16.  v  :  Cname
17.  \mneg{}(v  \mmember{}  K)
18.  v1  :  Cname
19.  \mneg{}(v1  \mmember{}  J)
20.  z2  :  A(iota(z1)(a@0))
\mvdash{}  ((u2  iota(z)(a@0)  (f  o  g)[z:=v])  iota(v)((f  o  g)(a@0))  rename-one-name(v;v))
    \mmember{}  A(iota(v)((f  o  g)(a@0)))


By

---

Latex:
Assert  \mkleeneopen{}rename-one-name(v;v)(iota(v)((f  o  g)(a@0)))  =  iota(v)((f  o  g)(a@0))\mkleeneclose{}\mcdot{}

---

Home Index