---

Step * of Lemma discrete-unary_wf

No Annotations
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[X:j⊢]. ∀[t:{X ⊢ _:discr(A)}].  (discrete-unary(t;x.f[x]) ∈ {X ⊢ _:discr(B)})
BY
{ PresheafMLTTInstance Obid: discrete-unary_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[X:j\mvdash{}].  \mforall{}[t:\{X  \mvdash{}  \_:discr(A)\}].
    (discrete-unary(t;x.f[x])  \mmember{}  \{X  \mvdash{}  \_:discr(B)\})


By

---

Latex:
PresheafMLTTInstance  Obid:  discrete-unary\_wf\mcdot{}

---

Home Index