CoRN.algebra.RSetoid
Classic Setoids presented in a bundled way.
*THIS NOTION IS OBSOLETE AND SHOULD NOT BE USED ANYMORE
Use abstract_algebra.Setoid instead
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
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.
{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.
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))))).