---

Step * 4 1 1 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))
6. p1 : ob(A) A@0
7. (arrow(B) A@0 A@0 (cat-id(op-cat(C)) A@0)) = (λx.x) ∈ ((ob(B) A@0) ⟶ (ob(B) A@0))
⊢ (arrow(B) A@0 A@0 (cat-id(op-cat(C)) A@0) (m A@0 p1)) = (m A@0 p1) ∈ (ob(B) A@0)
BY
{ (ApFunToHypEquands `Z' ⌜Z (m A@0 p1)⌝ ⌜ob(B) A@0⌝ (-1)⋅ THEN Auto) }

---

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.  (arrow(B)  A@0  A@0  (cat-id(op-cat(C))  A@0))  =  (\mlambda{}x.x)
\mvdash{}  (arrow(B)  A@0  A@0  (cat-id(op-cat(C))  A@0)  (m  A@0  p1))  =  (m  A@0  p1)


By

---

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

---

Home Index