---

Step * of Lemma presheaf-element-map_wf

∀[C:SmallCategory]. ∀[A,B:Presheaf(C)]. ∀[m:A ⟶ B].  (presheaf-element-map(m) ∈ Functor(el(A);el(B)))
BY
{ (Auto THEN Unfold `presheaf-element-map` 0 THEN BLemma `mk-functor_wf` THEN Try (Complete (RepeatFor 2 (MemCD)))) }

1
.....wf..... 
1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
⊢ λp.let I,a = p 
     in <I, m I a> ∈ cat-ob(el(A)) ⟶ cat-ob(el(B))

2
.....wf..... 
1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
⊢ λp,q,f. f ∈ x:cat-ob(el(A))
  ⟶ y:cat-ob(el(A))
  ⟶ (cat-arrow(el(A)) x y)
  ⟶ (cat-arrow(el(B)) let I,a = x in <I, m I a> let I,a = y in <I, m I a>)

3
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>))

4
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>))

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[A,B:Presheaf(C)].  \mforall{}[m:A  {}\mrightarrow{}  B].
    (presheaf-element-map(m)  \mmember{}  Functor(el(A);el(B)))


By

---

Latex:
(Auto
  THEN  Unfold  `presheaf-element-map`  0
  THEN  BLemma  `mk-functor\_wf`
  THEN  Try  (Complete  (RepeatFor  2  (MemCD))))

---

Home Index