---

Step * of Lemma ps-context-map-ap-type

No Annotations
∀[C:SmallCategory]. ∀[I:cat-ob(C)]. ∀[Gamma:ps_context{j:l}(C)]. ∀[rho:Gamma(I)]. ∀[A:{Gamma ⊢ _}].
  ((A)<rho> ∈ Yoneda(I) ⊢ )
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[I:cat-ob(C)].  \mforall{}[Gamma:ps\_context\{j:l\}(C)].  \mforall{}[rho:Gamma(I)].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].
    ((A)<rho>  \mmember{}  Yoneda(I)  \mvdash{}  )


By

---

Latex:
Auto

---

Home Index