From Tealeaves Require Import
  Functor
  Classes.Categorical.DecoratedFunctor
  Classes.Kleisli.DecoratedFunctor
  Adapters.CategoricalToKleisli.DecoratedFunctor
  Adapters.KleisliToCategorical.DecoratedFunctor.

Import Product.Notations.
Import Functor.Notations.
Import Comonad.Notations.

#[local] Generalizable Variable T.

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

  Context
    (E: Type)
    (T: Type -> Type)
    `{Map_T: Map T}
    `{Decorate_ET: Decorate E T}
    `{! Categorical.DecoratedFunctor.DecoratedFunctor E T}.

  Definition mapd': Mapd E T :=
    DerivedOperations.Mapd_Categorical E T.

  Definition map2: Map T :=
    DerivedOperations.Map_Mapd E T (Mapd_ET := mapd').

  Definition dec2: Decorate E T :=
    DerivedOperations.Decorate_Mapd E T (Mapd_ET := mapd').

  Goal Map_T = map2.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Map_T = map2
  Proof.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Map_T = map2
    unfold map2.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Map_T = DerivedOperations.Map_Mapd E T
    unfold_ops @DerivedOperations.Map_Mapd.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Map_T =
(fun (A B : Type) (f : A -> B) => mapd (f ∘ extract))
    unfold mapd.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Map_T =
(fun (A B : Type) (f : A -> B) =>
 mapd' A B (f ∘ extract))
    unfold mapd'.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Map_T =
(fun (A B : Type) (f : A -> B) =>
 DerivedOperations.Mapd_Categorical E T A B
   (f ∘ extract))
    unfold DerivedOperations.Mapd_Categorical.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Map_T =
(fun (A B : Type) (f : A -> B) =>
 map (f ∘ extract) ∘ dec T)
    ext A B f.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
Map_T A B f = map (f ∘ extract) ∘ dec T
    rewrite <- (fun_map_map (F := T)).
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
Map_T A B f = map f ∘ map extract ∘ dec T
    reassociate ->.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
Map_T A B f = map f ∘ (map extract ∘ dec T)
    rewrite (dfun_dec_extract (E := E) (F := T)).
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
A, B: Type
f: A -> B
Map_T A B f = map f ∘ id
    reflexivity.
  Qed.

  Goal Decorate_ET = dec2.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Decorate_ET = dec2
  Proof.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Decorate_ET = dec2
    unfold dec2.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Decorate_ET = DerivedOperations.Decorate_Mapd E T
    unfold_ops @DerivedOperations.Decorate_Mapd.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Decorate_ET = (fun A : Type => mapd id)
    unfold mapd.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Decorate_ET = (fun A : Type => mapd' A (E * A) id)
    unfold mapd'.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Decorate_ET =
(fun A : Type =>
 DerivedOperations.Mapd_Categorical E T A (E * A) id)
    unfold_ops @DerivedOperations.Mapd_Categorical.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
Decorate_ET = (fun A : Type => map id ∘ dec T)
    ext A.
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
A: Type
Decorate_ET A = map id ∘ dec T
    rewrite (fun_map_id (F := T)).
E: Type
T: Type -> Type
Map_T: Map T
Decorate_ET: Decorate E T
H: Categorical.DecoratedFunctor.DecoratedFunctor E T
A: Type
Decorate_ET A = id ∘ dec T
    reflexivity.
  Qed.

End decorated_functor_categorical_kleisli_categorical.

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

  Context
    (E: Type)
    (T: Type -> Type)
    `{Mapd_ET: Mapd E T}
    `{! Kleisli.DecoratedFunctor.DecoratedFunctor E T}.

  Definition map': Map T := DerivedOperations.Map_Mapd E T.
  Definition dec': Decorate E T := DerivedOperations.Decorate_Mapd E T.

  Definition mapd2: Mapd E T :=
    DerivedOperations.Mapd_Categorical E T
      (Map_F := map') (Decorate_EF := dec').

  Goal Mapd_ET = mapd2.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET = mapd2
  Proof.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET = mapd2
    unfold mapd2.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET = DerivedOperations.Mapd_Categorical E T
    unfold DerivedOperations.Mapd_Categorical.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET =
(fun (A B : Type) (f : E * A -> B) => map f ∘ dec T)
    unfold map.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET =
(fun (A B : Type) (f : E * A -> B) =>
 map' (E * A) B f ∘ dec T)
    unfold map'.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET =
(fun (A B : Type) (f : E * A -> B) =>
 DerivedOperations.Map_Mapd E T (E * A) B f ∘ dec T)
    unfold DerivedOperations.Map_Mapd.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET =
(fun (A B : Type) (f : E * A -> B) =>
 mapd (f ∘ extract) ∘ dec T)
    unfold dec.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET =
(fun (A B : Type) (f : E * A -> B) =>
 mapd (f ∘ extract) ∘ dec' A)
    unfold dec'.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET =
(fun (A B : Type) (f : E * A -> B) =>
 mapd (f ∘ extract)
 ∘ DerivedOperations.Decorate_Mapd E T A)
    unfold DerivedOperations.Decorate_Mapd.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
Mapd_ET =
(fun (A B : Type) (f : E * A -> B) =>
 mapd (f ∘ extract) ∘ mapd id)
    ext A B f.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
A, B: Type
f: E * A -> B
Mapd_ET A B f = mapd (f ∘ extract) ∘ mapd id
    unfold_compose_in_compose.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
A, B: Type
f: E * A -> B
Mapd_ET A B f = mapd (f ∘ extract) ∘ mapd id
    rewrite (kdf_mapd2 (E := E) (T := T)).
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
A, B: Type
f: E * A -> B
Mapd_ET A B f = mapd (f ∘ extract ⋆1 id)
    rewrite Comonad.kc1_01.
E: Type
T: Type -> Type
Mapd_ET: Mapd E T
H: DecoratedFunctor E T
A, B: Type
f: E * A -> B
Mapd_ET A B f = mapd (f ∘ id)
    reflexivity.
  Qed.

End decorated_functor_kleisli_categorical_kleisli.