---

Step * 3 of Lemma presheaf-element-map_wf


1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
⊢ ∀p,q,z:cat-ob(el(A)). ∀f:cat-arrow(el(A)) p q. ∀g:cat-arrow(el(A)) q z.
    ((cat-comp(el(A)) p q z f g)
    = (cat-comp(el(B)) let I,a = p in <I, m I a> let I,a = q in <I, m I a> let I,a = z in <I, m I a> f g)
    ∈ (cat-arrow(el(B)) let I,a = p in <I, m I a> let I,a = z in <I, m I a>))
BY
{ (RepeatFor 3 (((D 0 THENA Auto) THEN D -1 THEN Reduce 0))
   THEN RepeatFor 2 (((D 0 THENA (Auto THEN RepUR ``presheaf-elements mk-cat`` 0 THEN Auto))
                      THEN RepUR ``presheaf-elements mk-cat`` -1
                      ))
   ) }

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
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 : {f:cat-arrow(op-cat(C)) A1 A@0| (A A1 A@0 f q1) = p1 ∈ (A A@0)} @i
12. g : {f:cat-arrow(op-cat(C)) A2 A1| (A A2 A1 f z1) = q1 ∈ (A A1)} @i
⊢ (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>)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  A  :  Presheaf(C)
3.  B  :  Presheaf(C)
4.  m  :  A  {}\mrightarrow{}  B
\mvdash{}  \mforall{}p,q,z:cat-ob(el(A)).  \mforall{}f:cat-arrow(el(A))  p  q.  \mforall{}g:cat-arrow(el(A))  q  z.
        ((cat-comp(el(A))  p  q  z  f  g)
        =  (cat-comp(el(B))  let  I,a  =  p  in  <I,  m  I  a>  let  I,a  =  q  in  <I,  m  I  a> 
              let  I,a  =  z 
              in  <I,  m  I  a> 
              f 
              g))


By

---

Latex:
(RepeatFor  3  (((D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0))
  THEN  RepeatFor  2  (((D  0  THENA  (Auto  THEN  RepUR  ``presheaf-elements  mk-cat``  0  THEN  Auto))
                                        THEN  RepUR  ``presheaf-elements  mk-cat``  -1
                                        ))
  )

---

Home Index