---

Step * of Lemma presheaf-subset-true

No Annotations
∀[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)@i
⊢ {rho:F x| True}  ≡ F x

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

---

Latex:

---

Latex:
No  Annotations
\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