---

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

.....set predicate..... 
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
⊢ (B A@0 A@0 (cat-id(op-cat(C)) A@0) (m A@0 p1)) = (m A@0 p1) ∈ (B A@0)
BY
{ (InstLemma `functor-arrow-id` [⌜parm{i'}⌝;⌜op-cat(C)⌝;⌜TypeCat⌝;⌜B⌝;⌜A@0⌝]⋅ THENA Auto) }

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. (B A@0 A@0 (cat-id(op-cat(C)) A@0)) = (cat-id(TypeCat) (B A@0)) ∈ (cat-arrow(TypeCat) (B A@0) (B A@0))
⊢ (B A@0 A@0 (cat-id(op-cat(C)) A@0) (m A@0 p1)) = (m A@0 p1) ∈ (B A@0)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  C  :  SmallCategory
2.  A  :  Presheaf(C)
3.  B  :  Presheaf(C)
4.  m  :  A  {}\mrightarrow{}  B
5.  A@0  :  cat-ob(op-cat(C))@i
6.  p1  :  A  A@0@i
\mvdash{}  (B  A@0  A@0  (cat-id(op-cat(C))  A@0)  (m  A@0  p1))  =  (m  A@0  p1)


By

---

Latex:
(InstLemma  `functor-arrow-id`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}op-cat(C)\mkleeneclose{};\mkleeneopen{}TypeCat\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A@0\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index