# CoRN.algebra.RSetoid

Require Export Setoid.
Require Import CornBasics.
Require Import abstract_algebra.

*

# THIS NOTION IS OBSOLETE AND SHOULD NOT BE USED ANYMORE

Structure RSetoid: Type :=
{ st_car :> Type;
st_eq : Equiv st_car ;
st_isSetoid : Setoid st_car
}.

Typeclasses Transparent Equiv.
Hint Extern 10 (Equiv _) => apply @st_eq : typeclass_instances.
Hint Extern 10 (Setoid _) => apply @st_isSetoid : typeclass_instances.

Implicit Arguments st_eq [r].

Definition mcSetoid_as_RSetoid X {e : Equiv X} {setoid : Setoid X} : RSetoid := Build_RSetoid setoid.
Implicit Arguments mcSetoid_as_RSetoid [[e] [setoid]].

Propositions form a setoid under iff
Definition iffSetoid : RSetoid.

## Morhpisms between Setoids

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

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

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

Open Local Scope setoid_scope.

## Basic Combinators for Setoids

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

Definition compose1 (X Y Z : RSetoid) : (Y-->Z) -> (X --> Y) -> X --> Z.

Definition compose2 (X Y Z : RSetoid) : (Y-->Z) -> (X --> Y) --> X --> Z.

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

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

Definition flip1 (X Y Z : RSetoid) : (X-->Y-->Z)->Y-->X-->Z.

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

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

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

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