---

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

∀[C:SmallCategory]. EquivRel(Presheaf(C);F,G.ext-equal-presheaves(C;F;G))
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. C : SmallCategory
2. a : Presheaf(C)
⊢ ext-equal-presheaves(C;a;a)

2
1. C : SmallCategory
2. a : Presheaf(C)
3. b : Presheaf(C)
4. ext-equal-presheaves(C;a;b)
⊢ ext-equal-presheaves(C;b;a)

3
1. C : SmallCategory
2. Sym(Presheaf(C);F,G.ext-equal-presheaves(C;F;G))
3. a : Presheaf(C)
4. b : Presheaf(C)
5. c : Presheaf(C)
6. ext-equal-presheaves(C;a;b)
7. ext-equal-presheaves(C;b;c)
⊢ ext-equal-presheaves(C;a;c)

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  EquivRel(Presheaf(C);F,G.ext-equal-presheaves(C;F;G))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index