The Theory pcf2-defs

Parents

gst

Constants

func	GS BOOL
mk_func	GS GS GS GS
graph	GS GS
rights	GS GS
lefts	GS GS
idff	GS GS
idright	GS GS
idleft	GS GS
fields	GS GS
appg	GS GS GS
$og_f	GS GS GS
ccat	GS BOOL
ccat_const	GS GS
cfunc	GS BOOL
cfunc_const	GS GS
ccat_cfunc	GS BOOL
cfunc_ccat	GS BOOL
pf_hered	(GS BOOL) BOOL
pc_hered	(GS BOOL) BOOL
pure_functor	GS BOOL
pure_category	GS BOOL

Fixity

Right Infix 240:

og_f

Definitions

func	s func s ( d c g s = (d _g c) _g g fun g dom g = d ran g _g c)
mk_func	l g r mk_func l g r = (l _g r) _g g
lefts rights graph	f lefts f = fst (fst f) rights f = snd (fst f) graph f = snd f
idff	f idff f = mk_func f (id f) f
idleft idright	f idleft f = idff (lefts f) idright f = idff (rights f)
fields	f fields f = lefts f _g rights f
appg	f g appg f g = graph f _g g
og_f	f g f og_f g = mk_func (lefts f) (graph f o_g graph g) (rights g)
ccat	s ccat s ( t t _g s func t idleft t _g s idright t _g s ( u u _g s rights t = lefts u t og_f u _g s))
ccat_const	c ccat_const c = _g (Imagep lefts c)
cfunc	f cfunc f func f ( g g _g fields f func g) ( g h g _g lefts f h _g lefts f rights g = lefts h appg f (g og_f h) = appg f g og_f appg f h)
cfunc_const	f cfunc_const f = lefts f _g rights f
ccat_cfunc	f ccat_cfunc f cfunc f ( c c _g fields f ccat c)
cfunc_ccat	c cfunc_ccat c ccat c ( f f _g c cfunc f)
pf_hered	p pf_hered p ( f ccat_cfunc f ( g g _g cfunc_const f p g) p f)
pc_hered	p pc_hered p ( c cfunc_ccat c ( d d _g ccat_const c p d) p c)
pure_functor	s pure_functor s ( p pf_hered p p s)
pure_category	c pure_category c ( p pc_hered p p c)

V