Step * 1 of Lemma ps-context-map-comp2


1. SmallCategory
2. ps_context{j:l}(C)
3. cat-ob(C)
4. cat-ob(C)
5. cat-arrow(C) I
6. G(I)
7. I1 cat-ob(C)
⊢ <f(a)> I1 ∈ Yoneda(J)(I1) ⟶ G(I1)
BY
Auto }


Latex:


Latex:

1.  C  :  SmallCategory
2.  G  :  ps\_context\{j:l\}(C)
3.  I  :  cat-ob(C)
4.  J  :  cat-ob(C)
5.  f  :  cat-arrow(C)  J  I
6.  a  :  G(I)
7.  I1  :  cat-ob(C)
\mvdash{}  <f(a)>  I1  \mmember{}  Yoneda(J)(I1)  {}\mrightarrow{}  G(I1)


By


Latex:
Auto




Home Index