DecoratedTraversableMonad.v

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

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

#[local] Generalizable Variable T W.

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

  Context
    `{Monoid W}
    `{mapT: Map T}
    `{distT: ApplicativeDist T}
    `{joinT: Join T}
    `{decorateT: Decorate W T}
    `{Return T}
    `{! Categorical.DecoratedTraversableMonad.DecoratedTraversableMonad W T}.

  #[local] Instance binddt': Binddt W T T :=
    DerivedOperations.Binddt_Categorical W T.

  Definition map': Map T :=
    DerivedOperations.Map_Binddt W T T.
  Definition join': Join T :=
    DerivedOperations.Join_Binddt W T.
  Definition decorate': Decorate W T :=
    DerivedOperations.Decorate_Binddt W T.
  Definition dist': ApplicativeDist T :=
    DerivedOperations.Dist_Binddt W T.

  Goal mapT = map'.mapT = map'
  Proof.mapT = map'
    unfold map'.mapT = DerivedOperations.Map_Binddt W T T unfold_ops @DerivedOperations.Map_Binddt.mapT =
(fun (A B : Type) (f : A -> B) =>
 binddt (ret ∘ f ∘ extract))
    unfold binddt, binddt'.mapT =
(fun (A B : Type) (f : A -> B) =>
 DerivedOperations.Binddt_Categorical W T
   (fun A0 : Type => A0) Map_I Pure_I Mult_I A B
   (ret ∘ f ∘ extract))
    unfold_ops @DerivedOperations.Binddt_Categorical.mapT =
(fun (A B : Type) (f : A -> B) =>
 map join ∘ dist T (fun A0 : Type => A0)
 ∘ map (ret ∘ f ∘ extract) ∘ dec T)
    ext A B f.A, B: Type
f: A -> B
mapT A B f =
map join ∘ dist T (fun A : Type => A)
∘ map (ret ∘ f ∘ extract) ∘ dec T
    unfold_ops @Map_I.A, B: Type
f: A -> B
mapT A B f =
join ∘ dist T (fun A : Type => A)
∘ map (ret ∘ f ∘ extract) ∘ dec T
    rewrite (dist_unit (F := T)).A, B: Type
f: A -> B
mapT A B f =
join ∘ id ∘ map (ret ∘ f ∘ extract) ∘ dec T
    change (?f ∘ id) with f.A, B: Type
f: A -> B
mapT A B f = join ∘ map (ret ∘ f ∘ extract) ∘ dec T
    do 2 rewrite <- (fun_map_map (F := T)).A, B: Type
f: A -> B
mapT A B f =
join ∘ (map ret ∘ map f ∘ map extract) ∘ dec T
    do 2 reassociate <- on right.A, B: Type
f: A -> B
mapT A B f =
join ∘ map ret ∘ map f ∘ map extract ∘ dec T
    rewrite (mon_join_map_ret (T := T)).A, B: Type
f: A -> B
mapT A B f = id ∘ map f ∘ map extract ∘ dec T
    change (id ∘ ?f) with f.A, B: Type
f: A -> B
mapT A B f = map f ∘ map extract ∘ dec T
    reassociate -> on right.A, B: Type
f: A -> B
mapT A B f = map f ∘ (map extract ∘ dec T)
    rewrite (dfun_dec_extract (E := W) (F := T)).A, B: Type
f: A -> B
mapT A B f = map f ∘ id
    reflexivity.
  Qed.

  Goal forall G `{Applicative G}, @distT G _ _ _ = @dist' G _ _ _.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
distT G Map_G Pure_G Mult_G =
dist' 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 ->
distT G Map_G Pure_G Mult_G =
dist' G Map_G Pure_G Mult_G
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
distT G Map_G Pure_G Mult_G =
dist' G Map_G Pure_G Mult_G
    unfold dist'.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
distT G Map_G Pure_G Mult_G =
DerivedOperations.Dist_Binddt W T G Map_G Pure_G
  Mult_G unfold_ops @DerivedOperations.Dist_Binddt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
distT G Map_G Pure_G Mult_G =
(fun A : Type => binddt (map ret ∘ extract))
    unfold binddt, binddt'.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
distT G Map_G Pure_G Mult_G =
(fun A : Type =>
 DerivedOperations.Binddt_Categorical W T G Map_G
   Pure_G Mult_G (G A) A (map ret ∘ extract))
    unfold_ops @DerivedOperations.Binddt_Categorical.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
