Step
*
1
of Lemma
pscm-comp-context-map
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)
⊢ <(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