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)

Created: