Step * 1 2 1 1 1 2 1 of Lemma cubical-snd_wf


1. CubicalSet
2. A1 I:(Cname List) ⟶ X(I) ⟶ Type
3. A2 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 a) ⟶ (A1 f(a))
4. (∀I:Cname List. ∀a:X(I). ∀u:A1 a.  ((A2 u) u ∈ (A1 a)))
∧ (∀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))))
5. X ⊢ <A1, A2>
6. A@0 I:(Cname List) ⟶ X.<A1, A2>(I) ⟶ Type
7. B1 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A@0 a) ⟶ (A@0 f(a))
8. ∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A@0 a.  ((B1 u) u ∈ (A@0 a))
9. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X.<A1, A2>(I). ∀u:A@0 a.
     ((B1 (f g) u) (B1 f(a) (B1 u)) ∈ (A@0 (f g)(a)))
10. I:(Cname List) ⟶ a:X(I) ⟶ (u:<A1, A2>(a) × <A@0, B1>((a;u)))
11. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).
      (<A2 (fst((p a))), B1 (a;fst((p a))) (snd((p a)))>
      (p f(a))
      ∈ (u:<A1, A2>(f(a)) × <A@0, B1>((f(a);u))))
12. p.1 ∈ {X ⊢ _:<A1, A2>}
13. Cname List
14. Cname List
15. name-morph(I;J)
16. X(I)
17. <A2 (fst((p a))), B1 ([p.1])a (snd((p a)))> (p f(a)) ∈ (u:<A1, A2>(f(a)) × <A@0, B1>((f(a);u))\000C)
⊢ (B1 ([p.1])a (snd((p a)))) (snd((p f(a)))) ∈ (A@0 ([p.1])f(a))
BY
xxxRepUR ``cubical-type-at`` -1xxx }

1
1. CubicalSet
2. A1 I:(Cname List) ⟶ X(I) ⟶ Type
3. A2 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 a) ⟶ (A1 f(a))
4. (∀I:Cname List. ∀a:X(I). ∀u:A1 a.  ((A2 u) u ∈ (A1 a)))
∧ (∀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))))
5. X ⊢ <A1, A2>
6. A@0 I:(Cname List) ⟶ X.<A1, A2>(I) ⟶ Type
7. B1 I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A@0 a) ⟶ (A@0 f(a))
8. ∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A@0 a.  ((B1 u) u ∈ (A@0 a))
9. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X.<A1, A2>(I). ∀u:A@0 a.
     ((B1 (f g) u) (B1 f(a) (B1 u)) ∈ (A@0 (f g)(a)))
10. I:(Cname List) ⟶ a:X(I) ⟶ (u:<A1, A2>(a) × <A@0, B1>((a;u)))
11. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).
      (<A2 (fst((p a))), B1 (a;fst((p a))) (snd((p a)))>
      (p f(a))
      ∈ (u:<A1, A2>(f(a)) × <A@0, B1>((f(a);u))))
12. p.1 ∈ {X ⊢ _:<A1, A2>}
13. Cname List
14. Cname List
15. name-morph(I;J)
16. X(I)
17. <A2 (fst((p a))), B1 ([p.1])a (snd((p a)))> (p f(a)) ∈ (u:A1 f(a) × (A@0 (f(a);u)))
⊢ (B1 ([p.1])a (snd((p a)))) (snd((p f(a)))) ∈ (A@0 ([p.1])f(a))


Latex:


Latex:

1.  X  :  CubicalSet
2.  A1  :  I:(Cname  List)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  Type
3.  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))
4.  (\mforall{}I:Cname  List.  \mforall{}a:X(I).  \mforall{}u:A1  I  a.    ((A2  I  I  1  a  u)  =  u))
\mwedge{}  (\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))))
5.  X  \mvdash{}  <A1,  A2>
6.  A@0  :  I:(Cname  List)  {}\mrightarrow{}  X.<A1,  A2>(I)  {}\mrightarrow{}  Type
7.  B1  :  I:(Cname  List)
{}\mrightarrow{}  J:(Cname  List)
{}\mrightarrow{}  f:name-morph(I;J)
{}\mrightarrow{}  a:X.<A1,  A2>(I)
{}\mrightarrow{}  (A@0  I  a)
{}\mrightarrow{}  (A@0  J  f(a))
8.  \mforall{}I:Cname  List.  \mforall{}a:X.<A1,  A2>(I).  \mforall{}u:A@0  I  a.    ((B1  I  I  1  a  u)  =  u)
9.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}a:X.<A1,  A2>(I).  \mforall{}u:A@0  I  a.
          ((B1  I  K  (f  o  g)  a  u)  =  (B1  J  K  g  f(a)  (B1  I  J  f  a  u)))
10.  p  :  I:(Cname  List)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  (u:<A1,  A2>(a)  \mtimes{}  <A@0,  B1>((a;u)))
11.  \mforall{}I,J:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}a:X(I).
            (<A2  I  J  f  a  (fst((p  I  a))),  B1  I  J  f  (a;fst((p  I  a)))  (snd((p  I  a)))>  =  (p  J  f(a)))
12.  p.1  \mmember{}  \{X  \mvdash{}  \_:<A1,  A2>\}
13.  I  :  Cname  List
14.  J  :  Cname  List
15.  f  :  name-morph(I;J)
16.  a  :  X(I)
17.  <A2  I  J  f  a  (fst((p  I  a))),  B1  I  J  f  ([p.1])a  (snd((p  I  a)))>  =  (p  J  f(a))
\mvdash{}  (B1  I  J  f  ([p.1])a  (snd((p  I  a))))  =  (snd((p  J  f(a))))


By


Latex:
xxxRepUR  ``cubical-type-at``  -1xxx




Home Index