Step
*
2
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))
⊢ (B1 I J f ([u])a (w I a I 1 (u I a))) = (w J f(a) J 1 (u J f(a))) ∈ (A@0 J ([u])f(a))
BY
{ TACTIC:ApFunToHypEquands `Z' ⌜Z J 1⌝ ⌜u:A(f(a)) ⟶ <A@0, B1>((f(a);u))⌝ (-1)⋅ }
1
.....fun 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 : cubical-pi-family(X;A;<A@0, B1>;J;f(a))
⊢ (Z J 1) = (Z J 1) ∈ (u:A(f(a)) ⟶ <A@0, B1>((f(a);u)))
2
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. ((λK,g. (w I a K (f o g))) J 1) = (w J f(a) J 1) ∈ (u:A(f(a)) ⟶ <A@0, B1>((f(a);u)))
⊢ (B1 I J f ([u])a (w I a I 1 (u I a))) = (w J f(a) J 1 (u J f(a))) ∈ (A@0 J ([u])f(a))
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))
\mvdash{} (B1 I J f ([u])a (w I a I 1 (u I a))) = (w J f(a) J 1 (u J f(a)))
By
Latex:
TACTIC:ApFunToHypEquands `Z' \mkleeneopen{}Z J 1\mkleeneclose{} \mkleeneopen{}u:A(f(a)) {}\mrightarrow{} <A@0, B1>((f(a);u))\mkleeneclose{} (-1)\mcdot{}
Home
Index