From Tealeaves Require Import
  Classes.Categorical.Monad
  Classes.Kleisli.Monad.

Import Kleisli.Monad.Notations.

(** * Kleisli Monads to Categorical Monads *)
(**********************************************************************)

(** ** Derived <<join>> Operation *)
(**********************************************************************)
Module DerivedOperations.
  #[export] Instance Join_Bind
    (T : Type -> Type)
    `{Return_T: Return T}
    `{Bind_TT: Bind T T}: Join T :=
  fun A => bind (@id (T A)).
End DerivedOperations.

(** ** Derived Categorical Laws *)
(**********************************************************************)
Module ToCategorical.

  Section proofs.

    Context
      (T : Type -> Type)
      `{Classes.Kleisli.Monad.Monad T}.

    (* Alectyron doesn't like this
       Import KleisliToCategorical.Monad.DerivedOperations.
     *)
    Import DerivedOperations.
    Existing Instance Kleisli.Monad.DerivedOperations.Map_Bind.
    Existing Instance Kleisli.Monad.DerivedInstances.Functor_Monad.

    #[export] Instance Natural_Ret: Natural (@ret T Return_T).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@ret T Return_T)
    Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@ret T Return_T)
      constructor.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor (fun A : Type => A)
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor T
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad 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
H: Monad T
Functor (fun A : Type => A) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor T typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad 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
H: Monad T
A, B: Type
f: A -> B
map f ∘ ret = ret ∘ map f
        unfold_ops @DerivedOperations.Map_Bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (ret ∘ f) ∘ ret = ret ∘ map f
        unfold_ops @Map_I.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (ret ∘ f) ∘ ret = ret ∘ f
        rewrite (kmon_bind0 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
ret ∘ f = ret ∘ f
        reflexivity.
    Qed.

    #[export] Instance Natural_Join:
      Natural (@join T (Join_Bind T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@join T (Join_Bind T))
    Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@join T (Join_Bind T))
      constructor.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor (T ∘ T)
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor T
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map f
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor (T ∘ T) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor T typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map f intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
map f ∘ join = join ∘ map f
        unfold_ops @Map_compose.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
map f ∘ join = join ∘ map (map f)
        unfold_ops @DerivedOperations.Map_Bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (ret ∘ f) ∘ join =
join ∘ bind (ret ∘ bind (ret ∘ f))
        unfold_ops @DerivedOperations.Join_Bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (ret ∘ f) ∘ bind id =
bind id ∘ bind (ret ∘ bind (ret ∘ f))
        unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (ret ∘ f) ∘ bind id =
bind id ∘ bind (ret ∘ bind (ret ∘ f))
        rewrite (kmon_bind2 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (ret ∘ f ⋆ id) =
bind id ∘ bind (ret ∘ bind (ret ∘ f))
        unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (bind (ret ∘ f) ∘ id) =
bind id ∘ bind (ret ∘ bind (ret ∘ f))
        change (?x ∘ id) with x.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (bind (ret ∘ f)) =
bind id ∘ bind (ret ∘ bind (ret ∘ f))
        (* RHS *)
        rewrite (kmon_bind2 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (bind (ret ∘ f)) =
bind (id ⋆ ret ∘ bind (ret ∘ f))
        unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (bind (ret ∘ f)) =
bind (bind id ∘ (ret ∘ bind (ret ∘ f)))
        reassociate <- on right.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (bind (ret ∘ f)) =
bind (bind id ∘ ret ∘ bind (ret ∘ f))
        rewrite (kmon_bind0 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (bind (ret ∘ f)) = bind (id ∘ bind (ret ∘ f))
        change (id ∘ ?x) with x.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> B
bind (bind (ret ∘ f)) = bind (bind (ret ∘ f))
        reflexivity.
    Qed.

    #[local] Instance CategoricalFromKleisli_Monad:
      Classes.Categorical.Monad.Monad T.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Categorical.Monad.Monad T
    Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Categorical.Monad.Monad T
      constructor.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor T
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@ret T Return_T)
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@join T (Join_Bind T))
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, join ∘ ret = id
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, join ∘ map ret = id
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, join ∘ join = join ∘ map join
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Functor T typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@ret T Return_T) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Natural (@join T (Join_Bind T)) typeclasses eauto.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, join ∘ ret = id intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
join ∘ ret = id
        unfold transparent tcs.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind id ∘ ret = id
        unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind id ∘ ret = id
        rewrite (kmon_bind0 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
id = id
        reflexivity.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, join ∘ map ret = id intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
join ∘ map ret = id
        unfold transparent tcs.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind id ∘ bind (ret ∘ ret) = id
        unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind id ∘ bind (ret ∘ ret) = id
        rewrite (kmon_bind2 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (id ⋆ ret ∘ ret) = id
        unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (bind id ∘ (ret ∘ ret)) = id
        reassociate <- near (bind (@id (T A))).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (bind id ∘ ret ∘ ret) = id
        rewrite (kmon_bind0 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (id ∘ ret) = id
        change (id ∘ ?x) with x.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind ret = id
        rewrite (kmon_bind1 (T := T) A).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
id = id
        reflexivity.
      -
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
forall A : Type, join ∘ join = join ∘ map join intros.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
join ∘ join = join ∘ map join
        unfold transparent tcs.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind id ∘ bind id = bind id ∘ bind (ret ∘ bind id)
        unfold_compose_in_compose.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind id ∘ bind id = bind id ∘ bind (ret ∘ bind id)
        rewrite (kmon_bind2 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (id ⋆ id) = bind id ∘ bind (ret ∘ bind id)
        rewrite (kmon_bind2 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (id ⋆ id) = bind (id ⋆ ret ∘ bind id)
        unfold kc.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (bind id ∘ id) = bind (bind id ∘ (ret ∘ bind id))
        reassociate <- near (bind (@id (T A))).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (bind id ∘ id) = bind (bind id ∘ ret ∘ bind id)
        rewrite (kmon_bind0 (T := T)).
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A: Type
bind (bind id ∘ id) = bind (id ∘ bind id)
        reflexivity.
    Qed.

  End proofs.

End ToCategorical.