The Theory pcf-defs
Parents

gst
Constants
func
'a GS BOOL
mk_func
'a GS 'a GS 'a GS 'a GS
graph
'a GS 'a GS
rights
'a GS 'a GS
lefts
'a GS 'a GS
idff
'a GS 'a GS
idright
'a GS 'a GS
idleft
'a GS 'a GS
fields
'a GS 'a GS
appg
'a GS 'a GS 'a GS
$ogf
'a GS 'a GS 'a GS
ccat
'a GS BOOL
ccat_const
'a GS 'a GS
cfunc
'a GS BOOL
cfunc_const
'a GS 'a GS
ccat_cfunc
'a GS BOOL
cfunc_ccat
'a GS BOOL
pf_hered
('a GS BOOL) BOOL
pc_hered
('a GS BOOL) BOOL
pure_functor
'a GS BOOL
pure_category
'a GS BOOL
Fixity

Infix 240:ogf
Definitions
func
s
func s
( d c g
s = (d c) g
fun g
dom g = d
ran g c)
mk_func
l g r mk_func l g r = (l r) 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 rights f
appg
f g appg f g = graph f g g
ogf
f g
f ogf g
= mk_func
(lefts f)
(graph f o graph g)
(rights g)
ccat
s
ccat s
( t
t s
func t
idleft t s
idright t s
( u
u s rights t = lefts u
t ogf u s))
ccat_const
c ccat_const c = (Image lefts c)
cfunc
f
cfunc f
func f
( g g fields f func g)
( g h
g lefts f
h lefts f
rights g = lefts h
appg f (g ogf h)
= appg f g ogf appg f h)
cfunc_const
f cfunc_const f = lefts f rights f
ccat_cfunc
f
ccat_cfunc f
cfunc f ( c c fields f ccat c)
cfunc_ccat
c cfunc_ccat c ccat c ( f f c cfunc f)
pf_hered
p
pf_hered p
( f
ccat_cfunc f ( g g cfunc_const f p g)
p f)
pc_hered
p
pc_hered p
( c
cfunc_ccat c ( d d 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)

up quick index © RBJ