---

Step * of Lemma cu-cube-filler-uniform

∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[L:Cname List]. ∀[f:name-morph(I;L)]. ∀[J:nameset(L) List]. ∀[x:nameset(L)]. ∀[i:ℕ2].
∀[box:A-open-box(unit-cube(I);Kan-type(alpha);L;f;J;x;i)].
  uniform-Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))
BY
{ (Auto
   THEN (Assert SqStable(uniform-Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))) BY
               (BLemma `sq_stable_uniform-Kan-A-filler` THEN RWW "cu-cube-family-Kan-type-at<" 0 THEN Auto))
   ) }

1
1. I : Cname List
2. alpha : c𝕌(I)
3. L : Cname List
4. f : name-morph(I;L)
5. J : nameset(L) List
6. x : nameset(L)
7. i : ℕ2
8. box : A-open-box(unit-cube(I);Kan-type(alpha);L;f;J;x;i)
9. SqStable(uniform-Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha)))
⊢ uniform-Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[alpha:c\mBbbU{}(I)].  \mforall{}[L:Cname  List].  \mforall{}[f:name-morph(I;L)].  \mforall{}[J:nameset(L)  List].
\mforall{}[x:nameset(L)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[box:A-open-box(unit-cube(I);Kan-type(alpha);L;f;J;x;i)].
    uniform-Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))


By

---

Latex:
(Auto
  THEN  (Assert  SqStable(uniform-Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha)))  BY
                          (BLemma  `sq\_stable\_uniform-Kan-A-filler`
                            THEN  RWW  "cu-cube-family-Kan-type-at<"  0
                            THEN  Auto))
  )

---

Home Index