Step * 2 1 1 1 2 1 1 1 1 of Lemma csm-cubical-identity


1. CubicalSet
2. Delta CubicalSet
3. Delta ⟶ X
4. A1 I:(Cname List) ⟶ X(I) ⟶ Type
5. A2 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 a) ⟶ (A1 f(a))
6. ∀I:Cname List. ∀a:X(I). ∀u:A1 a.  ((A2 u) u ∈ (A1 a))
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 a.
     ((A2 (f g) u) (A2 f(a) (A2 u)) ∈ (A1 (f g)(a)))
8. {X ⊢ _:<A1, A2>}
9. {X ⊢ _:<A1, A2>}
10. X ⊢ <A1, A2>
11. Delta ⊢ (<A1, A2>)s
12. Cname List
13. Cname List
14. name-morph(I;J)
15. a1 Delta(I)
16. {z:Cname| ¬(z ∈ I)} 
17. u2 : <A1, A2>(iota(z)((s)a1))
18. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z;u2)
19. z1 {z:Cname| ¬(z ∈ I)} 
20. u3 : <A1, A2>(iota(z1)((s)a1))
21. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z1;u3)
22. (u2 iota(z)((s)a1) rename-one-name(z;z1)) u3 ∈ <A1, A2>(iota(z1)((s)a1))
23. X(I)
24. (s)a1 v ∈ X(I)
25. ∀[u:<A1, A2>(iota(z)(v))]
      (((u iota(z)(v) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(v)) f[z1:=fresh-cname(J)])
      (u iota(z)(v) (rename-one-name(z;z1) f[z1:=fresh-cname(J)]))
      ∈ <A1, A2>((rename-one-name(z;z1) f[z1:=fresh-cname(J)])(iota(z)(v))))
⊢ (u2 iota(z)(v) f[z:=fresh-cname(J)])
((u2 iota(z)(v) rename-one-name(z;z1)) iota(z1)(a1) f[z1:=fresh-cname(J)])
∈ <A1, A2>(iota(fresh-cname(J))((s)f(a1)))
BY
(Assert ⌜u2 ∈ <A1, A2>(iota(z)(v))⌝⋅ THENA InferEqualType) }

1
1. CubicalSet
2. Delta CubicalSet
3. Delta ⟶ X
4. A1 I:(Cname List) ⟶ X(I) ⟶ Type
5. A2 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 a) ⟶ (A1 f(a))
6. ∀I:Cname List. ∀a:X(I). ∀u:A1 a.  ((A2 u) u ∈ (A1 a))
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 a.
     ((A2 (f g) u) (A2 f(a) (A2 u)) ∈ (A1 (f g)(a)))
8. {X ⊢ _:<A1, A2>}
9. {X ⊢ _:<A1, A2>}
10. X ⊢ <A1, A2>
11. Delta ⊢ (<A1, A2>)s
12. Cname List
13. Cname List
14. name-morph(I;J)
15. a1 Delta(I)
16. {z:Cname| ¬(z ∈ I)} 
17. u2 : <A1, A2>(iota(z)((s)a1))
18. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z;u2)
19. z1 {z:Cname| ¬(z ∈ I)} 
20. u3 : <A1, A2>(iota(z1)((s)a1))
21. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z1;u3)
22. (u2 iota(z)((s)a1) rename-one-name(z;z1)) u3 ∈ <A1, A2>(iota(z1)((s)a1))
23. X(I)
24. (s)a1 v ∈ X(I)
25. ∀[u:<A1, A2>(iota(z)(v))]
      (((u iota(z)(v) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(v)) f[z1:=fresh-cname(J)])
      (u iota(z)(v) (rename-one-name(z;z1) f[z1:=fresh-cname(J)]))
      ∈ <A1, A2>((rename-one-name(z;z1) f[z1:=fresh-cname(J)])(iota(z)(v))))
⊢ <A1, A2>(iota(z)((s)a1)) = <A1, A2>(iota(z)(v)) ∈ Type

2
1. CubicalSet
2. Delta CubicalSet
3. Delta ⟶ X
4. A1 I:(Cname List) ⟶ X(I) ⟶ Type
5. A2 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 a) ⟶ (A1 f(a))
6. ∀I:Cname List. ∀a:X(I). ∀u:A1 a.  ((A2 u) u ∈ (A1 a))
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 a.
     ((A2 (f g) u) (A2 f(a) (A2 u)) ∈ (A1 (f g)(a)))
8. {X ⊢ _:<A1, A2>}
9. {X ⊢ _:<A1, A2>}
10. X ⊢ <A1, A2>
11. Delta ⊢ (<A1, A2>)s
12. Cname List
13. Cname List
14. name-morph(I;J)
15. a1 Delta(I)
16. {z:Cname| ¬(z ∈ I)} 
17. u2 : <A1, A2>(iota(z)((s)a1))
18. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z;u2)
19. z1 {z:Cname| ¬(z ∈ I)} 
20. u3 : <A1, A2>(iota(z1)((s)a1))
21. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z1;u3)
22. (u2 iota(z)((s)a1) rename-one-name(z;z1)) u3 ∈ <A1, A2>(iota(z1)((s)a1))
23. X(I)
24. (s)a1 v ∈ X(I)
25. ∀[u:<A1, A2>(iota(z)(v))]
      (((u iota(z)(v) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(v)) f[z1:=fresh-cname(J)])
      (u iota(z)(v) (rename-one-name(z;z1) f[z1:=fresh-cname(J)]))
      ∈ <A1, A2>((rename-one-name(z;z1) f[z1:=fresh-cname(J)])(iota(z)(v))))
