Step
*
1
1
of Lemma
csm-ap-cubical-app
.....subterm..... T:t
1:n
1. X : CubicalSet
2. X1 : L:(Cname List) ⟶ Type
3. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
4. let X,F = <X1, D1>
in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((F I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
5. A1 : I:(Cname List) ⟶ ((fst(X)) I) ⟶ Type
6. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:((fst(X)) I) ⟶ (A1 I a) ⟶ (A1 J f(a))
7. (∀I:Cname List. ∀a:(fst(X)) I. ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:(fst(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))))
8. A@0 : I:(Cname List) ⟶ ((fst(X.<A1, A2>)) I) ⟶ Type
9. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:((fst(X.<A1, A2>)) I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
10. (∀I:Cname List. ∀a:(fst(X.<A1, A2>)) I. ∀u:A@0 I a. ((B1 I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:(fst(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))))
11. w : I:(Cname List) ⟶ a:((fst(X)) I) ⟶ ((fst(Π<A1, A2> <A@0, B1>)) I a)
12. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:(fst(X)) I.
((λK,g. (w I a K (f o g))) = (w J f(a)) ∈ cubical-pi-family(X;<A1, A2>;<A@0, B1>;J;f(a)))
13. u : I:(Cname List) ⟶ a:((fst(X)) I) ⟶ (A1 I a)
14. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:(fst(X)) I. ((A2 I J f a (u I a)) = (u J f(a)) ∈ (A1 J f(a)))
15. s : A:(Cname List) ⟶ (X1 A) ⟶ ((fst(X)) A)
16. ∀A,B:Cname List. ∀g:name-morph(A;B). ((((snd(X)) A B g) o (s A)) = ((s B) o (D1 A B g)) ∈ ((X1 A) ⟶ ((fst(X)) B)))
17. X.<A1, A2> ⊢ <A@0, B1>
18. X ⊢ <A1, A2>
19. I : Cname List
20. a : X1 I
⊢ w I (s I a) I 1 (u I (s I a)) ∈ A@0 I <s I a, u I (s I a)>
BY
{ xxx(OnVar `s' (\h. (Fold `functor-ob` h THEN Fold `I-cube` h))⋅ THEN (GenConclTerm ⌜s I a⌝⋅ THENA Auto))xxx }
1
1. X : CubicalSet
2. X1 : L:(Cname List) ⟶ Type
3. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
4. let X,F = <X1, D1>
in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((F I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
5. A1 : I:(Cname List) ⟶ ((fst(X)) I) ⟶ Type
6. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:((fst(X)) I) ⟶ (A1 I a) ⟶ (A1 J f(a))
7. (∀I:Cname List. ∀a:(fst(X)) I. ∀u:A1 I a. ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:(fst(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))))
8. A@0 : I:(Cname List) ⟶ ((fst(X.<A1, A2>)) I) ⟶ Type
9. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:((fst(X.<A1, A2>)) I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
10. (∀I:Cname List. ∀a:(fst(X.<A1, A2>)) I. ∀u:A@0 I a. ((B1 I I 1 a u) = u ∈ (A@0 I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:(fst(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))))
11. w : I:(Cname List) ⟶ a:((fst(X)) I) ⟶ ((fst(Π<A1, A2> <A@0, B1>)) I a)
12. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:(fst(X)) I.
((λK,g. (w I a K (f o g))) = (w J f(a)) ∈ cubical-pi-family(X;<A1, A2>;<A@0, B1>;J;f(a)))
13. u : I:(Cname List) ⟶ a:((fst(X)) I) ⟶ (A1 I a)
14. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:(fst(X)) I. ((A2 I J f a (u I a)) = (u J f(a)) ∈ (A1 J f(a)))
15. s : A:(Cname List) ⟶ (X1 A) ⟶ X(A)
16. ∀A,B:Cname List. ∀g:name-morph(A;B). ((((snd(X)) A B g) o (s A)) = ((s B) o (D1 A B g)) ∈ ((X1 A) ⟶ ((fst(X)) B)))
17. X.<A1, A2> ⊢ <A@0, B1>
18. X ⊢ <A1, A2>
19. I : Cname List
20. a : X1 I
21. v : X(I)
22. (s I a) = v ∈ X(I)
⊢ w I v I 1 (u I v) ∈ A@0 I <v, u I v>
Latex:
Latex:
.....subterm..... T:t
1:n
1. X : CubicalSet
2. X1 : L:(Cname List) {}\mrightarrow{} Type
3. D1 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} name-morph(I;J) {}\mrightarrow{} (X1 I) {}\mrightarrow{} (X1 J)
4. let X,F = <X1, D1>
in (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K).
((F I K (f o g)) = ((F J K g) o (F I J f))))
\mwedge{} (\mforall{}I:Cname List. ((F I I 1) = (\mlambda{}x.x)))
5. A1 : I:(Cname List) {}\mrightarrow{} ((fst(X)) I) {}\mrightarrow{} Type
6. A2 : I:(Cname List)
{}\mrightarrow{} J:(Cname List)
{}\mrightarrow{} f:name-morph(I;J)
{}\mrightarrow{} a:((fst(X)) I)
{}\mrightarrow{} (A1 I a)
{}\mrightarrow{} (A1 J f(a))
7. (\mforall{}I:Cname List. \mforall{}a:(fst(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:(fst(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@0 : I:(Cname List) {}\mrightarrow{} ((fst(X.<A1, A2>)) I) {}\mrightarrow{} Type
9. B1 : I:(Cname List)
{}\mrightarrow{} J:(Cname List)
{}\mrightarrow{} f:name-morph(I;J)
{}\mrightarrow{} a:((fst(X.<A1, A2>)) I)
{}\mrightarrow{} (A@0 I a)
{}\mrightarrow{} (A@0 J f(a))
10. (\mforall{}I:Cname List. \mforall{}a:(fst(X.<A1, A2>)) I. \mforall{}u:A@0 I a. ((B1 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:(fst(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))))
11. w : I:(Cname List) {}\mrightarrow{} a:((fst(X)) I) {}\mrightarrow{} ((fst(\mPi{}<A1, A2> <A@0, B1>)) I a)
12. \mforall{}I,J:Cname List. \mforall{}f:name-morph(I;J). \mforall{}a:(fst(X)) I. ((\mlambda{}K,g. (w I a K (f o g))) = (w J f(a)))
13. u : I:(Cname List) {}\mrightarrow{} a:((fst(X)) I) {}\mrightarrow{} (A1 I a)
14. \mforall{}I,J:Cname List. \mforall{}f:name-morph(I;J). \mforall{}a:(fst(X)) I. ((A2 I J f a (u I a)) = (u J f(a)))
15. s : A:(Cname List) {}\mrightarrow{} (X1 A) {}\mrightarrow{} ((fst(X)) A)
16. \mforall{}A,B:Cname List. \mforall{}g:name-morph(A;B). ((((snd(X)) A B g) o (s A)) = ((s B) o (D1 A B g)))
17. X.<A1, A2> \mvdash{} <A@0, B1>
18. X \mvdash{} <A1, A2>
19. I : Cname List
20. a : X1 I
\mvdash{} w I (s I a) I 1 (u I (s I a)) \mmember{} A@0 I <s I a, u I (s I a)>
By
Latex:
xxx(OnVar `s' (\mbackslash{}h. (Fold `functor-ob` h THEN Fold `I-cube` h))\mcdot{}
THEN (GenConclTerm \mkleeneopen{}s I a\mkleeneclose{}\mcdot{} THENA Auto)
)xxx
Home
Index