corque / ElgotMonad.v @ 4806fe22
History  View  Annotate  Download (3.59 KB)
1 
(* Prettyprinting 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 