Step
*
2
1
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. 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))
BY
{ (InstHyp [⌜I⌝;⌜J⌝;⌜K⌝;⌜f⌝;⌜g⌝;⌜(a;u1)⌝;⌜u2⌝] 9⋅ THENA Auto) }
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>
20. (B1 I K (f o g) (a;u1) u2) = (B1 J K g f((a;u1)) (B1 I J f (a;u1) u2)) ∈ (A@0 K (f o g)((a;u1)))
⊢ (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. u1 : A1 I a
18. u2 : A@0 I (a;u1)
19. X \mvdash{} <A1, A2>
\mvdash{} (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))
By
Latex:
(InstHyp [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}(a;u1)\mkleeneclose{};\mkleeneopen{}u2\mkleeneclose{}] 9\mcdot{} THENA Auto)
Home
Index