Step
*
1
of Lemma
ps-context-map-comp2
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)
⊢ <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