---

Step * of Lemma discrete-presheaf-term-at-morph

No Annotations
∀[C:SmallCategory]. ∀[T:Type]. ∀[X:ps_context{j:l}(C)]. ∀[t:{X ⊢ _:discr(T)}].
  ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  (t(a) = t(f(a)) ∈ T)
BY
{ (Auto THEN DVar `t' THEN All (RepUR ``discrete-presheaf-type``) THEN All (Fold  `presheaf-term-at`) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[T:Type].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[t:\{X  \mvdash{}  \_:discr(T)\}].
    \mforall{}I,J:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:X(I).    (t(a)  =  t(f(a)))


By

---

Latex:
(Auto
  THEN  DVar  `t'
  THEN  All  (RepUR  ``discrete-presheaf-type``)
  THEN  All  (Fold    `presheaf-term-at`)
  THEN  Auto)

---

Home Index