From Tealeaves Require Export
  Tactics.Prelude
  Functors.Identity
  Classes.Categorical.Monad (Return, ret).

Import Functor.Notations.

#[local] Generalizable Variable T.

(** * Monads *)
(**********************************************************************)

(** ** Operations *)
(**********************************************************************)
Class Bind (T U: Type -> Type) :=
  bind: forall (A B: Type), (A -> T B) -> U A -> U B.

#[global] Arguments bind {T} {U}%function_scope {Bind}
  {A B}%type_scope _%function_scope _.

(** ** Kleisli Composition *)
(**********************************************************************)
Definition kc {T: Type -> Type} `{Return T} `{Bind T T}
  {A B C: Type} (g: B -> T C) (f: A -> T B): (A -> T C) :=
  @bind T T _ B C g ∘ f.

#[local] Infix "⋆" := (kc) (at level 60): tealeaves_scope.

(** ** Typeclasses *)
(**********************************************************************)
Class RightPreModule
  (T U: Type -> Type)
  `{Return T} `{Bind T T} `{Bind T U} :=
  { kmod_bind1: forall (A: Type),
      bind (U := U) ret = @id (U A);
    kmod_bind2: forall (A B C: Type) (g: B -> T C) (f: A -> T B),
      bind (U := U) g ∘ bind f = bind (g ⋆ f);
  }.

Class Monad (T: Type -> Type)
  `{Return_T: Return T}
  `{Bind_TT: Bind T T} :=
  { kmon_bind0: forall (A B: Type) (f: A -> T B),
      bind f ∘ ret = f;
    kmon_premod :> RightPreModule T T;
  }.

Class RightModule (T: Type -> Type) (U: Type -> Type)
  `{Return_T: Return T}
  `{Bind_TT: Bind T T}
  `{Bind_TU: Bind T U} :=
  { kmod_monad :> Monad T;
    kmod_premod :> RightPreModule T U;
  }.

#[local] Instance RightModule_Monad
  (T: Type -> Type)
  `{Monad_T: Monad T}: RightModule T T :=
  {| kmod_monad := Monad_T;
  |}.

(* right unit law of the monoid *)
Lemma kmon_bind1 `{Monad T}: forall (A: Type),
    @bind T T _ A A (@ret T _ A) = @id (T A).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, bind ret = id
Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, bind ret = id
  apply kmod_bind1.
Qed.

(* associativity of the monoid *)
Lemma kmon_bind2 `{Monad T}:
  forall (A B C: Type) (g: B -> T C) (f: A -> T B),
    @bind T T _ B C g ∘ @bind T T _ A B f = @bind T T _ A C (g ⋆ f).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (A B C : Type) (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (A B C : Type) (g : B -> T C) (f : A -> T B),
bind g ∘ bind f = bind (g ⋆ f)
  apply kmod_bind2.
Qed.

(** ** Kleisli Category Laws *)
(**********************************************************************)
Section Monad_Kleisli_category.

  Context
    `{Monad T}.

  #[local] Generalizable Variables A B C D.

  (** *** Left identity law *)
  Theorem kleisli_id_l: forall `(f: A -> T B),
      (@ret T _ B) ⋆ f = f.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (A B : Type) (f : A -> T B), ret ⋆ f = f
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (A B : Type) (f : A -> T B), ret ⋆ f = f
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
ret ⋆ f = f unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
bind ret ∘ f = f
    rewrite kmon_bind1.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
id ∘ f = f
    reflexivity.
  Qed.

  (** *** Right identity law *)
  Theorem kleisli_id_r: forall `(g: B -> T C),
      g ⋆ (@ret T _ B) = g.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (B C : Type) (g : B -> T C), g ⋆ ret = g
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (B C : Type) (g : B -> T C), g ⋆ ret = g
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
B, C: Type
g: B -> T C
g ⋆ ret = g unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
B, C: Type
g: B -> T C
bind g ∘ ret = g
    rewrite kmon_bind0.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
