---

Step * of Lemma constant-presheaf-type_wf

No Annotations
∀[C:SmallCategory]. ∀[X:small_ps_context{i:l}(C)]. ∀[Gamma:ps_context{j:l}(C)].  ((X) ∈ Gamma ⊢ )
BY
{ (Intros
   THEN Unhide
   THEN (Assert C ∈ SmallCategory BY
               Auto)
   THEN DCat 1
   THEN RepeatFor 2 (DVar `X')
   THEN All (RepUR ``type-cat op-cat constant-presheaf-type``)
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto
   THEN Try ((RWO "9 10" 0 THEN Auto))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:small\_ps\_context\{i:l\}(C)].  \mforall{}[Gamma:ps\_context\{j:l\}(C)].    ((X)  \mmember{}  Gamma  \mvdash{}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (Assert  C  \mmember{}  SmallCategory  BY
                          Auto)
  THEN  DCat  1
  THEN  RepeatFor  2  (DVar  `X')
  THEN  All  (RepUR  ``type-cat  op-cat  constant-presheaf-type``)
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((RWO  "9  10"  0  THEN  Auto)))

---

Home Index