Project

General

Profile

Statistics
| Branch: | Revision:

corque / ElgotMonad.v @ 4806fe22

History | View | Annotate | Download (3.59 KB)

1
(* Pretty-printing rules for coqdoc *)
2

    
3
(** printing ~>  %\ensuremath{\rightsquigarrow}% *)
4
(** printing η   %\ensuremath{\eta}% *)
5
(** printing τ   %\ensuremath{\tau}% *)
6
(** printing ⊕   %\ensuremath{+}% *)
7
(** printing ⊕⊕  %\ensuremath{+}% *)
8
(** printing ××  %\ensuremath{\times}% *)
9
(** printing ^^  %^%  *)
10
(** printing <   %\ensuremath{\langle}% *)
11
(** printing >   %\ensuremath{\rangle}% *)
12
(** printing *   %\ensuremath{\!{}^*}% *)
13
(** printing †   %\ensuremath{\!{}^\dagger}% *)
14
(** printing ∘   %\ensuremath{\circ}% *)
15

    
16
(** printing bang  %\ensuremath{!}% *)
17

    
18
(** printing pr1   %\coqdocprojection{pr}\ensuremath{{}_1}% *)
19
(** printing pr2   %\coqdocprojection{pr}\ensuremath{{}_2}% *)
20

    
21
(** printing inl   %\coqdocprojection{in}\ensuremath{{}_1}% *)
22
(** printing inr   %\coqdocprojection{in}\ensuremath{{}_2}% *)
23

    
24
(* begin hide *)
25

    
26
Add LoadPath "~/Schreibtisch/svnba/Elgot/Coq/".
27
Require Import biCCC.
28

    
29
(* Reserving Notations *)
30
Reserved Notation "a *" (at level 35).
31
Reserved Notation "a †" (at level 36).
32

    
33
Open Scope c_scope.
34

    
35
(* end hide *)
36

    
37

    
38
Class ElgotMonad (Obj: Type) (Hom: Obj -> Obj -> Type) (C: biCCC Obj Hom) (T: Obj -> Obj) := 
39
{ 
40
  (** Monad structure  *)
41

    
42
  (* unit *)
43
  η : forall a, a ~> T a;
44
  (* Kleisli lifting *)
45
  lifting : forall a b (f: a ~> T b), T a ~> T b 
46
    where "a *" := (lifting _ _ a);
47

    
48
  map (a b : Obj) (f: a ~> b) : T a ~> T b :=
49
    ((η _) ∘ f) *;
50

    
51
  (* laws of Kleisli triple for unit and lifting *)
52
  kl1 : forall a, 
53
    (η a) * = id;
54
  kl2 : forall a b (f: a ~> T b), 
55
    f * ∘ (η _) = f;
56
  kl3 : forall a b c (f : b ~> T c) (g : a ~> T b), 
57
    (f * ∘ g) * = f * ∘ g *;
58

    
59
  (* strength *)
60
  τ : forall a b, (a × T b) ~> T (a × b);
61

    
62
  (* laws for strength *)
63
  str1 : forall a,
64
    pr2 (a:=terminal_obj) (b:= T a) = (map _ _ pr2) ∘ (τ _ _);
65
  str2 : forall a b c,
66
    (map _ _ p_assoc1) ∘ (τ (prod a b) c) = (τ _ _) ∘ (id ×× (τ _ _)) ∘ p_assoc1;
67
  str3 : forall a b,
68
    (τ a b) ∘ (id ×× (η _)) = η _;
69
  str4 : forall a b c (f: a ~> (T b)),
70
    ((τ _ _) ∘ (id ×× f)) * ∘ (τ _ _) = (τ _ _) ∘ (id (a:=c) ×× f *);
71
 
72

    
73
  (** Iteration structure  *)
74

    
75
  iter : forall a b (f :  a ~> T (b ⊕ a)), a ~> T b 
76
    where "a †" := (iter _ _ a);
77

    
78
  (* laws of an Elgot Monad *)
79
  unfolding : forall a b (f : a ~> T (b ⊕ a)), 
80
    [ (η _) , f † ] * ∘ f = f †;
81
  naturality : forall a b c (f : a ~> T (b ⊕ a))(g : b ~> T c), 
82
    g * ∘ f † = ([ map _ _ inl ∘ g  , (η _) ∘ inr ] * ∘ f) †;
83
  dinaturality : forall a b c (g : a ~> T (b ⊕ c)) (h : c ~> T (b ⊕ a)),
84
    ([(η _) ∘ inl, h] * ∘ g) † =
85
    [(η _) , ([(η _) ∘ inl, g] * ∘ h) † ] * ∘ g;
86
  codiagonal : forall a b (g: a ~> T (b ⊕ a ⊕ a)),
87
    ((map _ _ ([id, inr])) ∘ g) † = g † †;
88
  uniformity : forall a b c (f : a ~> T (b ⊕ a)) (g: c ~> T (b ⊕ c)) (h: c ~> a),
89
    f ∘ h = (map _ _ (id ⊕⊕ h)) ∘ g ->
90
      f † ∘ h = g †;
91

    
92
  (* strength is compatible with iteration *)
93
  strength_iteration : forall a b (f: a ~> T (b ⊕ a)), 
94
    (τ _ _) ∘ (id ×× (f †)) = 
95
    ((map _ _ dist2) ∘ (τ _ _) ∘ (id (a:=a) ×× f)) †
96

    
97
}.
98

    
99
(*
100
Parameter Object : forall Obj (hom : Obj -> Obj -> Type) (T : Obj -> Obj), ElgotMonad Obj hom T -> Type.
101
Coercion Object : ElgotMonad >-> Sortclass.
102
*)
103

    
104
Arguments η [Obj Hom0 C T ElgotMonad a].
105
Arguments lifting [Obj Hom0 C T ElgotMonad a b] f.
106
Arguments map [Obj Hom0 C T ElgotMonad a b] f.
107
Arguments τ [Obj Hom0 C T ElgotMonad a b].
108
Arguments iter [Obj Hom0 C T ElgotMonad a b] f.
109

    
110
Notation "a *" := (lifting a)                    :c_scope.
111
Notation "a †" := (iter a)                       :c_scope.
112