---

Step * 2 2 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,y:cat-ob(C). ∀f:cat-arrow(C) y x.  ((arrow(b) x y f) = (arrow(a) x y f) ∈ ((ob(b) x) ⟶ (ob(b) y)))
BY
{ RepeatFor 3 (ParallelLast) }

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. ∀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)))
8. y : cat-ob(C)
9. ∀f:cat-arrow(C) y x. ((arrow(a) x y f) = (arrow(b) x y f) ∈ ((ob(a) x) ⟶ (ob(a) y)))
10. f : cat-arrow(C) y x
11. (arrow(a) x y f) = (arrow(b) x y f) ∈ ((ob(a) x) ⟶ (ob(a) y))
⊢ (arrow(b) x y f) = (arrow(a) x y f) ∈ ((ob(b) x) ⟶ (ob(b) y))

---

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,y:cat-ob(C).  \mforall{}f:cat-arrow(C)  y  x.    ((arrow(b)  x  y  f)  =  (arrow(a)  x  y  f))


By

---

Latex:
RepeatFor  3  (ParallelLast)

---

Home Index