---

Step * of Lemma presheaf-subset-true

∀[C:SmallCategory]. ∀[F:Presheaf(C)].  ext-equal-presheaves(C;F|True;F)
BY
{ (Auto THEN D 0 THEN Intros THEN RepUR ``presheaf-subset mk-presheaf`` 0) }

1
1. C : SmallCategory
2. F : Presheaf(C)
3. x : cat-ob(C)
⊢ {rho:ob(F) x| True}  ≡ ob(F) x

2
1. C : SmallCategory
2. F : Presheaf(C)
3. x : cat-ob(C)
4. y : cat-ob(C)
5. f : cat-arrow(C) y x
⊢ (λrho.(arrow(F) x y f rho)) = (arrow(F) x y f) ∈ ({rho:ob(F) x| True}  ⟶ {rho:ob(F) y| True} )

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[F:Presheaf(C)].    ext-equal-presheaves(C;F|True;F)


By

---

Latex:
(Auto  THEN  D  0  THEN  Intros  THEN  RepUR  ``presheaf-subset  mk-presheaf``  0)

---

Home Index