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 • 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 ogf ⊢ ∀ f g • f ogf g = mk_func (lefts f) (graph f og 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 ogf 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 ogf h) = appg f g ogf 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)