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

Import Product.Notations.
Import Functor.Notations.
Import Kleisli.DecoratedTraversableFunctor.Notations.

#[local] Generalizable Variable T.

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

  Context
    (E: Type)
    (T: Type -> Type)
    `{mapT: Map T}
    `{distT: ApplicativeDist T}
    `{decorateT: Decorate E T}
    `{! Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T}.

  #[local] Instance mapdt': Mapdt E T :=
    DerivedOperations.Mapdt_Categorical E T.

  Definition map2: Map T :=
    DerivedOperations.Map_Mapdt.
  Definition decorate2: Decorate E T :=
    DerivedOperations.Decorate_Mapdt E T.
  Definition dist2: ApplicativeDist T :=
    DerivedOperations.Dist_Mapdt E T.

  Goal mapT = map2.
mapT = map2
  Proof.
mapT = map2
    unfold map2.
mapT = DerivedOperations.Map_Mapdt
    unfold DerivedOperations.Map_Mapdt.
mapT =
(fun (A B : Type) (f : A -> B) => mapdt (f ∘ extract))
    unfold mapdt.
mapT =
(fun (A B : Type) (f : A -> B) =>
 mapdt' (fun A0 : Type => A0) Map_I Pure_I Mult_I A B
   (f ∘ extract))
    unfold mapdt'.
mapT =
(fun (A B : Type) (f : A -> B) =>
 DerivedOperations.Mapdt_Categorical E T
   (fun A0 : Type => A0) Map_I Pure_I Mult_I A B
   (f ∘ extract))
    unfold DerivedOperations.Mapdt_Categorical.
mapT =
(fun (A B : Type) (f : A -> B) =>
 dist T (fun A0 : Type => A0) ∘ map (f ∘ extract)
 ∘ dec T)
    ext A B f.
A, B: Type
f: A -> B
mapT A B f =
dist T (fun A : Type => A) ∘ map (f ∘ extract) ∘ dec T
    rewrite (dist_unit (F := T)).
A, B: Type
f: A -> B
mapT A B f = id ∘ map (f ∘ extract) ∘ dec T
    rewrite <- (fun_map_map (F := T)).
A, B: Type
f: A -> B
mapT A B f = id ∘ (map f ∘ map extract) ∘ dec T
    reassociate -> on right.
A, B: Type
f: A -> B
mapT A B f = id ∘ (map f ∘ map extract ∘ dec T)
    reassociate -> on right.
A, B: Type
f: A -> B
mapT A B f = id ∘ (map f ∘ (map extract ∘ dec T))
    rewrite (dfun_dec_extract (E := E) (F := T)).
A, B: Type
f: A -> B
mapT A B f = id ∘ (map f ∘ id)
    reflexivity.
  Qed.

  Goal distT = dist2.
distT = dist2
  Proof.
distT = dist2
    ext G Hmap Hpure Hmult A.
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u =
dist2 G Hmap Hpure Hmult u
    unfold dist2.
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u =
DerivedOperations.Dist_Mapdt E T G Hmap Hpure Hmult u
    unfold DerivedOperations.Dist_Mapdt.
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u = mapdt extract
    unfold mapdt.
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u =
mapdt' G Hmap Hpure Hmult (G u) u extract
    unfold mapdt'.
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u =
DerivedOperations.Mapdt_Categorical E T G Hmap Hpure
  Hmult (G u) u extract
    unfold DerivedOperations.Mapdt_Categorical.
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u =
dist T G ∘ map extract ∘ dec T
    reassociate -> on right.
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u =
dist T G ∘ (map extract ∘ dec T)
    rewrite (dfun_dec_extract (E := E) (F := T)).
G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
u: Type
distT G Hmap Hpure Hmult u = dist T G ∘ id
    reflexivity.
  Qed.

  Goal decorateT = decorate2.
decorateT = decorate2
  Proof.
decorateT = decorate2
    ext A.
A: Type
decorateT A = decorate2 A
    unfold decorate2.
A: Type
decorateT A = DerivedOperations.Decorate_Mapdt E T A
    unfold DerivedOperations.Decorate_Mapdt.
A: Type
decorateT A = mapdt id
    unfold mapdt.
