---

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


1. C : SmallCategory
2. a : Presheaf(C)
3. b : Presheaf(C)
4. ext-equal-presheaves(C;a;b)
⊢ ext-equal-presheaves(C;b;a)
BY
{ (ParallelLast THEN D -1 THEN D 0) }

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)))
⊢ ∀x:cat-ob(C). ob(b) x ≡ ob(a) x

2
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)))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  a  :  Presheaf(C)
3.  b  :  Presheaf(C)
4.  ext-equal-presheaves(C;a;b)
\mvdash{}  ext-equal-presheaves(C;b;a)


By

---

Latex:
(ParallelLast  THEN  D  -1  THEN  D  0)

---

Home Index