From Tealeaves Require Import
  Classes.Categorical.DecoratedMonad
  Classes.Kleisli.DecoratedMonad
  Adapters.CategoricalToKleisli.DecoratedMonad
  Adapters.KleisliToCategorical.DecoratedMonad.

Import Product.Notations.
Import Kleisli.Monad.Notations.
Import Kleisli.Comonad.Notations.
Import Kleisli.DecoratedMonad.Notations.

#[local] Generalizable Variable T W.

(** * Categorical ~> Kleisli ~> Categorical *)
(**********************************************************************)
Module decorated_monad_categorical_kleisli_categorical.

  Context
    `{mapT: Map T}
    `{decT: Decorate W T}
    `{joinT: Join T}
    `{retT: Return T}
    `{Monoid W}
    `{! Categorical.DecoratedMonad.DecoratedMonad W T}.

  Definition bindd': Bindd W T T :=
    DerivedOperations.Bindd_Categorical W T.

  Definition map2: Map T :=
    DerivedOperations.Map_Bindd W T T (Bindd_WTU := bindd').
  Definition dec2: Decorate W T :=
    DerivedOperations.Decorate_Bindd W T (Bindd_WTT := bindd').
  Definition join2: Join T :=
    DerivedOperations.Join_Bindd W T (Bindd_WTT := bindd').

  Goal mapT = map2.
mapT = map2
  Proof.
mapT = map2
    unfold map2.
mapT = DerivedOperations.Map_Bindd W T T
    unfold_ops @DerivedOperations.Map_Bindd.
mapT =
(fun (A B : Type) (f : A -> B) =>
 bindd (ret ∘ f ∘ extract))
    unfold bindd.
mapT =
(fun (A B : Type) (f : A -> B) =>
 bindd' A B (ret ∘ f ∘ extract))
    unfold bindd'.
mapT =
(fun (A B : Type) (f : A -> B) =>
 DerivedOperations.Bindd_Categorical W T A B
   (ret ∘ f ∘ extract))
    unfold_ops @DerivedOperations.Bindd_Categorical.
mapT =
(fun (A B : Type) (f : A -> B) =>
 join ∘ map (ret ∘ f ∘ extract) ∘ dec T)
    ext A B f.
A, B: Type
f: A -> B
mapT A B f = join ∘ map (ret ∘ f ∘ extract) ∘ dec T
    rewrite <- (fun_map_map (F := T)).
A, B: Type
f: A -> B
mapT A B f =
join ∘ (map (ret ∘ f) ∘ map extract) ∘ dec T
    reassociate <-.
A, B: Type
f: A -> B
mapT A B f =
join ∘ map (ret ∘ f) ∘ map extract ∘ dec T
    reassociate ->.
A, B: Type
f: A -> B
mapT A B f =
join ∘ map (ret ∘ f) ∘ (map extract ∘ dec T)
    rewrite (dfun_dec_extract (E := W) (F := T)).
A, B: Type
f: A -> B
mapT A B f = join ∘ map (ret ∘ f) ∘ id
    rewrite <- (fun_map_map (F := T)).
A, B: Type
f: A -> B
mapT A B f = join ∘ (map ret ∘ map f) ∘ id
    reassociate <-.
A, B: Type
f: A -> B
mapT A B f = join ∘ map ret ∘ map f ∘ id
    rewrite (mon_join_map_ret (T := T)).
A, B: Type
f: A -> B
mapT A B f = id ∘ map f ∘ id
    reflexivity.
  Qed.

  Goal decT = dec2.
decT = dec2
  Proof.
decT = dec2
    unfold dec2.
decT = DerivedOperations.Decorate_Bindd W T
    unfold_ops @DerivedOperations.Decorate_Bindd.
decT = (fun A : Type => bindd ret)
    unfold bindd.
decT = (fun A : Type => bindd' A (W * A) ret)
    unfold bindd'.
decT =
(fun A : Type =>
 DerivedOperations.Bindd_Categorical W T A (W * A) ret)
    unfold_ops @DerivedOperations.Bindd_Categorical.
decT = (fun A : Type => join ∘ map ret ∘ dec T)
    ext A.
A: Type
decT A = join ∘ map ret ∘ dec T
    rewrite (mon_join_map_ret (T := T)).
A: Type
decT A = id ∘ dec T
    reflexivity.
  Qed.

  Goal joinT = join2.
joinT = join2
  Proof.
joinT = join2
    unfold join2.
joinT = DerivedOperations.Join_Bindd W T
    unfold_ops @DerivedOperations.Join_Bindd.
joinT = (fun A : Type => bindd extract)
    unfold bindd.
joinT = (fun A : Type => bindd' (T A) A extract)
    unfold bindd'.
joinT =
(fun A : Type =>
 DerivedOperations.Bindd_Categorical W T (T A) A
   extract)
    unfold_ops @DerivedOperations.Bindd_Categorical.
joinT = (fun A : Type => join ∘ map extract ∘ dec T)
    ext A.
A: Type
joinT A = join ∘ map extract ∘ dec T
    reassociate ->.
A: Type
joinT A = join ∘ (map extract ∘ dec T)
    rewrite (dfun_dec_extract (E := W) (F := T)).
A: Type
joinT A = join ∘ id
    reflexivity.
  Qed.

End decorated_monad_categorical_kleisli_categorical.

(** * Kleisli ~> Categorical ~> Kleisli *)
(**********************************************************************)
Module decorated_monad_kleisli_categorical_kleisli.

  Context
    `{binddT: Bindd W T T}
    `{retT: Return T}
    `{Monoid W}
    `{@Kleisli.DecoratedMonad.DecoratedMonad W T _ _ retT binddT}.

  Definition map': Map T :=
    DerivedOperations.Map_Bindd W T T.
  Definition dec': Decorate W T :=
    DerivedOperations.Decorate_Bindd W T.
  Definition join': Join T :=
    DerivedOperations.Join_Bindd W T.

  Definition bindd2: Bindd W T T :=
    DerivedOperations.Bindd_Categorical W T
      (Map_T := map') (Join_T := join') (Decorate_WT := dec').

  Goal binddT = bindd2.
binddT = bindd2
  Proof.
binddT = bindd2
    unfold bindd2.
binddT = DerivedOperations.Bindd_Categorical W T
    unfold_ops @DerivedOperations.Bindd_Categorical.
binddT =
(fun (A B : Type) (f : W * A -> T B) =>
 join ∘ map f ∘ dec T)
    unfold map, map', dec, dec', join, join'.
binddT =
(fun (A B : Type) (f : W * A -> T B) =>
 DerivedOperations.Join_Bindd W T B
 ∘ DerivedOperations.Map_Bindd W T T (W * A) (T B) f
 ∘ DerivedOperations.Decorate_Bindd W T A)
    unfold_ops @DerivedOperations.Map_Bindd.
binddT =
(fun (A B : Type) (f : W * A -> T B) =>
 DerivedOperations.Join_Bindd W T B
 ∘ bindd (ret ∘ f ∘ extract)
 ∘ DerivedOperations.Decorate_Bindd W T A)
    unfold_ops @DerivedOperations.Join_Bindd.
binddT =
(fun (A B : Type) (f : W * A -> T B) =>
 bindd extract ∘ bindd (ret ∘ f ∘ extract)
 ∘ DerivedOperations.Decorate_Bindd W T A)
    unfold_ops @DerivedOperations.Decorate_Bindd.
binddT =
(fun (A B : Type) (f : W * A -> T B) =>
 bindd extract ∘ bindd (ret ∘ f ∘ extract) ∘ bindd ret)
    ext A B f.
A, B: Type
f: W * A -> T B
binddT A B f =
bindd extract ∘ bindd (ret ∘ f ∘ extract) ∘ bindd ret
    unfold_compose_in_compose.
A, B: Type
f: W * A -> T B
binddT A B f =
bindd extract ∘ bindd (ret ∘ f ∘ extract) ∘ bindd ret
    rewrite (kdm_bindd2 (T := T)).
A, B: Type
f: W * A -> T B
binddT A B f =
bindd (extract ⋆5 ret ∘ f ∘ extract) ∘ bindd ret
    rewrite (kdm_bindd2 (T := T)).
A, B: Type
f: W * A -> T B
binddT A B f =
bindd ((extract ⋆5 ret ∘ f ∘ extract) ⋆5 ret)
    fequal.
A, B: Type
f: W * A -> T B
f = (extract ⋆5 ret ∘ f ∘ extract) ⋆5 ret
    rewrite kc5_50.
A, B: Type
f: W * A -> T B
f = extract ∘ map f ⋆5 ret
    change (ret (T := T) (A := W * A)) with
      (ret (T:=T) (A := W * A) ∘ id).
A, B: Type
f: W * A -> T B
f = extract ∘ map f ⋆5 ret ∘ id
    rewrite kc5_51.
A, B: Type
f: W * A -> T B
f = extract ∘ map f ⋆1 id
    rewrite <- (natural (ϕ := @extract (W ×) _)).
A, B: Type
f: W * A -> T B
f = map f ∘ extract ⋆1 id
    rewrite kc1_01.
A, B: Type
f: W * A -> T B
f = map f ∘ id
    reflexivity.
  Qed.

End decorated_monad_kleisli_categorical_kleisli.