Nuprl Definition : ext-equal-presheaves
ext-equal-presheaves(C;F;G) ==
(∀x:cat-ob(C). F x ≡ G x) ∧ (∀x,y:cat-ob(C). ∀f:cat-arrow(C) y x. ((F x y f) = (G x y f) ∈ ((F x) ⟶ (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 :
and: P ∧ Q,
ext-eq: A ≡ B,
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
cat-arrow: cat-arrow(C),
equal: s = t ∈ T,
function: x:A ⟶ B[x],
functor-ob: ob(F),
apply: f a,
functor-arrow: arrow(F)
FDL editor aliases :
ext-equal-presheaves
Latex:
ext-equal-presheaves(C;F;G) ==
(\mforall{}x:cat-ob(C). F x \mequiv{} G x) \mwedge{} (\mforall{}x,y:cat-ob(C). \mforall{}f:cat-arrow(C) y x. ((F x y f) = (G x y f)))
Date html generated:
2020_05_20-AM-07_52_42
Last ObjectModification:
2017_10_03-PM-02_35_59
Theory : small!categories
Home
Index