B, C: Type
g: B -> T C
g = g
    reflexivity.
  Qed.

  (** *** Associativity law *)
  Theorem kleisli_assoc:
    forall `(h: C -> T D) `(g: B -> T C) `(f: A -> T B),
      h ⋆ (g ⋆ f) = (h ⋆ g) ⋆ f.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (C D : Type) (h : C -> T D) (B : Type)
  (g : B -> T C) (A : Type) (f : A -> T B),
h ⋆ (g ⋆ f) = (h ⋆ g) ⋆ f
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (C D : Type) (h : C -> T D) (B : Type)
  (g : B -> T C) (A : Type) (f : A -> T B),
h ⋆ (g ⋆ f) = (h ⋆ g) ⋆ f
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
C, D: Type
h: C -> T D
B: Type
g: B -> T C
A: Type
f: A -> T B
h ⋆ (g ⋆ f) = (h ⋆ g) ⋆ f unfold kc at 3.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
C, D: Type
h: C -> T D
B: Type
g: B -> T C
A: Type
f: A -> T B
h ⋆ (g ⋆ f) = bind (h ⋆ g) ∘ f
    rewrite <- kmon_bind2.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
C, D: Type
h: C -> T D
B: Type
g: B -> T C
A: Type
f: A -> T B
h ⋆ (g ⋆ f) = bind h ∘ bind g ∘ f
    reflexivity.
  Qed.

End Monad_Kleisli_category.

(** ** Monad Homomorphisms *)
(**********************************************************************)
Class MonadHom (T U: Type -> Type)
  `{Return T} `{Bind T T}
  `{Return U} `{Bind U U}
  (ϕ: forall (A: Type), T A -> U A) :=
  { kmon_hom_bind: forall (A B: Type) (f: A -> T B),
      ϕ B ∘ bind f = bind (ϕ B ∘ f) ∘ ϕ A;
    kmon_hom_ret: forall (A: Type),
      ϕ A ∘ ret (T := T) = ret;
  }.

Class RightModuleHom (T U V: Type -> Type)
  `{Return T} `{Bind T U} `{Bind T V}
  (ϕ: forall (A: Type), U A -> V A) :=
  { kmod_hom_bind: forall (A B: Type) (f: A -> T B),
      ϕ B ∘ @bind T U _ A B f = @bind T V _ A B f ∘ ϕ A;
  }.

Class ParallelRightModuleHom (T T' U U': Type -> Type)
  `{Return T} `{Bind T U} `{Bind T' U'}
  (ψ: forall (A: Type), T A -> T' A)
  (ϕ: forall (A: Type), U A -> U' A) :=
  { kmodpar_hom_bind: forall (A B: Type) (f: A -> T B),
      ϕ B ∘ @bind T U _ A B f = @bind T' U' _ A B (ψ B ∘ f) ∘ ϕ A;
  }.


(** * Derived Structures *)
(**********************************************************************)

(** ** Derived Operations *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Map_Bind (T U: Type -> Type)
    `{Return_T: Return T}
    `{Bind_TU: Bind T U}: Map U :=
  fun A B (f: A -> B) => @bind T U Bind_TU A B (@ret T Return_T B ∘ f).

End DerivedOperations.

Class Compat_Map_Bind
  (T: Type -> Type)
  (U: Type -> Type)
  `{Return_T: Return T}
  `{Map_U: Map U}
  `{Bind_TU: Bind T U}: Prop :=
  compat_map_bind:
    @Map_U = @DerivedOperations.Map_Bind T U Return_T Bind_TU.

#[export] Instance Compat_Map_Bind_Monad (T U: Type -> Type)
  `{Return_T: Return T} `{Bind_TU: Bind T U}:
  @Compat_Map_Bind T U Return_T
    (@DerivedOperations.Map_Bind T U Return_T Bind_TU) Bind_TU.
T, U: Type -> Type
Return_T: Return T
Bind_TU: Bind T U
Compat_Map_Bind T U
Proof.
T, U: Type -> Type
Return_T: Return T
Bind_TU: Bind T U
Compat_Map_Bind T U
  reflexivity.
Qed.

Lemma map_to_bind {T U: Type -> Type}
  `{Return_T: Return T}
  `{Map_U: Map U}
  `{Bind_TU: Bind T U}
  `{! Compat_Map_Bind T U}: forall {A B: Type} (f: A -> B),
    @map U Map_U A B f = @bind T U Bind_TU A B (@ret T Return_T B ∘ f).
T, U: Type -> Type
Return_T: Return T
Map_U: Map U
Bind_TU: Bind T U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (f : A -> B),
map f = bind (ret ∘ f)
Proof.
T, U: Type -> Type
Return_T: Return T
Map_U: Map U
Bind_TU: Bind T U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (f : A -> B),
map f = bind (ret ∘ f)
  rewrite compat_map_bind.
T, U: Type -> Type
Return_T: Return T
Map_U: Map U
Bind_TU: Bind T U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (f : A -> B),
DerivedOperations.Map_Bind T U A B f = bind (ret ∘ f)
  reflexivity.
Qed.

