---

Step * of Lemma ps-context-map-comp2

No Annotations
∀[C:SmallCategory]. ∀[G:ps_context{j:l}(C)]. ∀[I,J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[a:G(I)].
  (<a> o <f> = <f(a)> ∈ psc_map{[i | j]:l}(C; Yoneda(J); G))
BY
{ (Intros THEN BLemma `pscm-equal` THEN ((FunExt THENA Auto) ORELSE Auto)) }

1
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)

2
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)
⊢ (<a> o <f> I1) = (<f(a)> I1) ∈ (Yoneda(J)(I1) ⟶ G(I1))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[G:ps\_context\{j:l\}(C)].  \mforall{}[I,J:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  J  I].  \mforall{}[a:G(I)].
    (<a>  o  <f>  =  <f(a)>)


By

---

Latex:
(Intros  THEN  BLemma  `pscm-equal`  THEN  ((FunExt  THENA  Auto)  ORELSE  Auto))

---

Home Index