---

Step * 2 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)))
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))
BY
{ (FunExt THENW Auto) }

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))
12. x1 : ob(b) x
⊢ (arrow(b) x y f x1) = (arrow(a) x y f x1) ∈ (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))
6.  x  :  cat-ob(C)
7.  \mforall{}y:cat-ob(C).  \mforall{}f:cat-arrow(C)  y  x.    ((arrow(a)  x  y  f)  =  (arrow(b)  x  y  f))
8.  y  :  cat-ob(C)
9.  \mforall{}f:cat-arrow(C)  y  x.  ((arrow(a)  x  y  f)  =  (arrow(b)  x  y  f))
10.  f  :  cat-arrow(C)  y  x
11.  (arrow(a)  x  y  f)  =  (arrow(b)  x  y  f)
\mvdash{}  (arrow(b)  x  y  f)  =  (arrow(a)  x  y  f)


By

---

Latex:
(FunExt  THENW  Auto)

---

Home Index