---

Step * 3 1 of Lemma presheaf-element-map_wf


1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
5. A@0 : cat-ob(op-cat(C))
6. p1 : ob(A) A@0
7. A1 : cat-ob(op-cat(C))
8. q1 : ob(A) A1
9. A2 : cat-ob(op-cat(C))
10. z1 : ob(A) A2
11. f : {f:cat-arrow(op-cat(C)) A1 A@0| (arrow(A) A1 A@0 f q1) = p1 ∈ (ob(A) A@0)} 
12. g : {f:cat-arrow(op-cat(C)) A2 A1| (arrow(A) A2 A1 f z1) = q1 ∈ (ob(A) A1)} 
⊢ (cat-comp(el(A)) <A@0, p1> <A1, q1> <A2, z1> f g) = (cat-comp(el(B)) <A@0, m A@0 p1> <A1, m A1 q1> <A2, m A2 z1> f g) \000C∈ (cat-arrow(el(B)) <A@0, m A@0 p1> <A2, m A2 z1>)
BY
{ (D -2 THEN D -1 THEN RepUR ``presheaf-elements mk-cat`` 0) }

1
1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
5. A@0 : cat-ob(op-cat(C))
6. p1 : ob(A) A@0
7. A1 : cat-ob(op-cat(C))
8. q1 : ob(A) A1
9. A2 : cat-ob(op-cat(C))
10. z1 : ob(A) A2
11. f : cat-arrow(op-cat(C)) A1 A@0
12. (arrow(A) A1 A@0 f q1) = p1 ∈ (ob(A) A@0)
13. g : cat-arrow(op-cat(C)) A2 A1
14. (arrow(A) A2 A1 g z1) = q1 ∈ (ob(A) A1)
⊢ (cat-comp(op-cat(C)) A2 A1 A@0 g f)
= (cat-comp(op-cat(C)) A2 A1 A@0 g f)
∈ {f:cat-arrow(op-cat(C)) A2 A@0| (arrow(B) A2 A@0 f (m A2 z1)) = (m A@0 p1) ∈ (ob(B) A@0)} 

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  A  :  Presheaf(C)
3.  B  :  Presheaf(C)
4.  m  :  A  {}\mrightarrow{}  B
5.  A@0  :  cat-ob(op-cat(C))
6.  p1  :  ob(A)  A@0
7.  A1  :  cat-ob(op-cat(C))
8.  q1  :  ob(A)  A1
9.  A2  :  cat-ob(op-cat(C))
10.  z1  :  ob(A)  A2
11.  f  :  \{f:cat-arrow(op-cat(C))  A1  A@0|  (arrow(A)  A1  A@0  f  q1)  =  p1\} 
12.  g  :  \{f:cat-arrow(op-cat(C))  A2  A1|  (arrow(A)  A2  A1  f  z1)  =  q1\} 
\mvdash{}  (cat-comp(el(A))  <A@0,  p1>  <A1,  q1>  <A2,  z1>  f  g)  =  (cat-comp(el(B))  <A@0,  m  A@0  p1>  <A1,  m  A1  q1>\000C  <A2,  m  A2  z1>  f  g)


By

---

Latex:
(D  -2  THEN  D  -1  THEN  RepUR  ``presheaf-elements  mk-cat``  0)

---

Home Index