Step * 1 of Lemma ext-equal-presheaves_wf


1. SmallCategory
2. Presheaf(C)
3. Presheaf(C)
4. ∀x:cat-ob(C). ob(F) x ≡ ob(G) x
5. cat-ob(C)
6. cat-ob(C)
7. cat-arrow(C) x
⊢ arrow(G) f ∈ (ob(F) x) ⟶ (ob(F) y)
BY
((DoSubsume THEN Auto) THEN RepUR ``type-cat`` 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