---

Step * of Lemma pscm-comp-context-map

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

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

2
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. I1 : cat-ob(C)
⊢ (sigma o <rho> I1) = (<(sigma)rho> I1) ∈ (Yoneda(I)(I1) ⟶ Gamma(I1))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[Gamma,Delta:ps\_context\{j:l\}(C)].  \mforall{}[sigma:psc\_map\{j:l\}(C;  Delta;  Gamma)].
\mforall{}[I:cat-ob(C)].  \mforall{}[rho:Delta(I)].
    (sigma  o  <rho>  =  <(sigma)rho>)


By

---

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

---

Home Index