---

Step * of Lemma csm-equal

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

---

Latex:

---

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


By

---

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

---

Home Index