prop-basic.disco

-- XXX need a syntax for writing qualified types!
-- really want to say something like  (Cmp a, Cmp b) => (a -> b) -> Prop.

injective : (ℕ → ℕ) → Prop
injective(f) = ∀ x : N, y : N. (f(x) == f(y)) ==> (x == y)

surjective : (ℕ → ℕ) → Prop
surjective(f) = ∀ y : N. ∃ x : N. f x == y

-- bijective : (ℕ → ℕ) → Prop
-- bijective(f) = injective(f) and surjective(f)

idempotent : (ℕ → ℕ) → Prop
idempotent(f) = ∀ x : N. f(f(x)) == f(x)

commutative : (ℕ×ℕ → ℕ) → Prop
commutative(f) = ∀ x : N, y : N. f(x,y) == f(y,x)

associative : (ℕ×ℕ → ℕ) → Prop
associative(f) = ∀ (x : N, y : N, z : N). f(x, f(y,z)) == f(f(x,y), z)

identityFor : ℕ × (ℕ×ℕ → ℕ) → Prop
identityFor(e,f) = ∀ x : N. f(x,e) == x and f(e,x) == x