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

Export Categorical.Monad (Return, ret).

Import Product.Notations.
Import Functor.Notations.
Import Kleisli.Monad.Notations.

#[local] Generalizable Variable T.

(** * Categorical ~> Kleisli ~> Categorical *)
(**********************************************************************)
Section categorical_to_kleisli_to_categorical.

  Context
    `{Return_T: Return T}
    `{Map_T: Map T}
    `{Join_T: Join T}
    `{! Categorical.Monad.Monad T}.

  (* Derive the Kleisli operation *)
  Definition bind': Bind T T :=
    CategoricalToKleisli.Monad.DerivedOperations.Bind_Categorical T.

  (* Re-derive the categorical operations *)
  Definition map2: Map T :=
    Kleisli.Monad.DerivedOperations.Map_Bind T T
      (Bind_TU := bind').

  Definition join2: Join T :=
    Adapters.KleisliToCategorical.Monad.DerivedOperations.Join_Bind T
      (Bind_TT := bind').

  Lemma map_roundtrip: Map_T = map2.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
Map_T = map2
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
Map_T = map2
    ext A B f.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = map2 A B f
    unfold map2.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = DerivedOperations.Map_Bind T T A B f
    unfold DerivedOperations.Map_Bind.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = bind (ret ∘ f)
    unfold bind.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = bind' A B (ret ∘ f)
    unfold bind'.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f =
DerivedOperations.Bind_Categorical T A B (ret ∘ f)
    unfold DerivedOperations.Bind_Categorical.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = join ∘ map (ret ∘ f)
    rewrite <- (fun_map_map (F := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = join ∘ (map ret ∘ map f)
    reassociate <- on right.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = join ∘ map ret ∘ map f
    rewrite (mon_join_map_ret (T := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A, B: Type
f: A -> B
Map_T A B f = id ∘ map f
    reflexivity.
  Qed.

  Lemma join_roundtrip: Join_T = join2.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
Join_T = join2
  Proof.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
Join_T = join2
    ext A.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A: Type
Join_T A = join2 A
    unfold join2.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A: Type
Join_T A = DerivedOperations.Join_Bind T A
    unfold DerivedOperations.Join_Bind.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A: Type
Join_T A = bind id
    unfold bind.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A: Type
Join_T A = bind' (T A) A id
    unfold bind'.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A: Type
Join_T A =
DerivedOperations.Bind_Categorical T (T A) A id
    unfold DerivedOperations.Bind_Categorical.
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A: Type
Join_T A = join ∘ map id
    rewrite (fun_map_id (F := T)).
T: Type -> Type
Return_T: Return T
Map_T: Map T
Join_T: Join T
H: Categorical.Monad.Monad T
A: Type
Join_T A = join ∘ id
    reflexivity.
  Qed.

End categorical_to_kleisli_to_categorical.

(** * Kleisli ~> Categorical ~> Kleisli *)
(**********************************************************************)
Section kleisli_to_categorical_to_kleisli.

  Context
    `{Return_T: Return T}
    `{Bind_TT: Bind T T}
    `{! Kleisli.Monad.Monad T}.

  Definition map': Map T := DerivedOperations.Map_Bind T T.
  Definition join': Join T := DerivedOperations.Join_Bind T.

  Definition bind2: Bind T T :=
    DerivedOperations.Bind_Categorical T
      (map_T := map') (join_T := join').

  Goal Bind_TT = bind2.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Bind_TT = bind2
  Proof.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
Bind_TT = bind2
    ext A B f.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f = bind2 A B f
    unfold bind2.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f =
DerivedOperations.Bind_Categorical T A B f
    unfold DerivedOperations.Bind_Categorical.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f = join ∘ map f
    unfold join.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f = join' B ∘ map f
    unfold join'.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f =
DerivedOperations.Join_Bind T B ∘ map f
    unfold DerivedOperations.Join_Bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f = bind id ∘ map f
    unfold map.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f = bind id ∘ map' A (T B) f
    unfold map'.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f =
bind id ∘ DerivedOperations.Map_Bind T T A (T B) f
    unfold DerivedOperations.Map_Bind.
T: Type -> Type
Return_T: Return T
Bind_TT: Bind T T
H: Monad T
A, B: Type
f: A -> T B
Bind_TT A B f = bind id ∘ 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 -> T B
Bind_TT A B f = bind id ∘ 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 -> T B
Bind_TT A B f = bind (id ⋆ ret ∘ 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_TT A B f = bind (bind id ∘ (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 -> T B
Bind_TT A B f = bind (bind id ∘ 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 -> T B
Bind_TT A B f = bind (id ∘ f)
    reflexivity.
  Qed.

End kleisli_to_categorical_to_kleisli.