A: Type
decorateT A =
mapdt' (fun A : Type => A) Map_I Pure_I Mult_I A
  (E * A) id
    unfold mapdt'.
A: Type
decorateT A =
DerivedOperations.Mapdt_Categorical E T
  (fun A : Type => A) Map_I Pure_I Mult_I A (E * A) id
    unfold DerivedOperations.Mapdt_Categorical.
A: Type
decorateT A =
dist T (fun A : Type => A) ∘ map id ∘ dec T
    rewrite (dist_unit (F := T)).
A: Type
decorateT A = id ∘ map id ∘ dec T
    rewrite (fun_map_id (F := T)).
A: Type
decorateT A = id ∘ id ∘ dec T
    reflexivity.
  Qed.

End Roundtrip1.

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

  Context
    (E: Type)
    (T: Type -> Type)
    `{mapdtT: Mapdt E T}
    `{! Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T}.

  #[local] Instance map': Map T :=
    DerivedOperations.Map_Mapdt.
  #[local] Instance dist': ApplicativeDist T :=
    DerivedOperations.Dist_Mapdt E T.
  #[local] Instance decorate': Decorate E T :=
    DerivedOperations.Decorate_Mapdt E T.

  Definition mapdt2: Mapdt E T :=
    DerivedOperations.Mapdt_Categorical E T.

  Goal forall G `{Applicative G},
      @mapdtT G _ _ _ = @mapdt2 G _ _ _.
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
mapdtT G Map_G Pure_G Mult_G =
mapdt2 G Map_G Pure_G Mult_G
  Proof.
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
mapdtT G Map_G Pure_G Mult_G =
mapdt2 G Map_G Pure_G Mult_G
    intros.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
mapdtT G Map_G Pure_G Mult_G =
mapdt2 G Map_G Pure_G Mult_G
    ext A B f.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt2 G Map_G Pure_G Mult_G A B f
    unfold mapdt2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
DerivedOperations.Mapdt_Categorical E T G Map_G Pure_G
  Mult_G A B f
    unfold DerivedOperations.Mapdt_Categorical.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
dist T G ∘ map f ∘ dec T
    unfold map.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
dist T G ∘ map' (E * A) (G B) f ∘ dec T
    unfold map'.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
dist T G ∘ DerivedOperations.Map_Mapdt (E * A) (G B) f
∘ dec T
    unfold DerivedOperations.Map_Mapdt.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
dist T G ∘ mapdt (f ∘ extract) ∘ dec T
    unfold dist.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
dist' G Map_G Pure_G Mult_G B ∘ mapdt (f ∘ extract)
∘ dec T
    unfold dist'.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
DerivedOperations.Dist_Mapdt E T G Map_G Pure_G Mult_G
  B ∘ mapdt (f ∘ extract) ∘ dec T
    unfold DerivedOperations.Dist_Mapdt.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt extract ∘ mapdt (f ∘ extract) ∘ dec T
    unfold dec.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt extract ∘ mapdt (f ∘ extract) ∘ decorate' A
    unfold decorate'.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt extract ∘ mapdt (f ∘ extract)
∘ DerivedOperations.Decorate_Mapdt E T A
    unfold DerivedOperations.Decorate_Mapdt.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt extract ∘ mapdt (f ∘ extract) ∘ mapdt id
    rewrite <- map_to_mapdt.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt extract ∘ map f ∘ mapdt id
    rewrite mapdt_map.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt (extract ∘ map f) ∘ mapdt id
    change (mapdt (extract ∘ map f))
      with (map (F := fun A => A) (mapdt (extract ∘ map f))).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
map (mapdt (extract ∘ map f)) ∘ mapdt id
    rewrite (kdtf_mapdt2 (G2 := G) (G1 := fun A => A)).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt (extract ∘ map f ⋆3 id)
    rewrite mapdt_app_id_l.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt (extract ∘ map f ⋆3 id)
    rewrite <- (natural (ϕ := fun A => extract)).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt (map f ∘ extract ⋆3 id)
    rewrite kc3_23.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f =
mapdt (map (map f) ∘ id)
    unfold_ops @Map_I.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: E * A -> G B
mapdtT G Map_G Pure_G Mult_G A B f = mapdt (f ∘ id)
    reflexivity.
  Qed.

End Roundtrip2.