(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Prelude

   Definitions of operations and standard properties on them.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

Require Import Prelude.Basics.

Local Open Scope equiv_scope.

Fixpoint nary_operation n A : Setoid := 
  match n with
    | 0 => A
    | S n' => A ---> nary_operation n' A
  end.

Definition unary_operation := nary_operation 1.
Definition binary_operation := nary_operation 2.
Definition ternary_operation := nary_operation 3.

(** We define properties of [operation]s up-to an arbitrary setoid equality on the carrier.
   Note how we generalize statements to avoid implicit use of the leibniz equality. *)

Class associative `(op : binary_operation A) := 
  associativity : forall x₁ x₂ x₃, op x₁ (op x₂ x₃) === op (op x₁ x₂) x₃.

Class commutative `(op : binary_operation A) := 
  commutativity : forall x₁ x₂, op x₁ x₂ === op x₂ x₁.

Class idempotent `(op : binary_operation A) := 
  idempotency : forall x, op x x === x.

Class left_neutral `(op : binary_operation A) (e : A) := 
  left_neutrality : forall x, op e x === x.

Class right_neutral `(op : binary_operation A) (e : A) := 
  right_neutrality : forall x, op x e === x.

Class injective `(f : A ---> B) :=
  injectivity : forall x₁ x₂, f x₁ === f x₂ -> x₁ === x₂.

Class surjective `(f : A ---> B) :=
  surjectivity : forall y, exists x, f x === y.

Hint Transparent associative commutative idempotent left_neutral right_neutral. 
Hint Transparent injective surjective.