26. <A1, A2>(iota(z)((s)a1)) = <A1, A2>(iota(z)(v)) ∈ Type
⊢ u2 ∈ <A1, A2>(iota(z)((s)a1))

3
1. CubicalSet
2. Delta CubicalSet
3. Delta ⟶ X
4. A1 I:(Cname List) ⟶ X(I) ⟶ Type
5. A2 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 a) ⟶ (A1 f(a))
6. ∀I:Cname List. ∀a:X(I). ∀u:A1 a.  ((A2 u) u ∈ (A1 a))
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 a.
     ((A2 (f g) u) (A2 f(a) (A2 u)) ∈ (A1 (f g)(a)))
8. {X ⊢ _:<A1, A2>}
9. {X ⊢ _:<A1, A2>}
10. X ⊢ <A1, A2>
11. Delta ⊢ (<A1, A2>)s
12. Cname List
13. Cname List
14. name-morph(I;J)
15. a1 Delta(I)
16. {z:Cname| ¬(z ∈ I)} 
17. u2 : <A1, A2>(iota(z)((s)a1))
18. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z;u2)
19. z1 {z:Cname| ¬(z ∈ I)} 
20. u3 : <A1, A2>(iota(z1)((s)a1))
21. name-path-endpoints(X;<A1, A2>;a;b;I;(s)a1;z1;u3)
22. (u2 iota(z)((s)a1) rename-one-name(z;z1)) u3 ∈ <A1, A2>(iota(z1)((s)a1))
23. X(I)
24. (s)a1 v ∈ X(I)
25. ∀[u:<A1, A2>(iota(z)(v))]
      (((u iota(z)(v) rename-one-name(z;z1)) rename-one-name(z;z1)(iota(z)(v)) f[z1:=fresh-cname(J)])
      (u iota(z)(v) (rename-one-name(z;z1) f[z1:=fresh-cname(J)]))
      ∈ <A1, A2>((rename-one-name(z;z1) f[z1:=fresh-cname(J)])(iota(z)(v))))
26. u2 ∈ <A1, A2>(iota(z)(v))
⊢ (u2 iota(z)(v) f[z:=fresh-cname(J)])
((u2 iota(z)(v) rename-one-name(z;z1)) iota(z1)(a1) f[z1:=fresh-cname(J)])
∈ <A1, A2>(iota(fresh-cname(J))((s)f(a1)))


Latex:


Latex:

1.  X  :  CubicalSet
2.  Delta  :  CubicalSet
3.  s  :  Delta  {}\mrightarrow{}  X
4.  A1  :  I:(Cname  List)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  Type
5.  A2  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a))
6.  \mforall{}I:Cname  List.  \mforall{}a:X(I).  \mforall{}u:A1  I  a.    ((A2  I  I  1  a  u)  =  u)
7.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}a:X(I).  \mforall{}u:A1  I  a.
          ((A2  I  K  (f  o  g)  a  u)  =  (A2  J  K  g  f(a)  (A2  I  J  f  a  u)))
8.  a  :  \{X  \mvdash{}  \_:<A1,  A2>\}
9.  b  :  \{X  \mvdash{}  \_:<A1,  A2>\}
10.  X  \mvdash{}  <A1,  A2>
11.  Delta  \mvdash{}  (<A1,  A2>)s
12.  I  :  Cname  List
13.  J  :  Cname  List
14.  f  :  name-morph(I;J)
15.  a1  :  Delta(I)
16.  z  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
17.  u2  :  <A1,  A2>(iota(z)((s)a1))
18.  name-path-endpoints(X;<A1,  A2>a;b;I;(s)a1;z;u2)
19.  z1  :  \{z:Cname|  \mneg{}(z  \mmember{}  I)\} 
20.  u3  :  <A1,  A2>(iota(z1)((s)a1))
21.  name-path-endpoints(X;<A1,  A2>a;b;I;(s)a1;z1;u3)
22.  (u2  iota(z)((s)a1)  rename-one-name(z;z1))  =  u3
23.  v  :  X(I)
24.  (s)a1  =  v
25.  \mforall{}[u:<A1,  A2>(iota(z)(v))]
            (((u  iota(z)(v)  rename-one-name(z;z1))  rename-one-name(z;z1)(iota(z)(v))  f[z1:=...])
            =  (u  iota(z)(v)  (rename-one-name(z;z1)  o  f[z1:=fresh-cname(J)])))
\mvdash{}  (u2  iota(z)(v)  f[z:=fresh-cname(J)])
=  ((u2  iota(z)(v)  rename-one-name(z;z1))  iota(z1)(a1)  f[z1:=fresh-cname(J)])


By


Latex:
(Assert  \mkleeneopen{}u2  \mmember{}  <A1,  A2>(iota(z)(v))\mkleeneclose{}\mcdot{}  THENA  InferEqualType)




Home Index