---

Step * of Lemma cube-set-map-subtype

No Annotations
∀[A,B:j⊢].  (A j⟶ B ⊆r (I:fset(ℕ) ⟶ A(I) ⟶ B(I)))
BY
{ PresheafMLTTInstance Obid: psc-map-subtype⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:j\mvdash{}].    (A  j{}\mrightarrow{}  B  \msubseteq{}r  (I:fset(\mBbbN{})  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)))


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-map-subtype\mcdot{}

---

Home Index