---

Step * of Lemma presheaf-it-unique

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[t:{X ⊢ _:1}].  (t = * ∈ {X ⊢ _:1})
BY
{ ((Auto THEN PresheafTermEqual)
   THEN Auto
   THEN RepUR ``presheaf-unit discrete-presheaf-type`` 0
   THEN Fold `presheaf-term-at` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[t:\{X  \mvdash{}  \_:1\}].    (t  =  *)


By

---

Latex:
((Auto  THEN  PresheafTermEqual)
  THEN  Auto
  THEN  RepUR  ``presheaf-unit  discrete-presheaf-type``  0
  THEN  Fold  `presheaf-term-at`  0
  THEN  Auto)

---

Home Index