---

Step * 2 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)
⊢ (<a> o <f> I1) = (<f(a)> I1) ∈ (Yoneda(J)(I1) ⟶ G(I1))
BY
{ ((FunExt THENA Auto)
   THEN (Assert ⌜cat-comp(C) I1 J I x f(a) = x(f(a)) ∈ G(I1)⌝⋅
   THENM (NthHypSq (-1)
          THEN PscmUnfolding
          THEN RepUR ``ps-context-map Yoneda functor-arrow`` 0⋅
          THEN RepUR ``psc-restriction`` 0
          THEN Auto)
   )
   THEN 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{}  (<a>  o  <f>  I1)  =  (<f(a)>  I1)


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}cat-comp(C)  I1  J  I  x  f(a)  =  x(f(a))\mkleeneclose{}\mcdot{}
  THENM  (NthHypSq  (-1)
                THEN  PscmUnfolding
                THEN  RepUR  ``ps-context-map  Yoneda  functor-arrow``  0\mcdot{}
                THEN  RepUR  ``psc-restriction``  0
                THEN  Auto)
  )
  THEN  Auto)

---

Home Index