The Theory pc

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

privacy policy

Created:

V