---

Step * of Lemma discrete-presheaf-type_wf

No Annotations
∀[C:SmallCategory]. ∀[T:Type]. ∀[X:ps_context{j:l}(C)].  (discr(T) ∈ X ⊢ )
BY
{ (Auto THEN MemTypeCD THEN Auto THEN RepUR ``discrete-presheaf-type`` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[T:Type].  \mforall{}[X:ps\_context\{j:l\}(C)].    (discr(T)  \mmember{}  X  \mvdash{}  )


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto  THEN  RepUR  ``discrete-presheaf-type``  0  THEN  Auto)

---

Home Index