---

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


1. C : SmallCategory
2. a : Presheaf(C)@i'
3. b : Presheaf(C)@i'
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)@i'
3. b : Presheaf(C)@i'
4. ∀x:cat-ob(C). a x ≡ b x
5. ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y x.  ((a x y f) = (b x y f) ∈ ((a x) ⟶ (a y)))
⊢ ∀x:cat-ob(C). b x ≡ a x

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

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  a  :  Presheaf(C)@i'
3.  b  :  Presheaf(C)@i'
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