---

Step * of Lemma Kan-filler_wf

∀[X:CubicalSet]. ∀[filler:I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I)].
  (Kan-filler(X;filler) ∈ ℙ)
BY
{ (ProveWfLemma THEN D -1 THEN Auto THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[filler:I:(Cname  List)
                                                    {}\mrightarrow{}  J:(nameset(I)  List)
                                                    {}\mrightarrow{}  x:nameset(I)
                                                    {}\mrightarrow{}  i:\mBbbN{}2
                                                    {}\mrightarrow{}  open\_box(X;I;J;x;i)
                                                    {}\mrightarrow{}  X(I)].
    (Kan-filler(X;filler)  \mmember{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma  THEN  D  -1  THEN  Auto  THEN  Unhide  THEN  Auto)

---

Home Index