Nuprl Definition : ext-equal-presheaves
ext-equal-presheaves(C;F;G) ==
(∀x:cat-ob(C). ob(F) x ≡ ob(G) x)
∧ (∀x,y:cat-ob(C). ∀f:cat-arrow(C) y x. ((arrow(F) x y f) = (arrow(G) x y f) ∈ ((ob(F) x) ⟶ (ob(F) y))))
Definitions occuring in Statement :
functor-arrow: arrow(F),
functor-ob: ob(F),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
ext-eq: A ≡ B,
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
functor-arrow: arrow(F),
apply: f a,
functor-ob: ob(F),
function: x:A ⟶ B[x],
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
all: ∀x:A. B[x],
cat-ob: cat-ob(C),
ext-eq: A ≡ B,
and: P ∧ Q
FDL editor aliases :
ext-equal-presheaves
Latex:
ext-equal-presheaves(C;F;G) ==
(\mforall{}x:cat-ob(C). ob(F) x \mequiv{} ob(G) x)
\mwedge{} (\mforall{}x,y:cat-ob(C). \mforall{}f:cat-arrow(C) y x. ((arrow(F) x y f) = (arrow(G) x y f)))
Date html generated:
2017_10_05-AM-00_46_51
Last ObjectModification:
2017_10_03-PM-02_35_59
Theory : small!categories
Home
Index