distT G Map_G Pure_G Mult_G =
(fun A : Type =>
 map join ∘ dist T G ∘ map (map ret ∘ extract) ∘ dec T)
    ext A.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ dist T G ∘ map (map ret ∘ extract) ∘ dec T
    rewrite <- (fun_map_map (F := T)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ dist T G ∘ (map (map ret) ∘ map extract)
∘ dec T
    unfold_compose_in_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ dist T G ∘ (map (map ret) ∘ map extract)
∘ dec T
    reassociate <- on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ dist T G ∘ map (map ret) ∘ map extract
∘ dec T
    reassociate -> near (map (map (ret))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ (dist T G ∘ map (map ret)) ∘ map extract
∘ dec T
    change (map (map (ret)))
      with ((map (F := T ○ G) (ret (A := A)))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ (dist T G ∘ map ret) ∘ map extract ∘ dec T
    rewrite <- (natural (ϕ := @dist T _ G _ _ _)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ (map ret ∘ dist T G) ∘ map extract ∘ dec T
    unfold_ops @Map_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ (map (map ret) ∘ dist T G) ∘ map extract
∘ dec T
    reassociate <- on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
distT G Map_G Pure_G Mult_G A =
map join ∘ map (map ret) ∘ dist T G ∘ map extract
∘ dec T
    inversion H2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map left_unitor (mult (pure tt, x)) = x
app_unital_r: forall (A : Type) (x : G A),
map right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
distT G Map_G Pure_G Mult_G A =
map join ∘ map (map ret) ∘ dist T G ∘ map extract
∘ dec T
    rewrite (fun_map_map (F := G)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map left_unitor (mult (pure tt, x)) = x
app_unital_r: forall (A : Type) (x : G A),
map right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
distT G Map_G Pure_G Mult_G A =
map (join ∘ map ret) ∘ dist T G ∘ map extract ∘ dec T
    rewrite (mon_join_map_ret (T := T)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map left_unitor (mult (pure tt, x)) = x
app_unital_r: forall (A : Type) (x : G A),
map right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
distT G Map_G Pure_G Mult_G A =
map id ∘ dist T G ∘ map extract ∘ dec T
    rewrite (fun_map_id (F := G)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map left_unitor (mult (pure tt, x)) = x
app_unital_r: forall (A : Type) (x : G A),
map right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
distT G Map_G Pure_G Mult_G A =
id ∘ dist T G ∘ map extract ∘ dec T
    reassociate -> on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map left_unitor (mult (pure tt, x)) = x
app_unital_r: forall (A : Type) (x : G A),
map right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
distT G Map_G Pure_G Mult_G A =
id ∘ dist T G ∘ (map extract ∘ dec T)
    rewrite (dfun_dec_extract (E := W) (F := T)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
app_functor: Functor G
app_pure_natural: forall (A B : Type) (f : A -> B)
  (x : A),
map f (pure x) = pure (f x)
app_mult_natural: forall (A B C D : Type)
  (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
app_assoc: forall (A B C : Type) (x : G A) 
  (y : G B) (z : G C),
map α (mult (mult (x, y), z)) =
mult (x, mult (y, z))
app_unital_l: forall (A : Type) (x : G A),
map left_unitor (mult (pure tt, x)) = x
app_unital_r: forall (A : Type) (x : G A),
map right_unitor (mult (x, pure tt)) =
x
app_mult_pure: forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
distT G Map_G Pure_G Mult_G A = id ∘ dist T G ∘ id
    reflexivity.
  Qed.

  Goal joinT = join'.joinT = join'
  Proof.joinT = join'
    unfold join'.joinT = DerivedOperations.Join_Binddt W T unfold_ops @DerivedOperations.Join_Binddt.joinT = (fun A : Type => binddt extract)
    unfold binddt, binddt'.joinT =
(fun A : Type =>
 DerivedOperations.Binddt_Categorical W T
   (fun A0 : Type => A0) Map_I Pure_I Mult_I (T A) A
   extract)
    unfold_ops @DerivedOperations.Binddt_Categorical.joinT =
(fun A : Type =>
 map join ∘ dist T (fun A0 : Type => A0) ∘ map extract
 ∘ dec T)
    ext A.A: Type
joinT A =
map join ∘ dist T (fun A : Type => A) ∘ map extract
∘ dec T
    rewrite (dist_unit (F := T)).A: Type
joinT A = map join ∘ id ∘ map extract ∘ dec T
    reassociate -> on right.A: Type
joinT A = map join ∘ id ∘ (map extract ∘ dec T)
    rewrite (dfun_dec_extract (E := W) (F := T)).A: Type
joinT A = map join ∘ id ∘ id
    reflexivity.
  Qed.

  Goal decorateT = decorate'.decorateT = decorate'
  Proof.decorateT = decorate'
    unfold decorate'.decorateT = DerivedOperations.Decorate_Binddt W T unfold_ops @DerivedOperations.Decorate_Binddt.decorateT = (fun A : Type => binddt ret)
    unfold binddt, binddt'.decorateT =
(fun A : Type =>
 DerivedOperations.Binddt_Categorical W T
   (fun A0 : Type => A0) Map_I Pure_I Mult_I A (W * A)
   ret)
    unfold_ops @DerivedOperations.Binddt_Categorical @Map_I.decorateT =
(fun A : Type =>
 join ∘ dist T (fun A0 : Type => A0) ∘ map ret ∘ dec T)
    ext A.A: Type
decorateT A =
join ∘ dist T (fun A : Type => A) ∘ map ret ∘ dec T
    rewrite (dist_unit (F := T)).A: Type
decorateT A = join ∘ id ∘ map ret ∘ dec T
    change (?f ∘ id) with f.A: Type
decorateT A = join ∘ map ret ∘ dec T
    rewrite (mon_join_map_ret (T := T)).A: Type
decorateT A = id ∘ dec T
    reflexivity.
  Qed.

End Roundtrip1.

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

  Section section.

    Context
      `{Kleisli.DecoratedTraversableMonad.DecoratedTraversableMonad W T}.

    Definition map': Map T :=
      DerivedOperations.Map_Binddt W T T.
    Definition dist': ApplicativeDist T :=
      DerivedOperations.Dist_Binddt W T.
    Definition join': Join T :=
      DerivedOperations.Join_Binddt W T.
    Definition decorate': Decorate W T :=
      DerivedOperations.Decorate_Binddt W T.

    Definition binddt2: Binddt W T T :=
      DerivedOperations.Binddt_Categorical W T
        (H := map') (H0 := decorate') (H2 := join') (H1 := dist').

    #[local] Tactic Notation "binddt_to_bindd" :=
      rewrite <- bindd_to_binddt.
    #[local] Tactic Notation "binddt_to_bindt" :=
      rewrite <- bindt_to_binddt.
    #[local] Tactic Notation "bindd_to_map" :=
      rewrite <- map_to_bindd.

    Import Kleisli.DecoratedTraversableMonad.DerivedOperations.
    Import Kleisli.DecoratedTraversableMonad.DerivedInstances.

    Goal forall G `{Applicative G},
        @binddt W T T _ G _ _ _ = @binddt2 G _ _ _ .W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
@binddt W T T Bindd_T_inst G Map_G Pure_G Mult_G =
binddt2 G Map_G Pure_G Mult_G
    Proof.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
@binddt W T T Bindd_T_inst G Map_G Pure_G Mult_G =
binddt2 G Map_G Pure_G Mult_G
      intros.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
@binddt W T T Bindd_T_inst G Map_G Pure_G Mult_G =
binddt2 G Map_G Pure_G Mult_G
      ext A B f.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = binddt2 G Map_G Pure_G Mult_G A B f
      unfold binddt2.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
DerivedOperations.Binddt_Categorical W T G Map_G
  Pure_G Mult_G A B f
      unfold DerivedOperations.Binddt_Categorical.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = map join ∘ dist T G ∘ map f ∘ dec T
      unfold map at 2, map', DerivedOperations.Map_Binddt.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ dist T G ∘ binddt (ret ∘ f ∘ extract)
∘ dec T
      unfold dist, dist', DerivedOperations.Dist_Binddt.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ binddt (map ret ∘ extract)
∘ binddt (ret ∘ f ∘ extract) ∘ dec T
      unfold dec, decorate', DerivedOperations.Decorate_Binddt.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ binddt (map ret ∘ extract)
∘ binddt (ret ∘ f ∘ extract) ∘ binddt ret
      rewrite <- bindd_to_binddt.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ binddt (map ret ∘ extract)
∘ bindd (ret ∘ f ∘ extract) ∘ binddt ret
      binddt_to_bindd.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ binddt (map ret ∘ extract)
∘ bindd (ret ∘ f ∘ extract) ∘ bindd ret
      binddt_to_bindt.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ bindt (map ret) ∘ bindd (ret ∘ f ∘ extract)
∘ bindd ret
      bindd_to_map.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ bindt (map ret) ∘ map f ∘ bindd ret
      reassociate -> on right.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ bindt (map ret) ∘ (map f ∘ bindd ret)
      unfold map'.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ bindt (map ret) ∘ (map f ∘ bindd ret)
      rewrite map_bindd.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ bindt (map ret) ∘ bindd (map f ∘ ret)
      reassociate -> on right.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ (bindt (map ret) ∘ bindd (map f ∘ ret))
      unfold_compose_in_compose.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ (bindt (map ret) ∘ bindd (map f ∘ ret))
      rewrite (bindt_bindd).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ binddt (bindt (map ret) ∘ (map f ∘ ret))
      reassociate <- on right.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ binddt (bindt (map ret) ∘ map f ∘ ret)
      rewrite (bindt_map).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
map join ∘ binddt (bindt (map ret ∘ f) ∘ ret)
      rewrite (ktm_bindt0).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = map join ∘ binddt (map ret ∘ f)
      unfold join, join'; unfold_ops @DerivedOperations.Join_Binddt.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = map (binddt extract) ∘ binddt (map ret ∘ f)
      unfold compose at 2.W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = map (binddt extract) ∘ binddt (map ret ∘ f)
      rewrite (kdtm_binddt2 (G1 := G) (G2 := fun A => A)).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
binddt
  (kc7 G (fun A : Type => A) extract (map ret ∘ f))
      rewrite (binddt_app_id_r).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f =
binddt
  (kc7 G (fun A : Type => A) extract (map ret ∘ f))
      rewrite (kc7_73).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = binddt (kc3 extract f)
      change (extract (W := (W ×)) (A := T B))
        with (id ∘ extract (W := (W ×)) (A := T B)).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = binddt (kc3 (id ∘ extract) f)
      rewrite (kc3_03).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = binddt (map id ∘ f)
      rewrite (fun_map_id (F := G)).W: Type
T: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
binddt f = binddt (id ∘ f)
      reflexivity.
    Qed.

  End section.
End Roundtrip2.