---

Step * of Lemma cubical-subset-I_cube

∀[I,psi,J:Top].  (I,psi(J) ~ {f:J ⟶ I| (psi f) = 1} )
BY
{ (Auto THEN RepUR ``cubical-subset I_cube functor-ob rep-sub-sheaf cat-arrow cube-cat`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,psi,J:Top].    (I,psi(J)  \msim{}  \{f:J  {}\mrightarrow{}  I|  (psi  f)  =  1\}  )


By

---

Latex:
(Auto  THEN  RepUR  ``cubical-subset  I\_cube  functor-ob  rep-sub-sheaf  cat-arrow  cube-cat``  0  THEN  Auto)

---

Home Index