---

Step * of Lemma cube-set-map_wf

∀[A,B:CubicalSet].  (A ⟶ B ∈ 𝕌')
BY
{ (Auto THEN Unfold `cube-set-map` 0 THEN (Assert CubicalSet ≡ Functor(NameCat;TypeCat) BY Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:CubicalSet].    (A  {}\mrightarrow{}  B  \mmember{}  \mBbbU{}')


By

---

Latex:
(Auto
  THEN  Unfold  `cube-set-map`  0
  THEN  (Assert  CubicalSet  \mequiv{}  Functor(NameCat;TypeCat)  BY
                          Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index