---

Step * of Lemma discrete-presheaf-term_wf

No Annotations
∀[C:SmallCategory]. ∀[T:Type]. ∀[t:T]. ∀[X:ps_context{j:l}(C)].  (discr(t) ∈ {X ⊢ _:discr(T)})
BY
{ (Auto
   THEN RepUR ``discrete-presheaf-term discrete-presheaf-type`` 0
   THEN MemTypeCD
   THEN All (\h. RepUR ``presheaf-type-at presheaf-type-ap-morph`` h)⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``discrete-presheaf-term  discrete-presheaf-type``  0
  THEN  MemTypeCD
  THEN  All  (\mbackslash{}h.  RepUR  ``presheaf-type-at  presheaf-type-ap-morph``  h)\mcdot{}
  THEN  Auto)

---

Home Index