---

Step * 3 1 1 1 1 of Lemma presheaf-element-map_wf


1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A@0:cat-ob(op-cat(C)) ⟶ (cat-arrow(TypeCat) (ob(A) A@0) (ob(B) A@0))
5. ∀A@0,B@0:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A@0 B@0.
     (((arrow(B) A@0 B@0 g) o (m A@0)) = ((m B@0) o (arrow(A) A@0 B@0 g)) ∈ ((ob(A) A@0) ⟶ (ob(B) B@0)))
6. A@0 : cat-ob(op-cat(C))
7. p1 : ob(A) A@0
8. A1 : cat-ob(op-cat(C))
9. q1 : ob(A) A1
10. A2 : cat-ob(op-cat(C))
11. z1 : ob(A) A2
12. f : cat-arrow(op-cat(C)) A1 A@0
13. (arrow(A) A1 A@0 f q1) = p1 ∈ (ob(A) A@0)
14. g : cat-arrow(op-cat(C)) A2 A1
15. (arrow(A) A2 A1 g z1) = q1 ∈ (ob(A) A1)
16. ((arrow(B) A2 A@0 (cat-comp(op-cat(C)) A2 A1 A@0 g f)) o (m A2))
= ((m A@0) o (arrow(A) A2 A@0 (cat-comp(op-cat(C)) A2 A1 A@0 g f)))
∈ ((ob(A) A2) ⟶ (ob(B) A@0))
⊢ (arrow(B) A2 A@0 (cat-comp(op-cat(C)) A2 A1 A@0 g f) (m A2 z1)) = (m A@0 p1) ∈ (ob(B) A@0)
BY
{ (ApFunToHypEquands `Z' ⌜Z z1⌝ ⌜ob(B) A@0⌝ (-1)⋅ THENA Auto) }

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


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}Z  z1\mkleeneclose{}  \mkleeneopen{}ob(B)  A@0\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)

---

Home Index