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)