---

Step * of Lemma presheaf-term-at-comp

No Annotations
∀C:SmallCategory. ∀Gamma:ps_context{j:l}(C). ∀T:{Gamma ⊢ _}. ∀t:{Gamma ⊢ _:T}. ∀I:cat-ob(C). ∀rho:Gamma(I).
∀J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀K:cat-ob(C). ∀g:cat-arrow(C) K J.
  (t(cat-comp(C) K J I g f(rho)) = t(g(f(rho))) ∈ T(g(f(rho))))
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}Gamma:ps\_context\{j:l\}(C).  \mforall{}T:\{Gamma  \mvdash{}  \_\}.  \mforall{}t:\{Gamma  \mvdash{}  \_:T\}.  \mforall{}I:cat-ob(C).
\mforall{}rho:Gamma(I).  \mforall{}J:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}K:cat-ob(C).  \mforall{}g:cat-arrow(C)  K  J.
    (t(cat-comp(C)  K  J  I  g  f(rho))  =  t(g(f(rho))))


By

---

Latex:
Auto

---

Home Index