Step
*
1
1
1
1
of Lemma
csm-ap-cubical-snd
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. p : I:(Cname List) ⟶ a:((fst(X)) I) ⟶ (u:A1 I a × (A@0 I (a;u)))
12. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:(fst(X)) I.
(<(fst((p I a)) a f), (snd((p I a)) (a;fst((p I a))) f)> = (p J f(a)) ∈ (u:A1 J f(a) × (A@0 J (f(a);u))))
13. s : A:(Cname List) ⟶ (X1 A) ⟶ X(A)
14. ∀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)))
15. X.<A1, A2> ⊢ <A@0, B1>
16. X ⊢ <A1, A2>
17. I : Cname List
18. a : X1 I
19. v : X(I)
20. (s I a) = v ∈ X(I)
21. v1 : u:A1 I v × (A@0 I (v;u))
22. (p I v) = v1 ∈ (u:A1 I v × (A@0 I (v;u)))
⊢ snd(v1) ∈ A@0 I <v, fst(v1)>
BY
{ TACTIC:(D -2 THEN Reduce 0) }
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. p : I:(Cname List) ⟶ a:((fst(X)) I) ⟶ (u:A1 I a × (A@0 I (a;u)))
12. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:(fst(X)) I.
(<(fst((p I a)) a f), (snd((p I a)) (a;fst((p I a))) f)> = (p J f(a)) ∈ (u:A1 J f(a) × (A@0 J (f(a);u))))
13. s : A:(Cname List) ⟶ (X1 A) ⟶ X(A)
14. ∀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)))
15. X.<A1, A2> ⊢ <A@0, B1>
16. X ⊢ <A1, A2>
17. I : Cname List
18. a : X1 I
19. v : X(I)
20. (s I a) = v ∈ X(I)
21. u : A1 I v
22. v2 : A@0 I (v;u)
23. (p I v) = <u, v2> ∈ (u:A1 I v × (A@0 I (v;u)))
⊢ v2 ∈ A@0 I <v, u>
Latex:
Latex:
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. p : I:(Cname List) {}\mrightarrow{} a:((fst(X)) I) {}\mrightarrow{} (u:A1 I a \mtimes{} (A@0 I (a;u)))
12. \mforall{}I,J:Cname List. \mforall{}f:name-morph(I;J). \mforall{}a:(fst(X)) I.
(<(fst((p I a)) a f), (snd((p I a)) (a;fst((p I a))) f)> = (p J f(a)))
13. s : A:(Cname List) {}\mrightarrow{} (X1 A) {}\mrightarrow{} X(A)
14. \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)))
15. X.<A1, A2> \mvdash{} <A@0, B1>
16. X \mvdash{} <A1, A2>
17. I : Cname List
18. a : X1 I
19. v : X(I)
20. (s I a) = v
21. v1 : u:A1 I v \mtimes{} (A@0 I (v;u))
22. (p I v) = v1
\mvdash{} snd(v1) \mmember{} A@0 I <v, fst(v1)>
By
Latex:
TACTIC:(D -2 THEN Reduce 0)
Home
Index