---

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


1. x : ℕ
⊢ cat-isomorphic(FUN(op-cat(CubeCat);TypeCat');formal-cube({x});𝕀)
BY
{ RepUR ``cat-isomorphic functor-cat cat-isomorphism`` 0 }

1
1. x : ℕ
⊢ ∃f:nat-trans(op-cat(CubeCat);TypeCat';formal-cube({x});𝕀)
   ∃g:nat-trans(op-cat(CubeCat);TypeCat';𝕀;formal-cube({x})). (fg=1 ∧ gf=1)

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
\mvdash{}  cat-isomorphic(FUN(op-cat(CubeCat);TypeCat');formal-cube(\{x\});\mBbbI{})


By

---

Latex:
RepUR  ``cat-isomorphic  functor-cat  cat-isomorphism``  0

---

Home Index