---

Step * 2 1 of Lemma cubical-sigma_wf


1. X : 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 I a) ⟶ (A1 J f(a))
4. ∀I:Cname List. ∀a:X(I). ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a))
5. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
     ((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a)))
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 I a) ⟶ (A@0 J f(a))
8. ∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A@0 I a.  ((B1 I I 1 a u) = u ∈ (A@0 I 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 I a.
     ((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u)) ∈ (A@0 K (f o g)(a)))
10. ∀I:Cname List. ∀a:X(I). ∀u:u:<A1, A2>(a) × <A@0, B1>((a;u)).
      (<(fst(u) a 1), (snd(u) (a;fst(u)) 1)> = u ∈ (u:<A1, A2>(a) × <A@0, B1>((a;u))))
11. I : Cname List
12. J : Cname List
13. K : Cname List
14. f : name-morph(I;J)
15. g : name-morph(J;K)
16. a : X(I)
17. u : u:<A1, A2>(a) × <A@0, B1>((a;u))
18. X ⊢ <A1, A2>
⊢ (B1 I K (f o g) (a;fst(u)) (snd(u)))
= (B1 J K g (f(a);A2 I J f a (fst(u))) (B1 I J f (a;fst(u)) (snd(u))))
∈ (A@0 K ((f o g)(a);A2 I K (f o g) a (fst(u))))
BY
{ (RepUR ``cubical-type-at`` -2 THEN D -2 THEN Reduce 0) }

1
1. X : 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 I a) ⟶ (A1 J f(a))
4. ∀I:Cname List. ∀a:X(I). ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a))
5. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A1 I a.
     ((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a)))
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 I a) ⟶ (A@0 J f(a))
8. ∀I:Cname List. ∀a:X.<A1, A2>(I). ∀u:A@0 I a.  ((B1 I I 1 a u) = u ∈ (A@0 I 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 I a.
     ((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u)) ∈ (A@0 K (f o g)(a)))
10. ∀I:Cname List. ∀a:X(I). ∀u:u:<A1, A2>(a) × <A@0, B1>((a;u)).
      (<(fst(u) a 1), (snd(u) (a;fst(u)) 1)> = u ∈ (u:<A1, A2>(a) × <A@0, B1>((a;u))))
11. I : Cname List
12. J : Cname List
13. K : Cname List
14. f : name-morph(I;J)
15. g : name-morph(J;K)
16. a : X(I)
17. u1 : A1 I a
18. u2 : A@0 I (a;u1)
19. X ⊢ <A1, A2>
⊢ (B1 I K (f o g) (a;u1) u2)
= (B1 J K g (f(a);A2 I J f a u1) (B1 I J f (a;u1) u2))
∈ (A@0 K ((f o g)(a);A2 I K (f o g) a u1))

---

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)
5.  \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)))
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.  \mforall{}I:Cname  List.  \mforall{}a:X(I).  \mforall{}u:u:<A1,  A2>(a)  \mtimes{}  <A@0,  B1>((a;u)).
            (<(fst(u)  a  1),  (snd(u)  (a;fst(u))  1)>  =  u)
11.  I  :  Cname  List
12.  J  :  Cname  List
13.  K  :  Cname  List
14.  f  :  name-morph(I;J)
15.  g  :  name-morph(J;K)
16.  a  :  X(I)
17.  u  :  u:<A1,  A2>(a)  \mtimes{}  <A@0,  B1>((a;u))
18.  X  \mvdash{}  <A1,  A2>
\mvdash{}  (B1  I  K  (f  o  g)  (a;fst(u))  (snd(u)))
=  (B1  J  K  g  (f(a);A2  I  J  f  a  (fst(u)))  (B1  I  J  f  (a;fst(u))  (snd(u))))


By

---

Latex:
(RepUR  ``cubical-type-at``  -2  THEN  D  -2  THEN  Reduce  0)

---

Home Index