Profile

Statistics
| Branch: | Revision:

 1 (* Pretty-printing rules for coqdoc *)  (** printing ~> %\ensuremath{\rightsquigarrow}% *)  (** printing η %\ensuremath{\eta}% *)  (** printing τ %\ensuremath{\tau}% *)  (** printing ⊕ %\ensuremath{+}% *)  (** printing ⊕⊕ %\ensuremath{+}% *)  (** printing ×× %\ensuremath{\times}% *)  (** printing ^^ %^% *)  (** printing < %\ensuremath{\langle}% *)  (** printing > %\ensuremath{\rangle}% *)  (** printing * %\ensuremath{\!{}^*}% *)  (** printing † %\ensuremath{\!{}^\dagger}% *)  (** printing ∘ %\ensuremath{\circ}% *)  (** printing bang %\ensuremath{!}% *)  (** printing pr1 %\coqdocprojection{pr}\ensuremath{{}_1}% *)  (** printing pr2 %\coqdocprojection{pr}\ensuremath{{}_2}% *)  (** printing inl %\coqdocprojection{in}\ensuremath{{}_1}% *)  (** printing inr %\coqdocprojection{in}\ensuremath{{}_2}% *)  (* begin hide *)  Add LoadPath "~/Schreibtisch/svnba/Elgot/Coq/".  Require Import biCCC.  (* Reserving Notations *)  Reserved Notation "a *" (at level 35).  Reserved Notation "a †" (at level 36).  Open Scope c_scope.  (* end hide *)  Class ElgotMonad (Obj: Type) (Hom: Obj -> Obj -> Type) (C: biCCC Obj Hom) (T: Obj -> Obj) :=  {   (** Monad structure *)   (* unit *)   η : forall a, a ~> T a;   (* Kleisli lifting *)   lifting : forall a b (f: a ~> T b), T a ~> T b   where "a *" := (lifting _ _ a);   map (a b : Obj) (f: a ~> b) : T a ~> T b :=   ((η _) ∘ f) *;   (* laws of Kleisli triple for unit and lifting *)   kl1 : forall a,   (η a) * = id;   kl2 : forall a b (f: a ~> T b),   f * ∘ (η _) = f;   kl3 : forall a b c (f : b ~> T c) (g : a ~> T b),   (f * ∘ g) * = f * ∘ g *;   (* strength *)   τ : forall a b, (a × T b) ~> T (a × b);   (* laws for strength *)   str1 : forall a,   pr2 (a:=terminal_obj) (b:= T a) = (map _ _ pr2) ∘ (τ _ _);   str2 : forall a b c,   (map _ _ p_assoc1) ∘ (τ (prod a b) c) = (τ _ _) ∘ (id ×× (τ _ _)) ∘ p_assoc1;   str3 : forall a b,   (τ a b) ∘ (id ×× (η _)) = η _;   str4 : forall a b c (f: a ~> (T b)),   ((τ _ _) ∘ (id ×× f)) * ∘ (τ _ _) = (τ _ _) ∘ (id (a:=c) ×× f *);     (** Iteration structure *)   iter : forall a b (f : a ~> T (b ⊕ a)), a ~> T b   where "a †" := (iter _ _ a);   (* laws of an Elgot Monad *)   unfolding : forall a b (f : a ~> T (b ⊕ a)),   [ (η _) , f † ] * ∘ f = f †;   naturality : forall a b c (f : a ~> T (b ⊕ a))(g : b ~> T c),   g * ∘ f † = ([ map _ _ inl ∘ g , (η _) ∘ inr ] * ∘ f) †;   dinaturality : forall a b c (g : a ~> T (b ⊕ c)) (h : c ~> T (b ⊕ a)),   ([(η _) ∘ inl, h] * ∘ g) † =   [(η _) , ([(η _) ∘ inl, g] * ∘ h) † ] * ∘ g;   codiagonal : forall a b (g: a ~> T (b ⊕ a ⊕ a)),   ((map _ _ ([id, inr])) ∘ g) † = g † †;   uniformity : forall a b c (f : a ~> T (b ⊕ a)) (g: c ~> T (b ⊕ c)) (h: c ~> a),   f ∘ h = (map _ _ (id ⊕⊕ h)) ∘ g ->   f † ∘ h = g †;   (* strength is compatible with iteration *)   strength_iteration : forall a b (f: a ~> T (b ⊕ a)),   (τ _ _) ∘ (id ×× (f †)) =   ((map _ _ dist2) ∘ (τ _ _) ∘ (id (a:=a) ×× f)) †  }.  (*  Parameter Object : forall Obj (hom : Obj -> Obj -> Type) (T : Obj -> Obj), ElgotMonad Obj hom T -> Type.  Coercion Object : ElgotMonad >-> Sortclass.  *)  Arguments η [Obj Hom0 C T ElgotMonad a].  Arguments lifting [Obj Hom0 C T ElgotMonad a b] f.  Arguments map [Obj Hom0 C T ElgotMonad a b] f.  Arguments τ [Obj Hom0 C T ElgotMonad a b].  Arguments iter [Obj Hom0 C T ElgotMonad a b] f.  Notation "a *" := (lifting a) :c_scope.  Notation "a †" := (iter a) :c_scope.