Set Implicit Arguments.

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

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]].

Definition iffSetoid : RSetoid.
Proof.
 eexists Prop iff.
 firstorder.
Defined.

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

Definition extEq (X:Type) (Y : RSetoid) (f g:X → Y) := ∀ x, st_eq (f x) (g x).
Definition extSetoid (X Y : RSetoid) : RSetoid.
Proof.
 eexists (Morphism X Y) (extEq Y).
 split.
   intros x y; reflexivity.
  intros x y H a; symmetry; auto.
 intros x y z Hxy Hyz a; transitivity (y a); auto.
Defined.

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

Open Local Scope setoid_scope.

Definition id (X : RSetoid) : X-->X.
Proof.
 eexists (fun x ⇒ x).
 abstract (auto).
Defined.
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.
Proof.
 intros f0 f1.
 ∃ (compose0 f0 f1).
 abstract ( destruct f0 as [f0 Hf0]; destruct f1 as [f1 Hf1]; intros x1 x2 Hx; apply Hf0; apply Hf1;
   assumption).
Defined.

Definition compose2 (X Y Z : RSetoid) : (Y-->Z) → (X --> Y) --> X --> Z.
Proof.
 intros f0.
 eexists (compose1 f0).
 abstract ( destruct f0 as [f0 Hf0]; intros x1 x2 H y; apply: Hf0; apply H).
Defined.

Definition compose (X Y Z : RSetoid) : (Y-->Z) --> (X --> Y) --> X --> Z.
Proof.
 ∃ (@compose2 X Y Z).
 abstract ( intros x1 x2 H y z; apply: H).
Defined.
Definition const0 (X Y : RSetoid) : X→Y-->X.
Proof.
 intros x.
 eexists (fun y ⇒ x).
 abstract reflexivity.
Defined.

Definition const (X Y : RSetoid) : X-->Y-->X.
Proof.
 ∃ (@const0 X Y).
 abstract ( intros x1 x2 Hx y; assumption).
Defined.
Definition flip0 (X Y Z : RSetoid) : (X-->Y-->Z)->Y→X-->Z.
Proof.
 intros f y.
 ∃ (fun x ⇒ f x y).
 abstract ( destruct f as [f Hf]; intros x1 x2 H; apply Hf; auto).
Defined.

Definition flip1 (X Y Z : RSetoid) : (X-->Y-->Z)->Y-->X-->Z.
Proof.
 intros f.
 ∃ (flip0 f).
 abstract ( destruct f as [f Hf]; intros x1 x2 H y; simpl; destruct (f y) as [g Hg]; apply Hg; auto).
Defined.

Definition flip (X Y Z : RSetoid) : (X-->Y-->Z)-->Y-->X-->Z.
Proof.
 ∃ (@flip1 X Y Z).
 abstract ( intros x1 x2 H y z; apply: H).
Defined.
Definition join0 (X Y : RSetoid) : (X-->X-->Y)->X-->Y.
Proof.
 intros f.
 ∃ (fun y ⇒ f y y).
 abstract ( destruct f as [f Hf]; intros x1 x2 H; simpl; transitivity (f x1 x2);
   [destruct (f x1) as [g Hg]; apply Hg; auto |apply Hf; auto]).
Defined.

Definition join (X Y : RSetoid) : (X-->X-->Y)-->X-->Y.
Proof.
 ∃ (@join0 X Y).
 abstract ( intros x1 x2 H y; apply: H).
Defined.
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))))).