---

Step * of Lemma csm-ap-restriction

No Annotations
∀X,Y:j⊢. ∀s:X j⟶ Y. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  (f((s)a) = (s)f(a) ∈ Y(J))
BY
{ PresheafMLTTInstance Obid: pscm-ap-restriction⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Y:j\mvdash{}.  \mforall{}s:X  j{}\mrightarrow{}  Y.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:X(I).    (f((s)a)  =  (s)f(a))


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-ap-restriction\mcdot{}

---

Home Index