---

Step * of Lemma presheaf-subset-and

No Annotations
∀[C:SmallCategory]. ∀[F:presheaf{j:l}(C)]. ∀[P,Q:I:cat-ob(C) ⟶ (F I) ⟶ ℙ].
  ext-equal-presheaves(C;F|I,rho.P[I;rho]|I,rho.Q[I;rho];F|I,rho.P[I;rho] ∧ Q[I;rho]) 
  supposing stable-element-predicate(C;F;I,rho.P[I;rho]) ∧ stable-element-predicate(C;F;I,rho.Q[I;rho])
BY
{ RepeatFor 2 (Intro) }

1
1. [C] : SmallCategory
2. [F] : presheaf{j:l}(C)
⊢ ∀[P,Q:I:cat-ob(C) ⟶ (F I) ⟶ ℙ].
    ext-equal-presheaves(C;F|I,rho.P[I;rho]|I,rho.Q[I;rho];F|I,rho.P[I;rho] ∧ Q[I;rho]) 
    supposing stable-element-predicate(C;F;I,rho.P[I;rho]) ∧ stable-element-predicate(C;F;I,rho.Q[I;rho])

2
1. C : SmallCategory
⊢ istype(presheaf{j:l}(C))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[F:presheaf\{j:l\}(C)].  \mforall{}[P,Q:I:cat-ob(C)  {}\mrightarrow{}  (F  I)  {}\mrightarrow{}  \mBbbP{}].
    ext-equal-presheaves(C;F|I,rho.P[I;rho]|I,rho.Q[I;rho];F|I,rho.P[I;rho]  \mwedge{}  Q[I;rho]) 
    supposing  stable-element-predicate(C;F;I,rho.P[I;rho])
    \mwedge{}  stable-element-predicate(C;F;I,rho.Q[I;rho])


By

---

Latex:
RepeatFor  2  (Intro)

---

Home Index