From Tealeaves Require Import
  Classes.Categorical.DecoratedTraversableFunctor
  Classes.Kleisli.DecoratedTraversableFunctor.

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

#[local] Generalizable Variables G ϕ.

(** * Kleisli DTFs from Categorical DTFs *)
(**********************************************************************)

(** ** Derived Operations *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Mapdt_Categorical
    (E: Type)
    (T: Type -> Type)
    `{Map T}
    `{Decorate E T}
    `{ApplicativeDist T}:
  Mapdt E T :=
  fun (G: Type -> Type) `{Map G} `{Pure G} `{Mult G}
      (A B: Type) (f: E * A -> G B) =>
    (dist T G ∘ map f ∘ dec T: T A -> G (T B)).

End DerivedOperations.

(** ** Derived Instances *)
(**********************************************************************)
Module DerivedInstances.

  Import DerivedOperations.

  Section with_functor.

    Context
      (E: Type)
      (T: Type -> Type)
      `{Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T}.

    Theorem mapdt_id: forall (A: Type),
        mapdt (G := fun A => A) (extract (W := (E ×))) = @id (T A).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, mapdt extract = id
    Proof.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, mapdt extract = id
      introv.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapdt extract = id unfold_ops @Mapdt_Categorical.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
dist T (fun A : Type => A) ∘ map extract ∘ dec T = id
      reassociate -> on left.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
dist T (fun A : Type => A) ∘ (map extract ∘ dec T) =
id
      rewrite (dfun_dec_extract (E := E) (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
dist T (fun A : Type => A) ∘ id = id
      rewrite (dist_unit (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
id ∘ id = id
      reflexivity.
    Qed.

    Theorem mapdt_mapdt:
      forall `{Applicative G1} `{Applicative G2}
             (A B C: Type) (g: E * B -> G2 C) (f: E * A -> G1 B),
        map (mapdt g) ∘ mapdt f = mapdt (G := G1 ∘ G2) (g ⋆3 f).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : E * B -> G2 C)
  (f : E * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
    Proof.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : E * B -> G2 C)
  (f : E * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
      intros.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f) unfold transparent tcs.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2 ∘ map g ∘ dec T)
∘ (dist T G1 ∘ map f ∘ dec T) =
dist T (G1 ∘ G2) ∘ map (g ⋆3 f) ∘ dec T unfold kc3.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2 ∘ map g ∘ dec T)
∘ (dist T G1 ∘ map f ∘ dec T) =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      rewrite <- (fun_map_map (F := G1)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2 ∘ map g) ∘ map (dec T)
∘ (dist T G1 ∘ map f ∘ dec T) =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      repeat reassociate <- on left.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2 ∘ map g) ∘ map (dec T) ∘ dist T G1
∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      change (?f ∘ map (dec T) ∘ dist T G1 ∘ ?g) with
        (f ∘ (map (F := G1) (dec T) ∘ dist T G1) ∘ g).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2 ∘ map g) ∘ (map (dec T) ∘ dist T G1)
∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      rewrite <- (dtfun_compat (E := E) (F := T) B).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2 ∘ map g)
∘ (dist T G1 ∘ map strength ∘ dec T) ∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      rewrite <- (fun_map_map (F := G1)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ map (map g)
∘ (dist T G1 ∘ map strength ∘ dec T) ∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      repeat reassociate <- on left.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ map (map g) ∘ dist T G1
∘ map strength ∘ dec T ∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      change (?f ∘ map (map g) ∘ dist T G1 ∘ ?h) with
        (f ∘ (map (F := G1) (map (F := T) g) ∘ dist T G1) ∘ h).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ (map (map g) ∘ dist T G1)
∘ map strength ∘ dec T ∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      change (map (map g)) with (map (F := G1 ∘ T) g).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ (map g ∘ dist T G1) ∘ map strength
∘ dec T ∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      rewrite (natural (ϕ := @dist T _ G1 _ _ _)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ (dist T G1 ∘ map g) ∘ map strength
∘ dec T ∘ map f ∘ dec T =
dist T (G1 ∘ G2) ∘ map (map g ∘ strength ∘ cobind f)
∘ dec T
      rewrite (dist_linear (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ (dist T G1 ∘ map g) ∘ map strength
∘ dec T ∘ map f ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ map (map g ∘ strength ∘ cobind f) ∘ dec T
      repeat reassociate <- on left.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ dist T G1 ∘ map g ∘ map strength
∘ dec T ∘ map f ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ map (map g ∘ strength ∘ cobind f) ∘ dec T
      rewrite <- (fun_map_map (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ dist T G1 ∘ map g ∘ map strength
∘ dec T ∘ map f ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ (map (map g ∘ strength) ∘ map (cobind f)) ∘ dec T
      unfold_ops @Map_compose.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ dist T G1 ∘ map (map g)
∘ map strength ∘ dec T ∘ map f ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ (map (map g ∘ strength) ∘ map (cobind f)) ∘ dec T
      change (?f ∘ map (map g) ∘ ?x ∘ ?h) with
        (f ∘ (map (F := T) (map (F := G1) g) ∘ x) ∘ h).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ dist T G1
∘ (map (map g) ∘ map strength) ∘ dec T ∘ map f ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ (map (map g ∘ strength) ∘ map (cobind f)) ∘ dec T
      rewrite (fun_map_map (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ dist T G1 ∘ map (map g ∘ strength)
∘ dec T ∘ map f ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ (map (map g ∘ strength) ∘ map (cobind f)) ∘ dec T
      reassociate -> near (map f).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ dist T G1 ∘ map (map g ∘ strength)
∘ (dec T ∘ map f) ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ (map (map g ∘ strength) ∘ map (cobind f)) ∘ dec T
      rewrite <- (natural (ϕ := @dec E T _)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2) ∘ dist T G1 ∘ map (map g ∘ strength)
∘ (map f ∘ dec T) ∘ dec T =
map (dist T G2) ∘ dist T G1
∘ (map (map g ∘ strength) ∘ map (cobind f)) ∘ dec T
      repeat reassociate ->.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (dist T G2)
∘ (dist T G1
   ∘ (map (map g ∘ strength)
      ∘ (map f ∘ (dec T ∘ dec T)))) =
map (dist T G2)
∘ (dist T G1
   ∘ (map (map g ∘ strength)
      ∘ (map (cobind f) ∘ dec T)))
      repeat fequal.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map f ∘ (dec T ∘ dec T) = map (cobind f) ∘ dec T
      rewrite (dfun_dec_dec (E := E) (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map f ∘ (map cojoin ∘ dec T) = map (cobind f) ∘ dec T
      reassociate <-.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map f ∘ map cojoin ∘ dec T = map (cobind f) ∘ dec T unfold_ops @Map_compose.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (map f) ∘ map cojoin ∘ dec T =
map (cobind f) ∘ dec T
      rewrite (fun_map_map (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map (map f ∘ cojoin) ∘ dec T = map (cobind f) ∘ dec T
      do 2 fequal.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H3: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H4: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> G1 B
map f ∘ cojoin = cobind f now ext [e a].
    Qed.

    Theorem mapdt_mapdt_morphism:
      forall `{ApplicativeMorphism G1 G2 ϕ}
        (A B: Type) (f: E * A -> G1 B),
        ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 G2 : Type -> Type) (H3 : Map G1)
  (H4 : Mult G1) (H5 : Pure G1) (H6 : Map G2)
  (H7 : Mult G2) (H8 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : E * A -> G1 B),
ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f)
    Proof.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 G2 : Type -> Type) (H3 : Map G1)
  (H4 : Mult G1) (H5 : Pure G1) (H6 : Map G2)
  (H7 : Mult G2) (H8 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : E * A -> G1 B),
ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f)
      intros.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> Type
