---

Step * 3 1 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))@i
6. p1 : A A@0@i
7. A1 : cat-ob(op-cat(C))@i
8. q1 : A A1@i
9. A2 : cat-ob(op-cat(C))@i
10. z1 : A A2@i
11. f : cat-arrow(op-cat(C)) A1 A@0@i
12. (A A1 A@0 f q1) = p1 ∈ (A A@0)
13. g : cat-arrow(op-cat(C)) A2 A1@i
14. (A A2 A1 g z1) = q1 ∈ (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| (B A2 A@0 f (m A2 z1)) = (m A@0 p1) ∈ (B A@0)} 
BY
{ (At ⌜Type⌝ EqTypeCD⋅ THEN Auto) }

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


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  EqTypeCD\mcdot{}  THEN  Auto)

---

Home Index