---

Step * of Lemma cu-cube-filler-fills

∀[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)].
  Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))
BY
{ (Auto THEN Assert ⌜SqStable(Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha)))⌝⋅) }

1
.....assertion..... 
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)
⊢ SqStable(Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha)))

2
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(Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha)))
⊢ 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)].
    Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}SqStable(Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha)))\mkleeneclose{}\mcdot{})

---

Home Index