---

Step * 1 1 2 2 1 1 1 1 of Lemma set-path-name_wf

.....subterm..... T:t
1:n
1. X : CubicalSet@i'
2. A : {X ⊢ _}@i'
3. a : {X ⊢ _:A}@i
4. b : {X ⊢ _:A}@i
5. I : Cname List@i
6. a@0 : X(I)@i
7. (z:{z:Cname| ¬(z ∈ I)}  × named-path(X;A;a;b;I;a@0;z)) ⊆r cubical-path(X;A;a;b;I;a@0)
8. v : {x:Cname| ¬(x ∈ I)} 
9. named-path(X;A;a;b;I;1(a@0);v) ⊆r A(iota(v)(a@0))
10. z : {z:Cname| ¬(z ∈ I)} @i
11. u2 : named-path(X;A;a;b;I;a@0;z)@i
12. z1 : {z:Cname| ¬(z ∈ I)} @i
13. q1 : named-path(X;A;a;b;I;a@0;z1)@i
14. (u2 iota(z)(a@0) rename-one-name(z;z1)) = q1 ∈ A(iota(z1)(a@0))
15. ((u2 iota(z)(a@0) 1[z:=v]) 1[z:=v](iota(z)(a@0)) rename-one-name(v;z1))
= (u2 iota(z)(a@0) (1[z:=v] o rename-one-name(v;z1)))
∈ A((1[z:=v] o rename-one-name(v;z1))(iota(z)(a@0)))
⊢ A(iota(z1)(a@0)) = A((1[z:=v] o rename-one-name(v;z1))(iota(z)(a@0))) ∈ Type
BY
{ (EqCDA THEN DSetVars THEN RWO "rename-one-extend-name-morph" 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  X  :  CubicalSet@i'
2.  A  :  \{X  \mvdash{}  \_\}@i'
3.  a  :  \{X  \mvdash{}  \_:A\}@i
4.  b  :  \{X  \mvdash{}  \_:A\}@i
5.  I  :  Cname  List@i
6.  a@0  :  X(I)@i
7.  (z:\{z:Cname|  \mneg{}(z  \mmember{}  I)\}    \mtimes{}  named-path(X;A;a;b;I;a@0;z))  \msubseteq{}r  cubical-path(X;A;a;b;I;a@0)
8.  v  :  \{x:Cname|  \mneg{}(x  \mmember{}  I)\} 
9.  named-path(X;A;a;b;I;1(a@0);v)  \msubseteq{}r  A(iota(v)(a@0))
10.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\}  @i
11.  u2  :  named-path(X;A;a;b;I;a@0;z)@i
12.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\}  @i
13.  q1  :  named-path(X;A;a;b;I;a@0;z1)@i
14.  (u2  iota(z)(a@0)  rename-one-name(z;z1))  =  q1
15.  ((u2  iota(z)(a@0)  1[z:=v])  1[z:=v](iota(z)(a@0))  rename-one-name(v;z1))
=  (u2  iota(z)(a@0)  (1[z:=v]  o  rename-one-name(v;z1)))
\mvdash{}  A(iota(z1)(a@0))  =  A((1[z:=v]  o  rename-one-name(v;z1))(iota(z)(a@0)))


By

---

Latex:
(EqCDA  THEN  DSetVars  THEN  RWO  "rename-one-extend-name-morph"  0  THEN  Auto)

---

Home Index