The Theory pc

Parents

hol

Constants

$_o	F F F
$_a	F F F
$_f	F C BOOL
dom	F C
cod	F C
inj	C (F BOOL) F
id	C F
$_c	C C BOOL
$_c	(F F) C F
$_c	(F C) C C
_c	C
_f	F

Types

C

F

Fixity

Binder:

_c

_c

Right Infix 240:

_a

_o

_c

_f

Axioms

cat_ext_axiom	c1 c2 ( f f _f c1 f _f c2) c1 = c2
fun_ext_axiom	f1 f2 dom f1 = dom f2 cod f1 = cod f2 ( g g _f dom f1 f1 _a g = f2 _a g) f1 = f2
comp_assoc_axiom	f1 f2 f3 cod f1 = dom f2 cod f2 = dom f3 (f1 _o f2) _o f3 = f1 _o f2 _o f3
cat_comp_axiom	c f1 f2 f1 _f c f2 _f c cod f1 = dom f2 (f1 _o f2) _f c
func_comp_axiom	f f1 f2 f1 _f dom f f2 _f dom f cod f1 = dom f2 f _a f1 _o f2 = (f _a f1) _o f _a f2
cat_id_axiom	c f f _f c dom f _c c cod f _c c
injection_axiom	c p ( f g f _f c g _f c p f p g p (f _o g)) ( f f _f c p f p (id (dom f)) p (id (cod f))) ( f f _f dom (inj c p) p f) ( f f _f dom (inj c p) inj c p _a f = f) cod (inj c p) = c
well_founded_axiom	pc pf ( c ( f f _f c pf f) pc c) ( f pc (dom f) pc (cod f) pf f) ( c pc c) ( f pf f)
beta_axiom	c lam f ( g h g _f c g _f c cod g = dom h cod (lam f) = dom (lam h) lam (g _o h) = lam g _o lam h) f _f c $_c lam c _a f = lam f
dfs_axiom	c l L ( f f _f c l f _f L f) ( g h g _f c h _f c cod g = dom h cod (l g) = dom (l h) l (g _o h) = l g _o l h) $_c l c _f $_c L c
infinity_axiom	f c f _f c ( L g d d = dom g ( g g _f d L g _c c) $_c L d _c c ( uf uf _c c ( h1 h2 h1 _f cod f h2 _f dom h1 h2 _f uf)))

Definitions

id	c id c = inj c ( f T)
_c	c1 c2 c1 _c c2 id c1 _f c2
_c	_c = dom (inj ( c T) ( f F))
_f	_f = id _c

Theorems

empty_cat_thm	f f _f _c
cat_ext_thm	c1 c2 c1 = c2 ( f f _f c1 f _f c2)
fun_ext_thm	f1 f2 f1 = f2 dom f1 = dom f2 cod f1 = cod f2 ( g g _f dom f1 f1 _a g = f2 _a g)
empty_cat_initial_thm	c ₁ f dom f = _c cod f = c

V