Nuprl Definition : rep-sub-sheaf
rep-sub-sheaf(C;X;P) == <λU.{f:cat-arrow(C) U X| P U f} , λU,U',f,ux. (cat-comp(C) U' U X f ux)>
Definitions occuring in Statement :
cat-comp: cat-comp(C),
cat-arrow: cat-arrow(C),
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
set: {x:A| B[x]} ,
cat-arrow: cat-arrow(C),
lambda: λx.A[x],
apply: f a,
cat-comp: cat-comp(C)
FDL editor aliases :
rep-sub-sheaf
Latex:
rep-sub-sheaf(C;X;P) == <\mlambda{}U.\{f:cat-arrow(C) U X| P U f\} , \mlambda{}U,U',f,ux. (cat-comp(C) U' U X f ux)>
Date html generated:
2020_05_20-AM-07_53_03
Last ObjectModification:
2015_10_27-PM-01_15_42
Theory : small!categories
Home
Index