Nuprl Definition : poset-cat
poset-cat(J) == <name-morph(J;[]), λf,g. ∀x:nameset(J). (↑f x ≤z g x), λf,x. Ax, λf,g,h,p,q,x. Ax>
Definitions occuring in Statement :
name-morph: name-morph(I;J),
nameset: nameset(L),
nil: [],
le_int: i ≤z j,
assert: ↑b,
all: ∀x:A. B[x],
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
axiom: Ax
Definitions occuring in definition :
name-morph: name-morph(I;J),
nil: [],
all: ∀x:A. B[x],
nameset: nameset(L),
assert: ↑b,
le_int: i ≤z j,
apply: f a,
pair: <a, b>,
lambda: λx.A[x],
axiom: Ax
FDL editor aliases :
poset-cat
Latex:
poset-cat(J) == <name-morph(J;[]), \mlambda{}f,g. \mforall{}x:nameset(J). (\muparrow{}f x \mleq{}z g x), \mlambda{}f,x. Ax, \mlambda{}f,g,h,p,q,x. Ax>
Date html generated:
2016_06_16-PM-06_51_57
Last ObjectModification:
2015_09_23-AM-09_32_53
Theory : cubical!sets
Home
Index