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:ob(F) I. (P[I; rho] ⇒ P[J; arrow(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 :
functor-arrow: arrow(F),
apply: f a,
implies: P ⇒ Q,
functor-ob: ob(F),
all: ∀x:A. B[x],
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C)
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:ob(F) I. (P[I; rho] {}\mRightarrow{} P[J; arrow(F) I J f rho])
Date html generated:
2017_10_05-AM-00_50_51
Last ObjectModification:
2017_10_03-PM-03_09_48
Theory : small!categories
Home
Index