Step
*
1
of Lemma
ext-equal-presheaves_wf
1. C : SmallCategory
2. F : Presheaf(C)
3. G : Presheaf(C)
4. ∀x:cat-ob(C). ob(F) x ≡ ob(G) x
5. x : cat-ob(C)
6. y : cat-ob(C)
7. f : cat-arrow(C) y x
⊢ arrow(G) x y f ∈ (ob(F) x) ⟶ (ob(F) y)
BY
{ ((DoSubsume THEN Auto) THEN RepUR ``type-cat`` 0 THEN Auto) }
Latex:
Latex:
1.  C  :  SmallCategory
2.  F  :  Presheaf(C)
3.  G  :  Presheaf(C)
4.  \mforall{}x:cat-ob(C).  ob(F)  x  \mequiv{}  ob(G)  x
5.  x  :  cat-ob(C)
6.  y  :  cat-ob(C)
7.  f  :  cat-arrow(C)  y  x
\mvdash{}  arrow(G)  x  y  f  \mmember{}  (ob(F)  x)  {}\mrightarrow{}  (ob(F)  y)
By
Latex:
((DoSubsume  THEN  Auto)  THEN  RepUR  ``type-cat``  0  THEN  Auto)
Home
Index