(** ** Derived Kleisli Composition laws *)
(**********************************************************************)
Section derived_kleisli_composition_laws.

  Context
    `{Monad T} `{Map T} `{! Compat_Map_Bind T T}.

  #[local] Generalizable Variables A B C D.

  (** *** Special cases for Kleisli composition *)
  (********************************************************************)
  Lemma kc_00: forall `(g: B -> C) `(f: A -> B),
      (ret ∘ g) ⋆ (ret ∘ f) = ret ∘ (g ∘ f).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> C) (A : Type)
  (f : A -> B), ret ∘ g ⋆ ret ∘ f = ret ∘ (g ∘ f)
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> C) (A : Type)
  (f : A -> B), ret ∘ g ⋆ ret ∘ f = ret ∘ (g ∘ f)
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
A: Type
f: A -> B
ret ∘ g ⋆ ret ∘ f = ret ∘ (g ∘ f) unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
A: Type
f: A -> B
bind (ret ∘ g) ∘ (ret ∘ f) = ret ∘ (g ∘ f)
    reassociate <-.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
A: Type
f: A -> B
bind (ret ∘ g) ∘ ret ∘ f = ret ∘ (g ∘ f)
    rewrite kmon_bind0.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
A: Type
f: A -> B
ret ∘ g ∘ f = ret ∘ (g ∘ f)
    reflexivity.
  Qed.

  Lemma kc_10: forall `(g: B -> T C) `(f: A -> B),
      g ⋆ (ret ∘ f) = g ∘ f.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> T C) (A : Type)
  (f : A -> B), g ⋆ ret ∘ f = g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> T C) (A : Type)
  (f : A -> B), g ⋆ ret ∘ f = g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> T C
A: Type
f: A -> B
g ⋆ ret ∘ f = g ∘ f unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> T C
A: Type
f: A -> B
bind g ∘ (ret ∘ f) = g ∘ f
    reassociate <-.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> T C
A: Type
f: A -> B
bind g ∘ ret ∘ f = g ∘ f
    rewrite kmon_bind0.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> T C
A: Type
f: A -> B
g ∘ f = g ∘ f
    reflexivity.
  Qed.

  Lemma kc_01: forall `(g: B -> C) `(f: A -> T B),
      (ret ∘ g) ⋆ f = map g ∘ f.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> C) (A : Type)
  (f : A -> T B), ret ∘ g ⋆ f = map g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> C) (A : Type)
  (f : A -> T B), ret ∘ g ⋆ f = map g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
A: Type
f: A -> T B
ret ∘ g ⋆ f = map g ∘ f unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
A: Type
f: A -> T B
bind (ret ∘ g) ∘ f = map g ∘ f
    rewrite map_to_bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
A: Type
f: A -> T B
bind (ret ∘ g) ∘ f = bind (ret ∘ g) ∘ f
    reflexivity.
  Qed.

  (** *** Other rules for Kleisli composition *)
  (********************************************************************)
  Lemma kc_asc1: forall `(g: B -> C) `(h: C -> T D) `(f: A -> T B),
      (h ∘ g) ⋆ f = h ⋆ (map g ∘ f).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> C) (D : Type)
  (h : C -> T D) (A : Type) (f : A -> T B),
h ∘ g ⋆ f = h ⋆ map g ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (B C : Type) (g : B -> C) (D : Type)
  (h : C -> T D) (A : Type) (f : A -> T B),
h ∘ g ⋆ f = h ⋆ map g ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
D: Type
h: C -> T D
A: Type
f: A -> T B
h ∘ g ⋆ f = h ⋆ map g ∘ f unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
D: Type
h: C -> T D
A: Type
f: A -> T B
bind (h ∘ g) ∘ f = bind h ∘ (map g ∘ f)
    reassociate <-.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
D: Type
h: C -> T D
A: Type
f: A -> T B
bind (h ∘ g) ∘ f = bind h ∘ map g ∘ f
    rewrite map_to_bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
D: Type
h: C -> T D
A: Type
f: A -> T B
bind (h ∘ g) ∘ f = bind h ∘ bind (ret ∘ g) ∘ f
    rewrite kmod_bind2.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
D: Type
h: C -> T D
A: Type
f: A -> T B
bind (h ∘ g) ∘ f = bind (h ⋆ ret ∘ g) ∘ f
    rewrite kc_10.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
