---

Step * 4 of Lemma presheaf-element-map_wf


1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
⊢ ∀p:cat-ob(el(A))
    ((cat-id(el(A)) p)
    = (cat-id(el(B)) let I,a = p in <I, m I a>)
    ∈ (cat-arrow(el(B)) let I,a = p in <I, m I a> let I,a = p in <I, m I a>))
BY
{ (RepUR ``presheaf-elements mk-cat`` 0 THEN (D 0 THENA Auto) THEN D -1 THEN Reduce 0 THEN Fold `member` 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))@i
6. p1 : A A@0@i
⊢ cat-id(op-cat(C)) A@0 ∈ {f:cat-arrow(op-cat(C)) A@0 A@0| (B A@0 A@0 f (m A@0 p1)) = (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
\mvdash{}  \mforall{}p:cat-ob(el(A)).  ((cat-id(el(A))  p)  =  (cat-id(el(B))  let  I,a  =  p  in  <I,  m  I  a>))


By

---

Latex:
(RepUR  ``presheaf-elements  mk-cat``  0
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Fold  `member`  0)

---

Home Index