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• ∃1 f• dom f = ∅c ∧ cod f = c |