B, C: Type
g: B -> C
D: Type
h: C -> T D
A: Type
f: A -> T B
bind (h ∘ g) ∘ f = bind (h ∘ g) ∘ f
    reflexivity.
  Qed.

  Lemma kc_asc2: forall `(f: A -> B) `(g: B -> T C) `(h: C -> T D),
      h ⋆ (g ∘ f) = (h ⋆ g) ∘ f.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f : A -> B) (C : Type)
  (g : B -> T C) (D : Type) (h : C -> T D),
h ⋆ g ∘ f = (h ⋆ g) ∘ f
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f : A -> B) (C : Type)
  (g : B -> T C) (D : Type) (h : C -> T D),
h ⋆ g ∘ f = (h ⋆ g) ∘ f
    intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> B
C: Type
g: B -> T C
D: Type
h: C -> T D
h ⋆ g ∘ f = (h ⋆ g) ∘ f unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
H0: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> B
C: Type
g: B -> T C
D: Type
h: C -> T D
bind h ∘ (g ∘ f) = bind h ∘ g ∘ f
    reflexivity.
  Qed.

End derived_kleisli_composition_laws.

(** ** Derived Composition Laws *)
(**********************************************************************)
Section derived_instances.

  #[local] Generalizable Variables U A B C.

  Context
    `{RightModule_TU: RightPreModule T U}
    `{Map_U: Map U}
    `{Map_T: Map T}
    `{! Compat_Map_Bind T U}
    `{! Compat_Map_Bind T T}
    `{Monad_T: ! Monad T}.

  (** *** Composition between [bind] and [map] *)
  (********************************************************************)
  Lemma bind_map: forall `(g: B -> T C) `(f: A -> B),
      bind (U:= U) g ∘ map f = bind (g ∘ f).
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall (B C : Type) (g : B -> T C) (A : Type)
  (f : A -> B), bind g ∘ map f = bind (g ∘ f)
  Proof.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall (B C : Type) (g : B -> T C) (A : Type)
  (f : A -> B), bind g ∘ map f = bind (g ∘ f)
    intros.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> T C
A: Type
f: A -> B
bind g ∘ map f = bind (g ∘ f)
    rewrite map_to_bind.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> T C
A: Type
f: A -> B
bind g ∘ bind (ret ∘ f) = bind (g ∘ f)
    rewrite kmod_bind2.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> T C
A: Type
f: A -> B
bind (g ⋆ ret ∘ f) = bind (g ∘ f)
    rewrite kc_10.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> T C
A: Type
f: A -> B
bind (g ∘ f) = bind (g ∘ f)
    reflexivity.
  Qed.

  Corollary map_bind: forall `(g: B -> C) `(f: A -> T B),
      map g ∘ bind (U := U) f = bind (map g ∘ f).
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall (B C : Type) (g : B -> C) (A : Type)
  (f : A -> T B), map g ∘ bind f = bind (map g ∘ f)
  Proof.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall (B C : Type) (g : B -> C) (A : Type)
  (f : A -> T B), map g ∘ bind f = bind (map g ∘ f)
    intros.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> C
A: Type
f: A -> T B
map g ∘ bind f = bind (map g ∘ f)
    rewrite map_to_bind.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> C
A: Type
f: A -> T B
bind (ret ∘ g) ∘ bind f = bind (map g ∘ f)
    rewrite kmod_bind2.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> C
A: Type
f: A -> T B
bind (ret ∘ g ⋆ f) = bind (map g ∘ f)
    rewrite map_to_bind.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
B, C: Type
g: B -> C
A: Type
f: A -> T B
bind (ret ∘ g ⋆ f) = bind (bind (ret ∘ g) ∘ f)
    reflexivity.
  Qed.

  (** *** Functor laws *)
  (********************************************************************)
  Lemma map_id: forall (A: Type),
      map (F := U) (@id A) = id.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall A : Type, map id = id
  Proof.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall A : Type, map id = id
    intros.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A: Type
map id = id
    rewrite map_to_bind.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A: Type
bind (ret ∘ id) = id
    change (?f ∘ id) with f.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A: Type
bind ret = id
    rewrite kmod_bind1.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A: Type
id = id
    reflexivity.
  Qed.

  Lemma map_map: forall (A B C: Type) (f: A -> B) (g: B -> C),
      map g ∘ map f = map (F := U) (g ∘ f).
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  Proof.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
    intros.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f)
    rewrite map_to_bind.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A, B, C: Type
f: A -> B
g: B -> C
bind (ret ∘ g) ∘ map f = map (g ∘ f)
    rewrite map_to_bind.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A, B, C: Type
f: A -> B
g: B -> C
bind (ret ∘ g) ∘ bind (ret ∘ f) = map (g ∘ f)
    rewrite kmod_bind2.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A, B, C: Type
f: A -> B
g: B -> C
bind (ret ∘ g ⋆ ret ∘ f) = map (g ∘ f)
    rewrite kc_00.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A, B, C: Type
f: A -> B
g: B -> C
bind (ret ∘ (g ∘ f)) = map (g ∘ f)
    rewrite map_to_bind.
T, U: Type -> Type
H: Return T
H0: Bind T T
H1: Bind T U
RightModule_TU: RightPreModule T U
Map_U: Map U
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T U
Compat_Map_Bind1: Compat_Map_Bind T T
Monad_T: Monad T
A, B, C: Type
f: A -> B
g: B -> C
bind (ret ∘ (g ∘ f)) = bind (ret ∘ (g ∘ f))
    reflexivity.
  Qed.

End derived_instances.

(** ** Derived Typeclass Instances *)
(**********************************************************************)
Module DerivedInstances.
  #[local] Generalizable Variables U.

  #[export] Instance Functor_RightModule
    `{RightModule_TU: RightModule T U}
    `{Map_U: Map U}
    `{! Compat_Map_Bind T U}:
    Functor U (Map_F := Map_U) :=
    {| fun_map_id := map_id;
       fun_map_map := map_map;
    |}.

  #[export] Instance Functor_Monad
    `{Monad_T: Monad T}
    `{Map_T: Map T}
    `{! Compat_Map_Bind T T}:
    Functor T := Functor_RightModule.

  Include DerivedOperations.

End DerivedInstances.

(** ** Naturality Properties *)
(**********************************************************************)

(** *** Return *)
#[export] Instance Natural_Return
  `{Monad_T: Monad T} `{Map_T: Map T}
  `{! Compat_Map_Bind T T}:
  Natural (@ret T Return_T).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
