---

Step * 1 of Lemma cube-_wf


1. I : fset(ℕ)
2. i : ℕ
⊢ cube-(I;i) ∈ A:cat-ob(op-cat(CubeCat)) ⟶ (cat-arrow(type-cat{j':l}) (formal-cube(I+i) A) (formal-cube(I).𝕀 A))
BY
{ (RepUR ``cat-ob op-cat names-cat cat-arrow type-cat functor-ob formal-cube`` 0
   THEN RepUR ``cube-context-adjoin`` 0
   THEN (RWO "interval-type-at" 0 THENA Auto)
   THEN RepUR ``interval-presheaf cube-`` 0
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN All (RepUR ``names-hom``)
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
\mvdash{}  cube-(I;i)  \mmember{}  A:cat-ob(op-cat(CubeCat))  {}\mrightarrow{}  (cat-arrow(type-cat\{j':l\})  (formal-cube(I+i)  A) 
                                                                                          (formal-cube(I).\mBbbI{}  A))


By

---

Latex:
(RepUR  ``cat-ob  op-cat  names-cat  cat-arrow  type-cat  functor-ob  formal-cube``  0
  THEN  RepUR  ``cube-context-adjoin``  0
  THEN  (RWO  "interval-type-at"  0  THENA  Auto)
  THEN  RepUR  ``interval-presheaf  cube-``  0
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  All  (RepUR  ``names-hom``)
  THEN  Auto)

---

Home Index