---

Step * 1 3 of Lemma presheaf-fun-family-comp

.....subterm..... T:t
3:n
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. H : cat-ob(C)
14. K : cat-ob(C)
15. h : cat-arrow(C) H J
16. g : cat-arrow(C) K H
17. u : A(h((s)f(a)))
18. (w H (cat-comp(C) H J I h f) u cat-comp(C) H J I h f((s)a) g)
= (w K (cat-comp(C) K H I g (cat-comp(C) H J I h f)) (u cat-comp(C) H J I h f((s)a) g))
∈ B(g(cat-comp(C) H J I h f((s)a)))
⊢ (w K (cat-comp(C) K J I (cat-comp(C) K H J g h) f) (u (s)h(f(a)) g))
= (w K (cat-comp(C) K H I g (cat-comp(C) H J I h f)) (u cat-comp(C) H J I h f((s)a) g))
∈ B((s)g(h(f(a))))
BY
{ (InferEqualType THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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  \mvdash{}  \_\}
10.  B  :  \{X  \mvdash{}  \_\}
11.  w  :  J:cat-ob(C)  {}\mrightarrow{}  f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:A(f((s)a))  {}\mrightarrow{}  B(f((s)a))
12.  \mforall{}J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}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)))
13.  H  :  cat-ob(C)
14.  K  :  cat-ob(C)
15.  h  :  cat-arrow(C)  H  J
16.  g  :  cat-arrow(C)  K  H
17.  u  :  A(h((s)f(a)))
18.  (w  H  (cat-comp(C)  H  J  I  h  f)  u  cat-comp(C)  H  J  I  h  f((s)a)  g)
=  (w  K  (cat-comp(C)  K  H  I  g  (cat-comp(C)  H  J  I  h  f))  (u  cat-comp(C)  H  J  I  h  f((s)a)  g))
\mvdash{}  (w  K  (cat-comp(C)  K  J  I  (cat-comp(C)  K  H  J  g  h)  f)  (u  (s)h(f(a))  g))
=  (w  K  (cat-comp(C)  K  H  I  g  (cat-comp(C)  H  J  I  h  f))  (u  cat-comp(C)  H  J  I  h  f((s)a)  g))


By

---

Latex:
(InferEqualType  THEN  Auto)

---

Home Index