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
fill• dom f1 = dom f2
fill∧ cod f1 = cod f2
fill∧ (∀ g• g ∈f dom f1 ⇒ f1 a g = f2 a g)
fill⇒ f1 = f2
comp_assoc_axiom
⊢ ∀ f1 f2 f3
fill• cod f1 = dom f2 ∧ cod f2 = dom f3
fill⇒ (f1 o f2) o f3 = f1 o f2 o f3
cat_comp_axiom
⊢ ∀ c f1 f2
fill• f1 ∈f c ∧ f2 ∈f c ∧ cod f1 = dom f2
fill⇒ (f1 o f2) ∈f c
func_comp_axiom
⊢ ∀ f f1 f2
fill• f1 ∈f dom f ∧ f2 ∈f dom f ∧ cod f1 = dom f2
fill⇒ 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
fill• (∀ f g• f ∈f c ∧ g ∈f c ∧ p f ∧ p g ⇒ p (f o g))
fill∧ (∀ f
fill• f ∈f c ∧ p f
fill⇒ p (id (dom f)) ∧ p (id (cod f)))
fill⇒ (∀ f• f ∈f dom (inj c p) ⇔ p f)
fill∧ (∀ f• f ∈f dom (inj c p) ⇒ inj c p a f = f)
fill∧ cod (inj c p) = c
well_founded_axiom
⊢ ∀ pc pf
fill• (∀ c• (∀ f• f ∈f c ⇒ pf f) ⇒ pc c)
fill∧ (∀ f• pc (dom f) ∧ pc (cod f) ⇒ pf f)
fill⇒ (∀ c• pc c) ∧ (∀ f• pf f)
beta_axiom
⊢ ∀ c lam f
fill• (∀ g h
fill• g ∈f c ∧ g ∈f c ∧ cod g = dom h
fill⇒ cod (lam f) = dom (lam h)
fill∧ lam (g o h) = lam g o lam h)
fill∧ f ∈f c
fill⇒ $λc lam c a f = lam f
dfs_axiom
⊢ ∀ c l L
fill• (∀ f• f ∈f c ⇒ l f ∈f L f)
fill∧ (∀ g h
fill• g ∈f c ∧ h ∈f c
fill⇒ cod g = dom h
fill⇒ cod (l g) = dom (l h)
fill∧ l (g o h) = l g o l h)
fill⇒ $λc l c ∈fc L c
infinity_axiom
⊢ ∀ f
fill• ∃ c
fill• f ∈f c
fill∧ (∀ L g d
fill• d = dom g ∧ (∀ g• g ∈f d ⇒ L g ∈c c)
fill⇒ $Λc L d ∈c c
fill∧ (∃ uf
fill• uf ∈c c
fill∧ (∀ h1 h2
fill• h1 ∈f cod f ∧ h2 ∈f dom h1
fill⇒ 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 ∈fc
cat_ext_thm
⊢ ∀ c1 c2• c1 = c2 ⇔ (∀ f• f ∈f c1 ⇔ f ∈f c2)
fun_ext_thm
⊢ ∀ f1 f2
fill• f1 = f2
fill⇔ dom f1 = dom f2
fill∧ cod f1 = cod f2
fill∧ (∀ g• g ∈f dom f1 ⇒ f1 a g = f2 a g)
empty_cat_initial_thm
⊢ ∀ c• ∃1 f• dom f = ∅c ∧ cod f = c

up quick index

privacy policy

Created:

V