pc_ext
pf_ext
• f1 = f2 ⇔ domc f1 = domc f2 ∧ codc f1 = codc f2 ∧ (∀ f• f ∈f domc f1 ⇒ f1 f f = f2 f f)
associative_axiom
• codc h = domc g ∧ codc g = domc f ⇒ f of g of h = (f of g) of h
identity_axiom
• (domc f = c ⇒ idf c of f = f) ∧ (codc f = c ⇒ f of idf c = f)
pc_closure_axiom
• f ∈f c ⇒ domc f ∈c c ∧ codc f ∈c c ∧ (g ∈f c ∧ domc f = codc g ⇒ (f of g) ∈f c)
pf_induction
• (∀ f • (∀ g• g ∈f domc f ∨ g ∈f codc f ⇒ p g) ⇒ p f) ⇒ (∀ f• p f)
