---

Step * of Lemma csm-equal2

No Annotations
∀[A,B:j⊢]. ∀[f,g:A j⟶ B].  f = g ∈ A j⟶ B supposing ∀K:fset(ℕ). ∀x:A(K).  ((f K x) = (g K x) ∈ B(K))
BY
{ PresheafMLTTInstance Obid: pscm-equal2⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:j\mvdash{}].  \mforall{}[f,g:A  j{}\mrightarrow{}  B].    f  =  g  supposing  \mforall{}K:fset(\mBbbN{}).  \mforall{}x:A(K).    ((f  K  x)  =  (g  K  x))


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-equal2\mcdot{}

---

Home Index