Step * 1 1 1 1 of Lemma I-path-morph_functionality


1. CubicalSet
2. {X ⊢ _}
3. {X ⊢ _:A}
4. {X ⊢ _:A}
5. Cname List
6. Cname List
7. name-morph(I;K)
8. alpha X(I)
9. {z:Cname| ¬(z ∈ I)} 
10. p1 named-path(X;A;a;b;I;alpha;z)
11. z1 {z:Cname| ¬(z ∈ I)} 
12. q1 named-path(X;A;a;b;I;alpha;z1)
13. (p1 iota(z)(alpha) rename-one-name(z;z1)) q1 ∈ A(iota(z1)(alpha))
14. Cname
15. ¬(v ∈ K)
16. ∀z:Cname. rename-one-name(z;z) 1 ∈ name-morph([z K];[z K]) supposing ¬(z ∈ K)
17. ((p1 iota(z)(alpha) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(alpha)) f[z1:=v])
(p1 iota(z)(alpha) (rename-one-name(z;z1) f[z1:=v]))
∈ A((rename-one-name(z;z1) f[z1:=v])(iota(z)(alpha)))
18. f[z:=v] (rename-one-name(z;z1) f[z1:=v]) ∈ name-morph([z I];[v K])
⊢ (f iota(v)) (iota(z) (rename-one-name(z;z1) f[z1:=v])) ∈ name-morph(I;[v K])
BY
(ApFunToHypEquands `Z' ⌜(iota(z) Z)⌝ ⌜name-morph(I;[v K])⌝ (-1)⋅ THENA Auto) }

1
1. CubicalSet
2. {X ⊢ _}
3. {X ⊢ _:A}
4. {X ⊢ _:A}
5. Cname List
6. Cname List
7. name-morph(I;K)
8. alpha X(I)
9. {z:Cname| ¬(z ∈ I)} 
10. p1 named-path(X;A;a;b;I;alpha;z)
11. z1 {z:Cname| ¬(z ∈ I)} 
12. q1 named-path(X;A;a;b;I;alpha;z1)
13. (p1 iota(z)(alpha) rename-one-name(z;z1)) q1 ∈ A(iota(z1)(alpha))
14. Cname
15. ¬(v ∈ K)
16. ∀z:Cname. rename-one-name(z;z) 1 ∈ name-morph([z K];[z K]) supposing ¬(z ∈ K)
17. ((p1 iota(z)(alpha) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(alpha)) f[z1:=v])
(p1 iota(z)(alpha) (rename-one-name(z;z1) f[z1:=v]))
∈ A((rename-one-name(z;z1) f[z1:=v])(iota(z)(alpha)))
18. f[z:=v] (rename-one-name(z;z1) f[z1:=v]) ∈ name-morph([z I];[v K])
19. (iota(z) f[z:=v]) (iota(z) (rename-one-name(z;z1) f[z1:=v])) ∈ name-morph(I;[v K])
⊢ (f iota(v)) (iota(z) (rename-one-name(z;z1) f[z1:=v])) ∈ name-morph(I;[v K])


Latex:


Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  b  :  \{X  \mvdash{}  \_:A\}
5.  I  :  Cname  List
6.  K  :  Cname  List
7.  f  :  name-morph(I;K)
8.  alpha  :  X(I)
9.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
10.  p1  :  named-path(X;A;a;b;I;alpha;z)
11.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
12.  q1  :  named-path(X;A;a;b;I;alpha;z1)
13.  (p1  iota(z)(alpha)  rename-one-name(z;z1))  =  q1
14.  v  :  Cname
15.  \mneg{}(v  \mmember{}  K)
16.  \mforall{}z:Cname.  rename-one-name(z;z)  =  1  supposing  \mneg{}(z  \mmember{}  K)
17.  ((p1  iota(z)(alpha)  rename-one-name(z;z1))  rename-one-name(z;z1)(iota(z)(alpha))  f[z1:=v])
=  (p1  iota(z)(alpha)  (rename-one-name(z;z1)  o  f[z1:=v]))
18.  f[z:=v]  =  (rename-one-name(z;z1)  o  f[z1:=v])
\mvdash{}  (f  o  iota(v))  =  (iota(z)  o  (rename-one-name(z;z1)  o  f[z1:=v]))


By


Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}(iota(z)  o  Z)\mkleeneclose{}  \mkleeneopen{}name-morph(I;[v  /  K])\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)




Home Index