---

Step * 1 1 1 1 1 of Lemma presheaf-elements_wf


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)
BY
{ (RepUR ``type-cat`` -1 THEN ApFunToHypEquands `Z' ⌜Z A1⌝ ⌜P A⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

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))
\mvdash{}  (P  A  A  (cat-id(op-cat(C))  A)  A1)  =  A1


By

---

Latex:
(RepUR  ``type-cat``  -1  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z  A1\mkleeneclose{}  \mkleeneopen{}P  A\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index