---

Step * of Lemma ps-context-map_wf

No Annotations
∀C:SmallCategory. ∀I:cat-ob(C). ∀Gamma:ps_context{j:l}(C). ∀rho:Gamma(I).  (<rho> ∈ psc_map{j:l}(C; Yoneda(I); Gamma))
BY
{ (ProveWfLemma
   THEN (Assert C ∈ SmallCategory BY
               Auto)
   THEN RepUR ``psc_map nat-trans`` 0
   THEN DContext 3
   THEN DCat 1
   THEN All (RepUR ``op-cat type-cat cat-ob cat-arrow Yoneda functor-ob``)
   THEN RepUR ``cat-comp functor-arrow compose`` 0
   THEN MemTypeCD
   THEN Auto
   THEN FunExt
   THEN Reduce 0
   THEN Auto
   THEN RWO "11" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}I:cat-ob(C).  \mforall{}Gamma:ps\_context\{j:l\}(C).  \mforall{}rho:Gamma(I).
    (<rho>  \mmember{}  psc\_map\{j:l\}(C;  Yoneda(I);  Gamma))


By

---

Latex:
(ProveWfLemma
  THEN  (Assert  C  \mmember{}  SmallCategory  BY
                          Auto)
  THEN  RepUR  ``psc\_map  nat-trans``  0
  THEN  DContext  3
  THEN  DCat  1
  THEN  All  (RepUR  ``op-cat  type-cat  cat-ob  cat-arrow  Yoneda  functor-ob``)
  THEN  RepUR  ``cat-comp  functor-arrow  compose``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  FunExt
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "11"  0
  THEN  Auto)

---

Home Index