Step
*
2
1
1
1
1
1
of Lemma
cubical-app_wf
1. X : CubicalSet
2. A : {X ⊢ _}
3. A@0 : I:(Cname List) ⟶ X.A(I) ⟶ Type
4. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.A(I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
5. (∀I:Cname List. ∀a:X.A(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:X.A(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))))
6. X.A ⊢ <A@0, B1>
7. w : I:(Cname List) ⟶ a:X(I) ⟶ cubical-pi-family(X;A;<A@0, B1>;I;a)
8. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I). ((λK,g. (w I a K (f o g))) = (w J f(a)) ∈ cubical-pi-family(X;A;<A@0, \000CB1>;J;f(a)))
9. u : {X ⊢ _:A}
10. I : Cname List@i
11. J : Cname List@i
12. f : name-morph(I;J)@i
13. a : X(I)@i
14. (λK,g. (w I a K (f o g))) = (w J f(a)) ∈ cubical-pi-family(X;A;<A@0, B1>;J;f(a))
15. Z : J@0:(Cname List) ⟶ f@0:name-morph(J;J@0) ⟶ u:A(f@0(f(a))) ⟶ <A@0, B1>((f@0(f(a));u))
16. ∀J@0,K:Cname List. ∀f@0:name-morph(J;J@0). ∀g:name-morph(J@0;K). ∀u:A(f@0(f(a))).
((Z J@0 f@0 u (f@0(f(a));u) g) = (Z K (f@0 o g) (u f@0(f(a)) g)) ∈ <A@0, B1>(g((f@0(f(a));u))))
⊢ Z J 1 ∈ u:A(f(a)) ⟶ <A@0, B1>((f(a);u))
BY
{ TACTIC:All (RepUR ``cubical-type-at``) }
1
1. X : CubicalSet
2. A : {X ⊢ _}
3. A@0 : I:(Cname List) ⟶ X.A(I) ⟶ Type
4. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.A(I) ⟶ (A@0 I a) ⟶ (A@0 J f(a))
5. (∀I:Cname List. ∀a:X.A(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:X.A(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))))
6. X.A ⊢ <A@0, B1>
7. w : I:(Cname List) ⟶ a:X(I) ⟶ cubical-pi-family(X;A;<A@0, B1>;I;a)
8. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I). ((λK,g. (w I a K (f o g))) = (w J f(a)) ∈ cubical-pi-family(X;A;<A@0, \000CB1>;J;f(a)))
9. u : {X ⊢ _:A}
10. I : Cname List@i
11. J : Cname List@i
12. f : name-morph(I;J)@i
13. a : X(I)@i
14. (λK,g. (w I a K (f o g))) = (w J f(a)) ∈ cubical-pi-family(X;A;<A@0, B1>;J;f(a))
15. Z : J@0:(Cname List) ⟶ f@0:name-morph(J;J@0) ⟶ u:((fst(A)) J@0 f@0(f(a))) ⟶ (A@0 J@0 (f@0(f(a));u))
16. ∀J@0,K:Cname List. ∀f@0:name-morph(J;J@0). ∀g:name-morph(J@0;K). ∀u:(fst(A)) J@0 f@0(f(a)).
((Z J@0 f@0 u (f@0(f(a));u) g) = (Z K (f@0 o g) (u f@0(f(a)) g)) ∈ (A@0 K g((f@0(f(a));u))))
⊢ Z J 1 ∈ u:((fst(A)) J f(a)) ⟶ (A@0 J (f(a);u))
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_\}
3. A@0 : I:(Cname List) {}\mrightarrow{} X.A(I) {}\mrightarrow{} Type
4. B1 : I:(Cname List)
{}\mrightarrow{} J:(Cname List)
{}\mrightarrow{} f:name-morph(I;J)
{}\mrightarrow{} a:X.A(I)
{}\mrightarrow{} (A@0 I a)
{}\mrightarrow{} (A@0 J f(a))
5. (\mforall{}I:Cname List. \mforall{}a:X.A(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:X.A(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))))
6. X.A \mvdash{} <A@0, B1>
7. w : I:(Cname List) {}\mrightarrow{} a:X(I) {}\mrightarrow{} cubical-pi-family(X;A;<A@0, B1>I;a)
8. \mforall{}I,J:Cname List. \mforall{}f:name-morph(I;J). \mforall{}a:X(I). ((\mlambda{}K,g. (w I a K (f o g))) = (w J f(a)))
9. u : \{X \mvdash{} \_:A\}
10. I : Cname List@i
11. J : Cname List@i
12. f : name-morph(I;J)@i
13. a : X(I)@i
14. (\mlambda{}K,g. (w I a K (f o g))) = (w J f(a))
15. Z : J@0:(Cname List) {}\mrightarrow{} f@0:name-morph(J;J@0) {}\mrightarrow{} u:A(f@0(f(a))) {}\mrightarrow{} <A@0, B1>((f@0(f(a));u))
16. \mforall{}J@0,K:Cname List. \mforall{}f@0:name-morph(J;J@0). \mforall{}g:name-morph(J@0;K). \mforall{}u:A(f@0(f(a))).
((Z J@0 f@0 u (f@0(f(a));u) g) = (Z K (f@0 o g) (u f@0(f(a)) g)))
\mvdash{} Z J 1 \mmember{} u:A(f(a)) {}\mrightarrow{} <A@0, B1>((f(a);u))
By
Latex:
TACTIC:All (RepUR ``cubical-type-at``)
Home
Index