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
$ogf
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:
ogf
Definitions
func
⊢ ∀ s
fill• func s
fill⇔ (∃ d c g
fill• s = (d ↦g c) ↦g g
fill∧ fun g
fill∧ dom g = d
fill∧ ran g ⊆g c)
mk_func
⊢ ∀ l g r• mk_func l g r = (l ↦g r) ↦g g
lefts
rights
graph
⊢ ∀ f
fill• lefts f = fst (fst f)
fill∧ rights f = snd (fst f)
fill∧ graph f = snd f
idff
⊢ ∀ f• idff f = mk_func f (id f) f
idleft
idright
⊢ ∀ f
fill• idleft f = idff (lefts f)
fill∧ idright f = idff (rights f)
fields
⊢ ∀ f• fields f = lefts f ∪g rights f
appg
⊢ ∀ f g• appg f g = graph f g g
ogf
⊢ ∀ f g
fill• f ogf g
fill= mk_func
fill(lefts f)
fill(graph f og graph g)
fill(rights g)
ccat
⊢ ∀ s
fill• ccat s
fill⇔ (∀ t
fill• t ∈g s
fill⇒ func t
fill∧ idleft t ∈g s
fill∧ idright t ∈g s
fill∧ (∀ u
fill• u ∈g s ∧ rights t = lefts u
fill⇒ t ogf u ∈g s))
ccat_const
⊢ ∀ c• ccat_const c = ⋃g (Imagep lefts c)
cfunc
⊢ ∀ f
fill• cfunc f
fill⇔ func f
fill∧ (∀ g• g ∈g fields f ⇒ func g)
fill∧ (∀ g h
fill• g ∈g lefts f
fill∧ h ∈g lefts f
fill∧ rights g = lefts h
fill⇒ appg f (g ogf h)
fill= appg f g ogf appg f h)
cfunc_const
⊢ ∀ f• cfunc_const f = lefts f ∪g rights f
ccat_cfunc
⊢ ∀ f
fill• ccat_cfunc f
fill⇔ 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
fill• pf_hered p
fill⇔ (∀ f
fill• ccat_cfunc f ∧ (∀ g• g ∈g cfunc_const f ⇒ p g)
fill⇒ p f)
pc_hered
⊢ ∀ p
fill• pc_hered p
fill⇔ (∀ c
fill• cfunc_ccat c ∧ (∀ d• d ∈g ccat_const c ⇒ p d)
fill⇒ 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

privacy policy

Created:

V