Nuprl Definition : stable-element-predicate
stable-element-predicate(C;F;I,rho.P[I; rho]) ==
∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀rho:F I. (P[I; rho] ⇒ P[J; F I J f rho])
Definitions occuring in Statement :
functor-arrow: arrow(F),
functor-ob: ob(F),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
Definitions occuring in definition :
cat-ob: cat-ob(C),
cat-arrow: cat-arrow(C),
all: ∀x:A. B[x],
functor-ob: ob(F),
implies: P ⇒ Q,
apply: f a,
functor-arrow: arrow(F)
FDL editor aliases :
stable-element-predicate
Latex:
stable-element-predicate(C;F;I,rho.P[I; rho]) ==
\mforall{}I,J:cat-ob(C). \mforall{}f:cat-arrow(C) J I. \mforall{}rho:F I. (P[I; rho] {}\mRightarrow{} P[J; F I J f rho])
Date html generated:
2020_05_20-AM-07_57_16
Last ObjectModification:
2017_10_03-PM-03_09_48
Theory : small!categories
Home
Index