---

Step * of Lemma presheaf-fun-family-comp

No Annotations
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀s:psc_map{j:l}(C; Delta; X). ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I.
∀a:Delta(I). ∀A,B:{X ⊢ _}. ∀w:presheaf-fun-family(C; X; A; B; I; (s)a).
  (λK,g. (w K (cat-comp(C) K J I g f)) ∈ presheaf-fun-family(C; X; A; B; J; (s)f(a)))
BY
{ ((UnivCD THENA Auto) THEN D -1 THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. s : psc_map{j:l}(C; Delta; X)
5. I : cat-ob(C)
6. J : cat-ob(C)
7. f : cat-arrow(C) J I
8. a : Delta(I)
9. A : {X ⊢ _}
10. B : {X ⊢ _}
11. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B(f((s)a))
12. ∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f((s)a)).
      ((w J f u f((s)a) g) = (w K (cat-comp(C) K J I g f) (u f((s)a) g)) ∈ B(g(f((s)a))))
13. J@0 : cat-ob(C)
14. K : cat-ob(C)
15. f@0 : cat-arrow(C) J@0 J
16. g : cat-arrow(C) K J@0
17. u : A(f@0((s)f(a)))
⊢ (w J@0 (cat-comp(C) J@0 J I f@0 f) u (s)f@0(f(a)) g)
= (w K (cat-comp(C) K J I (cat-comp(C) K J@0 J g f@0) f) (u (s)f@0(f(a)) g))
∈ B((s)g(f@0(f(a))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}X,Delta:ps\_context\{j:l\}(C).  \mforall{}s:psc\_map\{j:l\}(C;  Delta;  X).  \mforall{}I,J:cat-ob(C).
\mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:Delta(I).  \mforall{}A,B:\{X  \mvdash{}  \_\}.  \mforall{}w:presheaf-fun-family(C;  X;  A;  B;  I;  (s)a).
    (\mlambda{}K,g.  (w  K  (cat-comp(C)  K  J  I  g  f))  \mmember{}  presheaf-fun-family(C;  X;  A;  B;  J;  (s)f(a)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index