Step
*
2
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
⊢ (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:(Assert ⌜(λK,g. (w I a K (f o g))) = (w J f(a)) ∈ cubical-pi-family(X;A;<A@0, B1>;J;f(a))⌝⋅ THENA BackThruSomeH\000Cyp) }
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))
⊢ (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
\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:(Assert \mkleeneopen{}(\mlambda{}K,g. (w I a K (f o g))) = (w J f(a))\mkleeneclose{}\mcdot{} THENA BackThruSomeHyp)
Home
Index