---

Step * of Lemma discrete-unary_wf

No Annotations
∀[C:SmallCategory]. ∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[X:ps_context{j:l}(C)]. ∀[t:{X ⊢ _:discr(A)}].
  (discrete-unary(t;x.f[x]) ∈ {X ⊢ _:discr(B)})
BY
{ (ProveWfLemma
   THEN Unfold `presheaf-term` 0
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``discrete-presheaf-type`` 0
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma
  THEN  Unfold  `presheaf-term`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``discrete-presheaf-type``  0
  THEN  EqCDA
  THEN  Auto)

---

Home Index