Natural (@ret T Return_T)
Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
Natural (@ret T Return_T)
  constructor.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
Functor (fun A : Type => A)
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
Functor T
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f
  -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
Functor (fun A : Type => A) apply Functor_I.
  -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
Functor T apply DerivedInstances.Functor_Monad.
  -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> B
map f ∘ ret = ret ∘ map f
    rewrite map_to_bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> B
bind (ret ∘ f) ∘ ret = ret ∘ map f
    rewrite kmon_bind0.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> B
ret ∘ f = ret ∘ map f
    unfold_ops @Map_I.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
Monad_T: Monad T
Map_T: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> B
ret ∘ f = ret ∘ f
    reflexivity.
Qed.


(** *** Monad Homomorphisms *)
#[export] Instance Natural_MonadHom
  `{Monad T1} `{Monad T2}
  `{Map T1} `{Map T2}
  `{! Compat_Map_Bind T1 T1}
  `{! Compat_Map_Bind T2 T2}
  (ϕ: forall (A: Type), T1 A -> T2 A)
  `{! MonadHom T1 T2 ϕ}: Natural ϕ.
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
Natural ϕ
Proof.
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
Natural ϕ
  constructor.
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
Functor T1
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
Functor T2
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
forall (A B : Type) (f : A -> B),
map f ∘ ϕ A = ϕ B ∘ map f
  -
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
Functor T1 apply DerivedInstances.Functor_Monad.
  -
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
Functor T2 apply DerivedInstances.Functor_Monad.
  -
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
forall (A B : Type) (f : A -> B),
map f ∘ ϕ A = ϕ B ∘ map f intros.
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
A, B: Type
f: A -> B
map f ∘ ϕ A = ϕ B ∘ map f
    rewrite map_to_bind.
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
A, B: Type
f: A -> B
bind (ret ∘ f) ∘ ϕ A = ϕ B ∘ map f
    rewrite <- (kmon_hom_ret (T := T1) (U := T2)) at 1.
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
A, B: Type
f: A -> B
bind (ϕ B ∘ ret ∘ f) ∘ ϕ A = ϕ B ∘ map f
    rewrite map_to_bind.
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
A, B: Type
f: A -> B
bind (ϕ B ∘ ret ∘ f) ∘ ϕ A = ϕ B ∘ bind (ret ∘ f)
    rewrite (kmon_hom_bind (T := T1) (U := T2)).
T1: Type -> Type
Return_T: Return T1
Bind_TT: Bind T1 T1
H: Monad T1
T2: Type -> Type
Return_T0: Return T2
Bind_TT0: Bind T2 T2
H0: Monad T2
H1: Map T1
H2: Map T2
Compat_Map_Bind0: Compat_Map_Bind T1 T1
Compat_Map_Bind1: Compat_Map_Bind T2 T2
ϕ: T1 ⇒ T2
MonadHom0: MonadHom T1 T2 ϕ
A, B: Type
f: A -> B
bind (ϕ B ∘ ret ∘ f) ∘ ϕ A =
bind (ϕ B ∘ (ret ∘ f)) ∘ ϕ A
    reflexivity.
Qed.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Infix "⋆" := (kc) (at level 60): tealeaves_scope.
End Notations.