---

Step * of Lemma presheaf-type-ap-morph-comp-eq

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[I,J,K:cat-ob(C)]. ∀[f:cat-arrow(C) J I].
∀[g:cat-arrow(C) K J]. ∀[a:X(I)]. ∀[b:X(J)]. ∀[u:A(a)].
  ((u a f) b g) = (u a cat-comp(C) K J I g f) ∈ A(cat-comp(C) K J I g f(a)) supposing b = f(a) ∈ X(J)
BY
{ Auto }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. I : cat-ob(C)
5. J : cat-ob(C)
6. K : cat-ob(C)
7. f : cat-arrow(C) J I
8. g : cat-arrow(C) K J
9. a : X(I)
10. b : X(J)
11. u : A(a)
12. b = f(a) ∈ X(J)
⊢ ((u a f) b g) = (u a cat-comp(C) K J I g f) ∈ A(cat-comp(C) K J I g f(a))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I,J,K:cat-ob(C)].
\mforall{}[f:cat-arrow(C)  J  I].  \mforall{}[g:cat-arrow(C)  K  J].  \mforall{}[a:X(I)].  \mforall{}[b:X(J)].  \mforall{}[u:A(a)].
    ((u  a  f)  b  g)  =  (u  a  cat-comp(C)  K  J  I  g  f)  supposing  b  =  f(a)


By

---

Latex:
Auto

---

Home Index