---

Step * 2 1 of Lemma ext-equal-presheaves-equiv-rel


1. C : SmallCategory
2. a : Presheaf(C)
3. b : Presheaf(C)
4. ∀x:cat-ob(C). ob(a) x ≡ ob(b) x
5. ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y x.  ((arrow(a) x y f) = (arrow(b) x y f) ∈ ((ob(a) x) ⟶ (ob(a) y)))
⊢ ∀x:cat-ob(C). ob(b) x ≡ ob(a) x
BY
{ ParallelOp -2 }

1
1. C : SmallCategory
2. a : Presheaf(C)
3. b : Presheaf(C)
4. ∀x:cat-ob(C). ob(a) x ≡ ob(b) x
5. ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y x.  ((arrow(a) x y f) = (arrow(b) x y f) ∈ ((ob(a) x) ⟶ (ob(a) y)))
6. x : cat-ob(C)
7. ob(a) x ≡ ob(b) x
⊢ ob(b) x ≡ ob(a) x

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  a  :  Presheaf(C)
3.  b  :  Presheaf(C)
4.  \mforall{}x:cat-ob(C).  ob(a)  x  \mequiv{}  ob(b)  x
5.  \mforall{}x,y:cat-ob(C).  \mforall{}f:cat-arrow(C)  y  x.    ((arrow(a)  x  y  f)  =  (arrow(b)  x  y  f))
\mvdash{}  \mforall{}x:cat-ob(C).  ob(b)  x  \mequiv{}  ob(a)  x


By

---

Latex:
ParallelOp  -2

---

Home Index