---

Step * 1 1 1 1 of Lemma presheaf-elements_wf

.....set predicate..... 
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
⊢ (P A A (cat-id(op-cat(C)) A) A1) = A1 ∈ (P A)
BY
{ (InstLemma `functor-arrow-id` [⌜parm{i'}⌝;⌜op-cat(C)⌝;⌜TypeCat⌝;⌜P⌝;⌜A⌝]⋅ THENA Auto) }

1
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
5. (P A A (cat-id(op-cat(C)) A)) = (cat-id(TypeCat) (P A)) ∈ (cat-arrow(TypeCat) (P A) (P A))
⊢ (P A A (cat-id(op-cat(C)) A) A1) = A1 ∈ (P A)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
3.  A  :  cat-ob(op-cat(C))
4.  A1  :  P  A
\mvdash{}  (P  A  A  (cat-id(op-cat(C))  A)  A1)  =  A1


By

---

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

---

Home Index