---

Step * of Lemma formal-cube-singleton-iso-interval-presheaf

No Annotations
∀x:ℕ. cat-isomorphic(FUN(op-cat(CubeCat);TypeCat');formal-cube({x});𝕀)
BY
{ Auto }

1
1. x : ℕ
⊢ cat-isomorphic(FUN(op-cat(CubeCat);TypeCat');formal-cube({x});𝕀)

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbN{}.  cat-isomorphic(FUN(op-cat(CubeCat);TypeCat');formal-cube(\{x\});\mBbbI{})


By

---

Latex:
Auto

---

Home Index