Step * 1 of Lemma pscm-comp-context-map


1. SmallCategory
2. Gamma ps_context{j:l}(C)
3. Delta ps_context{j:l}(C)
4. sigma psc_map{j:l}(C; Delta; Gamma)
5. cat-ob(C)
6. rho Delta(I)
7. I@0 cat-ob(C)
⊢ <(sigma)rho> I@0 ∈ Yoneda(I)(I@0) ⟶ Gamma(I@0)
BY
Auto }


Latex:


Latex:

1.  C  :  SmallCategory
2.  Gamma  :  ps\_context\{j:l\}(C)
3.  Delta  :  ps\_context\{j:l\}(C)
4.  sigma  :  psc\_map\{j:l\}(C;  Delta;  Gamma)
5.  I  :  cat-ob(C)
6.  rho  :  Delta(I)
7.  I@0  :  cat-ob(C)
\mvdash{}  <(sigma)rho>  I@0  \mmember{}  Yoneda(I)(I@0)  {}\mrightarrow{}  Gamma(I@0)


By


Latex:
Auto




Home Index