---

Step * 1 4 1 1 of Lemma presheaf-elements_wf


1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
5. A2 : cat-ob(op-cat(C))
6. B1 : P A2
7. A3 : cat-ob(op-cat(C))
8. z1 : P A3
9. A4 : cat-ob(op-cat(C))
10. D1 : P A4
11. f : {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} 
12. g : {f:cat-arrow(op-cat(C)) A3 A2| (P A3 A2 f z1) = B1 ∈ (P A2)} 
13. h : {f:cat-arrow(op-cat(C)) A4 A3| (P A4 A3 f D1) = z1 ∈ (P A3)} 
14. (cat-comp(op-cat(C)) A4 A2 A (cat-comp(op-cat(C)) A4 A3 A2 h g) f)
= (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f))
∈ (cat-arrow(op-cat(C)) A4 A)
⊢ (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f))
= (cat-comp(op-cat(C)) A4 A2 A (cat-comp(op-cat(C)) A4 A3 A2 h g) f)
∈ (cat-arrow(op-cat(C)) A4 A)
BY
{ Eq }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
3.  A  :  cat-ob(op-cat(C))
4.  A1  :  P  A
5.  A2  :  cat-ob(op-cat(C))
6.  B1  :  P  A2
7.  A3  :  cat-ob(op-cat(C))
8.  z1  :  P  A3
9.  A4  :  cat-ob(op-cat(C))
10.  D1  :  P  A4
11.  f  :  \{f:cat-arrow(op-cat(C))  A2  A|  (P  A2  A  f  B1)  =  A1\} 
12.  g  :  \{f:cat-arrow(op-cat(C))  A3  A2|  (P  A3  A2  f  z1)  =  B1\} 
13.  h  :  \{f:cat-arrow(op-cat(C))  A4  A3|  (P  A4  A3  f  D1)  =  z1\} 
14.  (cat-comp(op-cat(C))  A4  A2  A  (cat-comp(op-cat(C))  A4  A3  A2  h  g)  f)
=  (cat-comp(op-cat(C))  A4  A3  A  h  (cat-comp(op-cat(C))  A3  A2  A  g  f))
\mvdash{}  (cat-comp(op-cat(C))  A4  A3  A  h  (cat-comp(op-cat(C))  A3  A2  A  g  f))
=  (cat-comp(op-cat(C))  A4  A2  A  (cat-comp(op-cat(C))  A4  A3  A2  h  g)  f)


By

---

Latex:
Eq

---

Home Index