Step
*
1
4
of Lemma
csm-cubical-pi-family
1. X1 : L:(Cname List) ⟶ Type
2. X2 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((X2 I K (f o g)) = (λx.(X2 J K g (X2 I J f x))) ∈ ((X1 I) ⟶ (X1 K))))
∧ (∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I))))
4. X : L:(Cname List) ⟶ Type
5. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
6. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((D1 I K (f o g)) = (λx.(D1 J K g (D1 I J f x))) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
7. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type
8. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(X1 I) ⟶ (A1 I a) ⟶ (A1 J f(a))
9. (∀I:Cname List. ∀a:X1 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:X1 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))))
10. A : I:(Cname List) ⟶ (alpha:X1 I × (A1 I alpha)) ⟶ Type
11. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(alpha:X1 I × (A1 I alpha)) ⟶ (A I a) ⟶ (A J f(a))
12. (∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀u:A I a. ((B1 I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:alpha:X1 I × (A1 I alpha). ∀u:A I a.
((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u)) ∈ (A K (f o g)(a))))
13. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)
14. ∀A,B:Cname List. ∀g:name-morph(A;B). ((λx.(X2 A B g (s A x))) = (λx.(s B (D1 A B g x))) ∈ ((X A) ⟶ (X1 B)))
15. I : Cname List
16. a : X I
17. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:(A1 J f(s I a)) ⟶ (A J <f(s I a), u>)
18. J : Cname List
19. K : Cname List
20. f : name-morph(I;J)
21. g : name-morph(J;K)
22. u : A1 J f(s I a)
23. f(s I a) = (s J f(a)) ∈ (X1 J)
⊢ (w K (f o g) (A2 J K g f(s I a) u)) = (w K (f o g) (A2 J K g (s J f(a)) u)) ∈ (A K g(<f(s I a), u>))
BY
{ TACTIC:All (RepUR ``cube-set-restriction``) }
1
1. X1 : L:(Cname List) ⟶ Type
2. X2 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((X2 I K (f o g)) = (λx.(X2 J K g (X2 I J f x))) ∈ ((X1 I) ⟶ (X1 K))))
∧ (∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I))))
4. X : L:(Cname List) ⟶ Type
5. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
6. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((D1 I K (f o g)) = (λx.(D1 J K g (D1 I J f x))) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
7. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type
8. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(X1 I) ⟶ (A1 I a) ⟶ (A1 J (X2 I J f a))
9. (∀I:Cname List. ∀a:X1 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:X1 I. ∀u:A1 I a.
((A2 I K (f o g) a u) = (A2 J K g (X2 I J f a) (A2 I J f a u)) ∈ (A1 K (X2 I K (f o g) a))))
10. A : I:(Cname List) ⟶ (alpha:X1 I × (A1 I alpha)) ⟶ Type
11. B1 : I:(Cname List)
⟶ J:(Cname List)
⟶ f:name-morph(I;J)
⟶ a:(alpha:X1 I × (A1 I alpha))
⟶ (A I a)
⟶ (A J <X2 I J f (fst(a)), A2 I J f (fst(a)) (snd(a))>)
12. (∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀u:A I a. ((B1 I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:alpha:X1 I × (A1 I alpha). ∀u:A I a.
((B1 I K (f o g) a u)
= (B1 J K g <X2 I J f (fst(a)), A2 I J f (fst(a)) (snd(a))> (B1 I J f a u))
∈ (A K <X2 I K (f o g) (fst(a)), A2 I K (f o g) (fst(a)) (snd(a))>)))
13. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)
14. ∀A,B:Cname List. ∀g:name-morph(A;B). ((λx.(X2 A B g (s A x))) = (λx.(s B (D1 A B g x))) ∈ ((X A) ⟶ (X1 B)))
15. I : Cname List
16. a : X I
17. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:(A1 J (X2 I J f (s I a))) ⟶ (A J <X2 I J f (s I a), u>)
18. J : Cname List
19. K : Cname List
20. f : name-morph(I;J)
21. g : name-morph(J;K)
22. u : A1 J (X2 I J f (s I a))
23. (X2 I J f (s I a)) = (s J (D1 I J f a)) ∈ (X1 J)
⊢ (w K (f o g) (A2 J K g (X2 I J f (s I a)) u))
= (w K (f o g) (A2 J K g (s J (D1 I J f a)) u))
∈ (A K <X2 J K g (X2 I J f (s I a)), A2 J K g (X2 I J f (s I a)) u>)
Latex:
Latex:
1. X1 : L:(Cname List) {}\mrightarrow{} Type
2. X2 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} name-morph(I;J) {}\mrightarrow{} (X1 I) {}\mrightarrow{} (X1 J)
3. (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K).
((X2 I K (f o g)) = (\mlambda{}x.(X2 J K g (X2 I J f x)))))
\mwedge{} (\mforall{}I:Cname List. ((X2 I I 1) = (\mlambda{}x.x)))
4. X : L:(Cname List) {}\mrightarrow{} Type
5. D1 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} name-morph(I;J) {}\mrightarrow{} (X I) {}\mrightarrow{} (X J)
6. (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K).
((D1 I K (f o g)) = (\mlambda{}x.(D1 J K g (D1 I J f x)))))
\mwedge{} (\mforall{}I:Cname List. ((D1 I I 1) = (\mlambda{}x.x)))
7. A1 : I:(Cname List) {}\mrightarrow{} (X1 I) {}\mrightarrow{} Type
8. A2 : I:(Cname List) {}\mrightarrow{} J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} a:(X1 I) {}\mrightarrow{} (A1 I a) {}\mrightarrow{} (A1 J f(a))
9. (\mforall{}I:Cname List. \mforall{}a:X1 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:X1 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))))
10. A : I:(Cname List) {}\mrightarrow{} (alpha:X1 I \mtimes{} (A1 I alpha)) {}\mrightarrow{} Type
11. B1 : I:(Cname List)
{}\mrightarrow{} J:(Cname List)
{}\mrightarrow{} f:name-morph(I;J)
{}\mrightarrow{} a:(alpha:X1 I \mtimes{} (A1 I alpha))
{}\mrightarrow{} (A I a)
{}\mrightarrow{} (A J f(a))
12. (\mforall{}I:Cname List. \mforall{}a:alpha:X1 I \mtimes{} (A1 I alpha). \mforall{}u:A 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:alpha:X1 I \mtimes{} (A1 I alpha).
\mforall{}u:A I a.
((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u))))
13. s : A:(Cname List) {}\mrightarrow{} (X A) {}\mrightarrow{} (X1 A)
14. \mforall{}A,B:Cname List. \mforall{}g:name-morph(A;B). ((\mlambda{}x.(X2 A B g (s A x))) = (\mlambda{}x.(s B (D1 A B g x))))
15. I : Cname List
16. a : X I
17. w : J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} u:(A1 J f(s I a)) {}\mrightarrow{} (A J <f(s I a), u>)
18. J : Cname List
19. K : Cname List
20. f : name-morph(I;J)
21. g : name-morph(J;K)
22. u : A1 J f(s I a)
23. f(s I a) = (s J f(a))
\mvdash{} (w K (f o g) (A2 J K g f(s I a) u)) = (w K (f o g) (A2 J K g (s J f(a)) u))
By
Latex:
TACTIC:All (RepUR ``cube-set-restriction``)
Home
Index