Record Setoid: Type :=
{ st_car:>Type;
  st_eq:st_car-> st_car ->Prop;
  st_isSetoid: Setoid_Theory _ st_eq
}.


Add Parametric Relation s : (st_car s) (@st_eq s)
 reflexivity proved by (@Equivalence_Reflexive _ _ (st_isSetoid s))
 symmetry proved by (@Equivalence_Symmetric _ _ (st_isSetoid s))
 transitivity proved by (@Equivalence_Transitive _ _ (st_isSetoid s))
 as genericSetoid.

Definition iffSetoid : Setoid.
Defined.

Record Morphism (X Y:Setoid) :=
{evalMorphism :> X -> Y
;Morphism_prf : forall x1 x2, (st_eq x1 x2) -> (st_eq (evalMorphism x1) (evalMorphism x2))
}.

Definition extEq (X:Type) (Y:Setoid) (f g:X -> Y) := forall x, st_eq (f x) (g x).
Definition extSetoid (X Y:Setoid) : Setoid.
Defined.

Notation "x --> y" := (extSetoid x y) (at level 55, right associativity) : setoid_scope.

Definition id (X:Setoid) : X-->X.
Defined.
Definition compose0 X Y Z (x : Y ->Z) (y:X -> Y) z := x (y z).

Definition compose1 (X Y Z:Setoid) : (Y-->Z) -> (X --> Y) -> X --> Z.
Defined.

Definition compose2 (X Y Z:Setoid) : (Y-->Z) -> (X --> Y) --> X --> Z.
Defined.

Definition compose (X Y Z:Setoid) : (Y-->Z) --> (X --> Y) --> X --> Z.
Defined.
Definition const0 (X Y:Setoid) : X->Y-->X.
Defined.

Definition const (X Y:Setoid) : X-->Y-->X.
Defined.
Definition flip0 (X Y Z:Setoid) : (X-->Y-->Z)->Y->X-->Z.
Defined.

Definition flip1 (X Y Z:Setoid) : (X-->Y-->Z)->Y-->X-->Z.
Defined.

Definition flip (X Y Z:Setoid) : (X-->Y-->Z)-->Y-->X-->Z.
Defined.
Definition join0 (X Y:Setoid) : (X-->X-->Y)->X-->Y.
Defined.

Definition join (X Y:Setoid) : (X-->X-->Y)-->X-->Y.
Defined.
Definition ap (X Y Z:Setoid) : (X --> Y --> Z) --> (X --> Y) --> (X --> Z)
:= compose (compose (compose (@join _ _)) (@flip _ _ _)) (compose (@compose _ _ _)).

Definition bind (X Y Z:Setoid) : (X--> Y) --> (Y --> X--> Z) --> (X--> Z):=
(compose (compose (@join _ _)) (flip (@compose X Y (X-->Z)))).

Definition bind_compose (X Y Z W:Setoid) :
 (W--> X--> Y) --> (Y --> X--> Z) --> (W--> X--> Z):=
 (flip (compose (@compose W _ _) ((flip (@bind X Y Z))))).