---

Step * 3 of Lemma pscm-presheaf-pi-family

.....subterm..... T:t
2:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {X ⊢ _}
5. B : {X.A ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
7. I : cat-ob(C)
8. a : Delta(I)
9. s o p ∈ psc_map{j:l}(C; Delta.(A)s; X)
10. q ∈ {Delta.(A)s ⊢ _:((A)s)p}
11. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B((f((s)a);u))
12. J : cat-ob(C)
13. K : cat-ob(C)
14. f : cat-arrow(C) J I
⊢ (∀g:cat-arrow(C) K J. ∀u:A(f((s)a)).
     ((w J f u (f((s)a);u) g) = (w K (cat-comp(C) K J I g f) (u f((s)a) g)) ∈ B(g((f((s)a);u)))))
= (∀g:cat-arrow(C) K J. ∀u:(A)s(f(a)).
     ((w J f u (f(a);u) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ (B)(s o p;q)(g((f(a);u)))))
∈ Type
BY
{ (RepeatFor 2 (EqCDA) THEN Try (QuickAuto)) }

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

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  Delta  :  ps\_context\{j:l\}(C)
4.  A  :  \{X  \mvdash{}  \_\}
5.  B  :  \{X.A  \mvdash{}  \_\}
6.  s  :  psc\_map\{j:l\}(C;  Delta;  X)
7.  I  :  cat-ob(C)
8.  a  :  Delta(I)
9.  s  o  p  \mmember{}  psc\_map\{j:l\}(C;  Delta.(A)s;  X)
10.  q  \mmember{}  \{Delta.(A)s  \mvdash{}  \_:((A)s)p\}
11.  w  :  J:cat-ob(C)  {}\mrightarrow{}  f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:A(f((s)a))  {}\mrightarrow{}  B((f((s)a);u))
12.  J  :  cat-ob(C)
13.  K  :  cat-ob(C)
14.  f  :  cat-arrow(C)  J  I
\mvdash{}  (\mforall{}g:cat-arrow(C)  K  J.  \mforall{}u:A(f((s)a)).
          ((w  J  f  u  (f((s)a);u)  g)  =  (w  K  (cat-comp(C)  K  J  I  g  f)  (u  f((s)a)  g))))
=  (\mforall{}g:cat-arrow(C)  K  J.  \mforall{}u:(A)s(f(a)).
          ((w  J  f  u  (f(a);u)  g)  =  (w  K  (cat-comp(C)  K  J  I  g  f)  (u  f(a)  g))))


By

---

Latex:
(RepeatFor  2  (EqCDA)  THEN  Try  (QuickAuto))

---

Home Index