H3: Map G1
H4: Mult G1
H5: Pure G1
H6: Map G2
H7: Mult G2
H8: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H9: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f) unfold transparent tcs.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> Type
H3: Map G1
H4: Mult G1
H5: Pure G1
H6: Map G2
H7: Mult G2
H8: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H9: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (T B) ∘ (dist T G1 ∘ map f ∘ dec T) =
dist T G2 ∘ map (ϕ B ∘ f) ∘ dec T
      do 2 reassociate <-.
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> Type
H3: Map G1
H4: Mult G1
H5: Pure G1
H6: Map G2
H7: Mult G2
H8: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H9: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (T B) ∘ dist T G1 ∘ map f ∘ dec T =
dist T G2 ∘ map (ϕ B ∘ f) ∘ dec T
      rewrite <- (fun_map_map (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> Type
H3: Map G1
H4: Mult G1
H5: Pure G1
H6: Map G2
H7: Mult G2
H8: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H9: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (T B) ∘ dist T G1 ∘ map f ∘ dec T =
dist T G2 ∘ (map (ϕ B) ∘ map f) ∘ dec T
      rewrite <- (dist_morph (F := T)).
E: Type
T: Type -> Type
H: Map T
H0: Decorate E T
H1: ApplicativeDist T
H2: Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> Type
H3: Map G1
H4: Mult G1
H5: Pure G1
H6: Map G2
H7: Mult G2
H8: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H9: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
dist T G2 ∘ map (ϕ B) ∘ map f ∘ dec T =
dist T G2 ∘ (map (ϕ B) ∘ map f) ∘ dec T
      reflexivity.
    Qed.

    (** ** Typeclass Instance *)
    (******************************************************************)
    #[export] Instance:
      Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T :=
      {| kdtf_mapdt1 := @mapdt_id;
         kdtf_mapdt2 := @mapdt_mapdt;
         kdtf_morph := @mapdt_mapdt_morphism;
      |}.

  End with_functor.

End DerivedInstances.