From Tealeaves Require Export
  Classes.Categorical.Applicative
  Classes.Kleisli.Comonad
  Classes.Kleisli.DecoratedFunctor
  Classes.Kleisli.TraversableFunctor
  Functors.Early.Reader.

Import Monoid.Notations.
Import Strength.Notations.
Import TraversableFunctor.Notations.
Import Comonad.Notations.
Import Product.Notations.

#[local] Generalizable Variables E T ϕ G A B C M.

(** * Decorated Traversable Functor *)
(**********************************************************************)

(** ** Operation <<mapdt>> *)
(**********************************************************************)
Class Mapdt (E: Type) (T: Type -> Type) :=
  mapdt: forall (G: Type -> Type) `{Map G} `{Pure G} `{Mult G}
           (A B: Type), (E * A -> G B) -> T A -> G (T B).

#[global] Arguments mapdt {E}%type_scope {T}%function_scope {Mapdt}
  {G}%function_scope {H H0 H1} {A B}%type_scope _%function_scope _.

(** ** Kleisli Composition *)
(**********************************************************************)
Definition kc3
  {E A B C: Type}
  {G1 G2: Type -> Type}
  `{Map G1} `{Pure G1} `{Mult G1}
  `{Map G2} `{Pure G2} `{Mult G2}
  (g: E * B -> G2 C)
  (f: E * A -> G1 B):
  (E * A -> G1 (G2 C)) :=
  map (F := G1) (A := E * B) (B := G2 C) g ∘ strength ∘ cobind f.

#[local] Infix "⋆3" := kc3 (at level 60): tealeaves_scope.

(** ** Typeclass *)
(**********************************************************************)
Class DecoratedTraversableFunctor
  (E: Type) (T: Type -> Type) `{Mapdt E T} :=
  { kdtf_mapdt1: forall (A: Type),
      mapdt (G := fun A => A) extract = @id (T A);
    kdtf_mapdt2:
    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);
    kdtf_morph: forall `{morphism: ApplicativeMorphism G1 G2 ϕ}
                  {A B: Type} (f: E * A -> G1 B),
      ϕ (T B) ∘ mapdt f = mapdt (ϕ B ∘ f);
  }.

(** ** Kleisli Category Laws *)
(** TODO: The left and right unit are simply <<extract>> with <<G>> =
    <<fun A => A>> *)
(**********************************************************************)


(** * Derived Structures *)
(**********************************************************************)

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

    Context
      `{Mapdt_ET: Mapdt E T}.

    #[export] Instance Mapd_Mapdt: Mapd E T :=
      fun A B f => mapdt (G := fun A => A) f.
    #[export] Instance Traverse_Mapdt: Traverse T :=
      fun G _ _ _ A B f => mapdt (f ∘ extract).
    #[export] Instance Map_Mapdt: Map T :=
      fun A B f => mapdt (G := fun A => A) (f ∘ extract).

  End operations.
End DerivedOperations.

Section compat.

  Context
    (E: Type)
    (T: Type -> Type)
    `{Map_T: Map T}
    `{Mapd_ET: Mapd E T}
    `{Traverse_T: Traverse T}
    `{Mapdt_ET: Mapdt E T}.

  Class Compat_Map_Mapdt: Prop :=
    compat_map_mapdt:
      @Map_T = @DerivedOperations.Map_Mapdt E T Mapdt_ET.

  Class Compat_Mapd_Mapdt: Prop :=
    compat_mapd_mapdt:
      @Mapd_ET = @DerivedOperations.Mapd_Mapdt E T Mapdt_ET.

  Class Compat_Traverse_Mapdt: Prop :=
    compat_traverse_mapdt:
      @Traverse_T =
        @DerivedOperations.Traverse_Mapdt E T Mapdt_ET.
(*
  forall {G: Type -> Type}
  `{Map_G: Map G}
  `{Mult_G: Mult G}
  `{Pure_G: Pure G}
  `{! Applicative G},
  @Traverse_T G Map_G Pure_G Mult_G =
  @DerivedOperations.Traverse_Mapdt E T Mapdt_ET G Map_G Pure_G Mult_G.
 *)

End compat.

Section rewriting.

  Context
    `{Map_T: Map T}
    `{Mapd_ET: Mapd E T}
    `{Traverse_T: Traverse T}
    `{Mapdt_ET: Mapdt E T}
    `{! Compat_Map_Mapdt E T}
    `{! Compat_Mapd_Mapdt E T}
    `{! Compat_Traverse_Mapdt E T}.

  Definition traverse_to_mapdt
    `{Applicative G}: forall `(f: A -> G B),
      traverse (T := T) f = mapdt (f ∘ extract).
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> G B),
traverse f = mapdt (f ∘ extract)
  Proof.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> G B),
traverse f = mapdt (f ∘ extract)
    rewrite (compat_traverse_mapdt E T).
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> G B),
DerivedOperations.Traverse_Mapdt G Map_G Pure_G Mult_G
  A B f = mapdt (f ∘ extract)
    reflexivity.
  Qed.

  Definition mapd_to_mapdt: forall `(f: E * A -> B),
      mapd f = mapdt (T := T) (G := fun A => A) f :=
    ltac:(now rewrite (compat_mapd_mapdt E T)).

  Definition map_to_mapdt: forall `(f: A -> B),
      map f = mapdt (T := T) (G := fun A => A) (f ∘ extract) :=
    ltac:(now rewrite (compat_map_mapdt E T)).

  Corollary map_to_mapd: forall `(f: A -> B),
      map f = mapd (T := T) (f ∘ extract).
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
  Proof.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
    intros.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
A, B: Type
f: A -> B
map f = mapd (f ∘ extract)
    rewrite map_to_mapdt.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
A, B: Type
f: A -> B
mapdt (f ∘ extract) = mapd (f ∘ extract)
    rewrite mapd_to_mapdt.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
A, B: Type
f: A -> B
mapdt (f ∘ extract) = mapdt (f ∘ extract)
    reflexivity.
  Qed.

  Corollary map_to_traverse: forall `(f: A -> B),
      map f = traverse (T := T) (G := fun A => A) f.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
forall (A B : Type) (f : A -> B), map f = traverse f
  Proof.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
forall (A B : Type) (f : A -> B), map f = traverse f
    intros.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
A, B: Type
f: A -> B
map f = traverse f
    rewrite map_to_mapdt.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
A, B: Type
f: A -> B
mapdt (f ∘ extract) = traverse f
    rewrite traverse_to_mapdt.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
A, B: Type
f: A -> B
mapdt (f ∘ extract) = mapdt (f ∘ extract)
    reflexivity.
  Qed.

End rewriting.

#[export] Instance Compat_Map_Mapdt_Self `{Mapdt_ET: Mapdt E T}:
  Compat_Map_Mapdt E T
    (Map_T := DerivedOperations.Map_Mapdt)
  := ltac:(reflexivity).

#[export] Instance Compat_Mapd_Mapdt_Self `{Mapdt_inst: Mapdt E T}:
  Compat_Mapd_Mapdt E T
    (Mapd_ET := DerivedOperations.Mapd_Mapdt)
  := ltac:(reflexivity).

#[export] Instance Compat_Traverse_Mapdt_Self `{Mapdt_inst: Mapdt E T}:
  Compat_Traverse_Mapdt E T
    (Traverse_T := DerivedOperations.Traverse_Mapdt) :=
  ltac:(hnf; reflexivity).

#[export] Instance Compat_Map_Mapd_Mapdt
  `{Map_T: Map T}
  `{Mapd_ET: Mapd E T}
  `{Mapdt_ET: Mapdt E T}
  `{! Compat_Map_Mapdt E T}
  `{! Compat_Mapd_Mapdt E T}:
  Compat_Map_Mapd E T.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Map_Mapd E T
Proof.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Map_Mapd E T
  hnf.
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Map_T = DerivedOperations.Map_Mapd E T
  rewrite (compat_map_mapdt E T).
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
DerivedOperations.Map_Mapdt =
DerivedOperations.Map_Mapd E T
  rewrite (compat_mapd_mapdt E T).
T: Type -> Type
Map_T: Map T
E: Type
Mapd_ET: Mapd E T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
DerivedOperations.Map_Mapdt =
DerivedOperations.Map_Mapd E T
  reflexivity.
Qed.

#[export] Instance Compat_Map_Traverse_Mapdt
  `{Map_T: Map T}
  `{Traverse_T: Traverse T}
  `{Mapdt_ET: Mapdt E T}
  `{! Compat_Map_Mapdt E T}
  `{! Compat_Traverse_Mapdt E T}:
  Compat_Map_Traverse T.
T: Type -> Type
Map_T: Map T
Traverse_T: Traverse T
E: Type
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
Compat_Map_Traverse T
Proof.
T: Type -> Type
Map_T: Map T
Traverse_T: Traverse T
E: Type
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
Compat_Map_Traverse T
  hnf.
T: Type -> Type
Map_T: Map T
Traverse_T: Traverse T
E: Type
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
Map_T = DerivedOperations.Map_Traverse T
  rewrite (compat_map_mapdt E T).
T: Type -> Type
Map_T: Map T
Traverse_T: Traverse T
E: Type
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DerivedOperations.Map_Mapdt =
DerivedOperations.Map_Traverse T
  rewrite (compat_traverse_mapdt E T).
T: Type -> Type
Map_T: Map T
Traverse_T: Traverse T
E: Type
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DerivedOperations.Map_Mapdt =
DerivedOperations.Map_Traverse T
  reflexivity.
Qed.

(** ** Composition with the Identity Applicative Functor *)
(**********************************************************************)
Section mapdt_identity_applicative.

  #[local] Arguments mapdt E%type_scope T%function_scope {Mapdt}
    G%function_scope (H H0 H1) (A B)%type_scope _%function_scope _.

  Context
    `{DecoratedTraversableFunctor E T}.

  Context
    {G: Type -> Type}
    {A B: Type}
    {mapG: Map G}
    {pureG: Pure G}
    {multG: Mult G}
    `{! Applicative G}.

  Lemma mapdt_app_id_l: forall (f: E * A -> G B),
      mapdt E T ((fun A => A) ∘ G)
        (Map_compose  (fun A => A) G)
        (Pure_compose (fun A => A) G)
        (Mult_compose (fun A => A) G)
        A B f = mapdt E T G mapG pureG multG A B f.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
forall f : E * A -> G B,
mapdt E T ((fun A : Type => A) ∘ G)
  (Map_compose (fun A : Type => A) G)
  (Pure_compose (fun A : Type => A) G)
  (Mult_compose (fun A : Type => A) G) A B f =
mapdt E T G mapG pureG multG A B f
  Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
forall f : E * A -> G B,
mapdt E T ((fun A : Type => A) ∘ G)
  (Map_compose (fun A : Type => A) G)
  (Pure_compose (fun A : Type => A) G)
  (Mult_compose (fun A : Type => A) G) A B f =
mapdt E T G mapG pureG multG A B f
    intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
mapdt E T ((fun A : Type => A) ∘ G)
  (Map_compose (fun A : Type => A) G)
  (Pure_compose (fun A : Type => A) G)
  (Mult_compose (fun A : Type => A) G) A B f =
mapdt E T G mapG pureG multG A B f cbv.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
H (fun a : Type => G a)
  (fun (A B : Type) (f : A -> B) => mapG A B f)
  (fun (A : Type) (a : A) => pureG A a)
  (fun (A B : Type) (p : G A * G B) =>
   multG A B
     (let (x, _) := p in x, let (_, y) := p in y)) A B
  f = H G mapG pureG multG A B f fequal.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
(fun (A B : Type) (p : G A * G B) =>
 multG A B
   (let (x, _) := p in x, let (_, y) := p in y)) =
multG ext A' B' p.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
A', B': Type
p: G A' * G B'
multG A' B'
  (let (x, _) := p in x, let (_, y) := p in y) =
multG A' B' p now destruct p.
  Qed.

  Lemma mapdt_app_id_r: forall (f: E * A -> G B),
      mapdt E T (G ∘ (fun A => A))
        (Map_compose  G (fun A => A))
        (Pure_compose G (fun A => A))
        (Mult_compose G (fun A => A))
        A B f = mapdt E T G mapG pureG multG A B f.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
forall f : E * A -> G B,
mapdt E T (G ∘ (fun A : Type => A))
  (Map_compose G (fun A : Type => A))
  (Pure_compose G (fun A : Type => A))
  (Mult_compose G (fun A : Type => A)) A B f =
mapdt E T G mapG pureG multG A B f
  Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
forall f : E * A -> G B,
mapdt E T (G ∘ (fun A : Type => A))
  (Map_compose G (fun A : Type => A))
  (Pure_compose G (fun A : Type => A))
  (Mult_compose G (fun A : Type => A)) A B f =
mapdt E T G mapG pureG multG A B f
    intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
mapdt E T (G ∘ (fun A : Type => A))
  (Map_compose G (fun A : Type => A))
  (Pure_compose G (fun A : Type => A))
  (Mult_compose G (fun A : Type => A)) A B f =
mapdt E T G mapG pureG multG A B f cbv.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
H (fun a : Type => G a)
  (fun (A B : Type) (f : A -> B) => mapG A B f)
  (fun (A : Type) (a : A) => pureG A a)
  (fun (A B : Type) (p : G A * G B) =>
   mapG (A * B) (A * B) (fun p0 : A * B => p0)
     (multG A B
        (let (x, _) := p in x, let (_, y) := p in y)))
  A B f = H G mapG pureG multG A B f fequal.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
(fun (A B : Type) (p : G A * G B) =>
 mapG (A * B) (A * B) (fun p0 : A * B => p0)
   (multG A B
      (let (x, _) := p in x, let (_, y) := p in y))) =
multG ext A' B' p.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
A', B': Type
p: G A' * G B'
mapG (A' * B') (A' * B') (fun p : A' * B' => p)
  (multG A' B'
     (let (x, _) := p in x, let (_, y) := p in y)) =
multG A' B' p
    destruct p.
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
A', B': Type
g: G A'
g0: G B'
mapG (A' * B') (A' * B') (fun p : A' * B' => p)
  (multG A' B' (g, g0)) = multG A' B' (g, g0)
    change (mapG (A' * B') (A' * B') (fun p: A' * B' => p))
      with (map (F := G) (@id (A' * B'))).
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
A', B': Type
g: G A'
g0: G B'
map id (multG A' B' (g, g0)) = multG A' B' (g, g0)
    rewrite (fun_map_id (F := G)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: DecoratedTraversableFunctor E T
G: Type -> Type
A, B: Type
mapG: Map G
pureG: Pure G
multG: Mult G
Applicative0: Applicative G
f: E * A -> G B
A', B': Type
g: G A'
g0: G B'
id (multG A' B' (g, g0)) = multG A' B' (g, g0)
    reflexivity.
  Qed.

End mapdt_identity_applicative.

(** ** Derived Kleisli Composition Laws *)
(**********************************************************************)
Section decorated_traversable_functor_derived_kleisli_laws.

  Context
    {E: Type} {T: Type -> Type}
    `{Map_inst: Map T}
    `{Mapd_inst: Mapd E T}
    `{Traverse_inst: Traverse T}
    `{Mapdt_inst: Mapdt E T}
    `{! Compat_Map_Mapdt E T}
    `{! Compat_Mapd_Mapdt E T}
    `{! Compat_Traverse_Mapdt E T}
    `{! DecoratedTraversableFunctor E T}.

  Lemma kc3_spec `{Applicative G2} `{Applicative G1}:
    forall (A B C: Type) (f: E * A -> G1 B) (g: E * B -> G2 C),
      g ⋆3 f =
        (fun '(w, a) => map (g ∘ pair w) (f (w, a))).
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
forall (A B C : Type) (f : E * A -> G1 B)
  (g : E * B -> G2 C),
g ⋆3 f = (fun '(w, a) => map (g ∘ pair w) (f (w, a)))
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
forall (A B C : Type) (f : E * A -> G1 B)
  (g : E * B -> G2 C),
g ⋆3 f = (fun '(w, a) => map (g ∘ pair w) (f (w, a)))
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
A, B, C: Type
f: E * A -> G1 B
g: E * B -> G2 C
g ⋆3 f = (fun '(w, a) => map (g ∘ pair w) (f (w, a))) unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
A, B, C: Type
f: E * A -> G1 B
g: E * B -> G2 C
map g ∘ σ ∘ cobind f =
(fun '(w, a) => map (g ∘ pair w) (f (w, a)))
    rewrite (map_strength_cobind_spec E).
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
A, B, C: Type
f: E * A -> G1 B
g: E * B -> G2 C
(fun '(e, a) => map (g ∘ pair e) (f (e, a))) =
(fun '(w, a) => map (g ∘ pair w) (f (w, a)))
    reflexivity.
  Qed.

  Import Monoid.

  Lemma kc3_preincr `{Monoid_op E} `{Applicative G2} `{Applicative G1}:
    forall (A B C: Type) (f: E * A -> G1 B) (g: E * B -> G2 C) (e: E),
      (g ⋆3 f) ⦿ e =
        (g  ⦿ e ⋆3 f ⦿ e).
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
H: Monoid_op E
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
forall (A B C : Type) (f : E * A -> G1 B)
  (g : E * B -> G2 C) (e : E),
(g ⋆3 f) ⦿ e = g ⦿ e ⋆3 f ⦿ e
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
H: Monoid_op E
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
forall (A B C : Type) (f : E * A -> G1 B)
  (g : E * B -> G2 C) (e : E),
(g ⋆3 f) ⦿ e = g ⦿ e ⋆3 f ⦿ e
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
H: Monoid_op E
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
A, B, C: Type
f: E * A -> G1 B
g: E * B -> G2 C
e: E
(g ⋆3 f) ⦿ e = g ⦿ e ⋆3 f ⦿ e
    do 2 rewrite kc3_spec.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
H: Monoid_op E
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
A, B, C: Type
f: E * A -> G1 B
g: E * B -> G2 C
e: E
(fun '(w, a) => map (g ∘ pair w) (f (w, a))) ⦿ e =
(fun '(w, a) => map (g ⦿ e ∘ pair w) ((f ⦿ e) (w, a)))
    ext [e' a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
H: Monoid_op E
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
A, B, C: Type
f: E * A -> G1 B
g: E * B -> G2 C
e, e': E
a: A
((fun '(w, a) => map (g ∘ pair w) (f (w, a))) ⦿ e)
  (e', a) = map (g ⦿ e ∘ pair e') ((f ⦿ e) (e', a))
    unfold compose; cbn.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
H: Monoid_op E
G2: Type -> Type
Map_G: Map G2
Pure_G: Pure G2
Mult_G: Mult G2
H0: Applicative G2
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H1: Applicative G1
A, B, C: Type
f: E * A -> G1 B
g: E * B -> G2 C
e, e': E
a: A
map (g ○ pair (e ● e')) (f (e ● e', a)) =
map (g ⦿ e ○ pair e') ((f ⦿ e) (e', a))
    reflexivity.
  Qed.

  Import Comonad.Notations.
  Import Product.Notations.

  Context
    `{Applicative G1}
    `{Applicative G2}
    (A B C: Type).

  (** *** Homogeneous cases *)
  (********************************************************************)
  Lemma kc3_11:
    forall (g: E * B -> C) (f: E * A -> B),
      kc3 (G1 := fun A => A) (G2 := fun A => A) g f = g ⋆1 f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> B),
g ⋆3 f = g ⋆1 f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> B),
g ⋆3 f = g ⋆1 f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
g ⋆3 f = g ⋆1 f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ σ ∘ cobind f = g ⋆1 f
    rewrite strength_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
map g ∘ id ∘ cobind f = g ⋆1 f
    unfold_ops @Map_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
g ∘ id ∘ cobind f = g ⋆1 f
    reflexivity.
  Qed.

  Lemma kc3_22:
    forall (g: B -> G2 C) (f: A -> G1 B),
      (g ∘ extract) ⋆3 (f ∘ extract) =
        map g ∘ f ∘ (extract (W := (E ×))).
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
g ∘ extract ⋆3 f ∘ extract = map g ∘ f ∘ extract
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
g ∘ extract ⋆3 f ∘ extract = map g ∘ f ∘ extract
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
g ∘ extract ⋆3 f ∘ extract = map g ∘ f ∘ extract
    unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (g ∘ extract) ∘ σ ∘ cobind (f ∘ extract) =
map g ∘ f ∘ extract
    rewrite <- map_to_cobind.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (g ∘ extract) ∘ σ ∘ map f = map g ∘ f ∘ extract
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
e: E
a: A
(map (g ∘ extract) ∘ σ ∘ map f) (e, a) =
(map g ∘ f ∘ extract) (e, a)
    do 2 (unfold compose; cbn).
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
e: E
a: A
map (g ○ extract) (map (pair (id e)) (f a)) =
map g (f a)
    compose near (f a) on left.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
e: E
a: A
(map (g ○ extract) ∘ map (pair (id e))) (f a) =
map g (f a)
    rewrite fun_map_map.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
e: E
a: A
map (g ○ extract ∘ pair (id e)) (f a) = map g (f a)
    reflexivity.
  Qed.

  Lemma kc3_00:
    forall (f: A -> B) (g: B -> C),
      kc3 (G1 := fun A => A) (G2 := fun A => A)
        (g ∘ extract) (f ∘ extract) =
        g ∘ f ∘ extract (W := (E ×)).
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (f : A -> B) (g : B -> C),
g ∘ extract ⋆3 f ∘ extract = g ∘ f ∘ extract
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (f : A -> B) (g : B -> C),
g ∘ extract ⋆3 f ∘ extract = g ∘ f ∘ extract
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
f: A -> B
g: B -> C
g ∘ extract ⋆3 f ∘ extract = g ∘ f ∘ extract unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
f: A -> B
g: B -> C
map (g ∘ extract) ∘ σ ∘ cobind (f ∘ extract) =
g ∘ f ∘ extract
    unfold_ops @Map_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
f: A -> B
g: B -> C
g ∘ extract ∘ σ ∘ cobind (f ∘ extract) =
g ∘ f ∘ extract
    rewrite strength_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
f: A -> B
g: B -> C
g ∘ extract ∘ id ∘ cobind (f ∘ extract) =
g ∘ f ∘ extract
    change (?f ∘ id) with f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
f: A -> B
g: B -> C
g ∘ extract ∘ cobind (f ∘ extract) = g ∘ f ∘ extract
    reassociate ->.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
f: A -> B
g: B -> C
g ∘ (extract ∘ cobind (f ∘ extract)) = g ∘ f ∘ extract
    rewrite kcom_cobind0.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
f: A -> B
g: B -> C
g ∘ (f ∘ extract) = g ∘ f ∘ extract
    reflexivity.
  Qed.

  (** *** Heterogeneous cases *)
  (********************************************************************)

  (** **** [3x] *)
  (********************************************************************)
  Lemma kc3_31:
    forall (g: E * B -> G2 C)
           (f: E * A -> B),
      g ⋆3 f = g ⋆1 f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : E * A -> B),
g ⋆3 f = g ⋆1 f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : E * A -> B),
g ⋆3 f = g ⋆1 f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
g ⋆3 f = g ⋆1 f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
map g ∘ σ ∘ cobind f = g ⋆1 f
    unfold strength.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
map g ∘ (fun '(a, t) => map (pair a) t) ∘ cobind f =
g ⋆1 f
    ext [w a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
w: E
a: A
(map g ∘ (fun '(a, t) => map (pair a) t) ∘ cobind f)
  (w, a) = (g ⋆1 f) (w, a)
    reflexivity.
  Qed.

  Lemma kc3_32:
    forall (g: E * B -> G2 C) (f: A -> G1 B),
      g ⋆3 (f ∘ extract) = map g ∘ σ ∘ map f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> G1 B),
g ⋆3 f ∘ extract = map g ∘ σ ∘ map f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> G1 B),
g ⋆3 f ∘ extract = map g ∘ σ ∘ map f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
g ⋆3 f ∘ extract = map g ∘ σ ∘ map f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
map g ∘ σ ∘ cobind (f ∘ extract) = map g ∘ σ ∘ map f
    ext [w a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
w: E
a: A
(map g ∘ σ ∘ cobind (f ∘ extract)) (w, a) =
(map g ∘ σ ∘ map f) (w, a)
    rewrite <- map_to_cobind.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
w: E
a: A
(map g ∘ σ ∘ map f) (w, a) =
(map g ∘ σ ∘ map f) (w, a)
    unfold compose; cbn.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
w: E
a: A
map g (map (pair (id w)) (f a)) =
map g (map (pair (id w)) (f a))
    reflexivity.
  Qed.

  Lemma kc3_30:
    forall (g: E * B -> G2 C) (f: A -> B),
      g ⋆3 (f ∘ extract) = g ∘ map f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> B),
g ⋆3 f ∘ extract = g ∘ map f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> B),
g ⋆3 f ∘ extract = g ∘ map f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
g ⋆3 f ∘ extract = g ∘ map f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
map g ∘ σ ∘ cobind (f ∘ extract) = g ∘ map f
    rewrite strength_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
map g ∘ id ∘ cobind (f ∘ extract) = g ∘ map f
    unfold_ops @Map_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
g ∘ id ∘ cobind (f ∘ extract) = g ∘ map f
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
e: E
a: A
(g ∘ id ∘ cobind (f ∘ extract)) (e, a) =
(g ∘ map f) (e, a)
    reflexivity.
  Qed.

  (** **** [x3] *)
  (********************************************************************)
  Lemma kc3_13:
    forall (g: E * B -> C) (f: E * A -> G1 B),
      kc3 (G2 := fun A => A) g f = map g ∘ σ ∘ cobind f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> G1 B),
g ⋆3 f = map g ∘ σ ∘ cobind f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> G1 B),
g ⋆3 f = map g ∘ σ ∘ cobind f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> G1 B
g ⋆3 f = map g ∘ σ ∘ cobind f
    unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> G1 B
map g ∘ σ ∘ cobind f = map g ∘ σ ∘ cobind f
    reflexivity.
  Qed.

  Lemma kc3_23:
    forall (g: B -> G2 C) (f: E * A -> G1 B),
      (g ∘ extract) ⋆3 f = map g ∘ f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : E * A -> G1 B),
g ∘ extract ⋆3 f = map g ∘ f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : E * A -> G1 B),
g ∘ extract ⋆3 f = map g ∘ f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
g ∘ extract ⋆3 f = map g ∘ f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
map (g ∘ extract) ∘ σ ∘ cobind f = map g ∘ f
    ext [w a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
w: E
a: A
(map (g ∘ extract) ∘ σ ∘ cobind f) (w, a) =
(map g ∘ f) (w, a)
    unfold compose; cbn.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
w: E
a: A
map (g ○ extract) (map (pair w) (f (w, a))) =
map g (f (w, a))
    compose near (f (w, a)) on left.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
w: E
a: A
(map (g ○ extract) ∘ map (pair w)) (f (w, a)) =
map g (f (w, a))
    now rewrite fun_map_map.
  Qed.

  Lemma kc3_03:
    forall (g: B -> C) (f: E * A -> G1 B),
      kc3 (G2 := fun A => A) (g ∘ extract) f = map g ∘ f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> G1 B),
g ∘ extract ⋆3 f = map g ∘ f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> G1 B),
g ∘ extract ⋆3 f = map g ∘ f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
g ∘ extract ⋆3 f = map g ∘ f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
map (g ∘ extract) ∘ σ ∘ cobind f = map g ∘ f
    ext [w a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
w: E
a: A
(map (g ∘ extract) ∘ σ ∘ cobind f) (w, a) =
(map g ∘ f) (w, a)
    unfold compose; cbn.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
w: E
a: A
map (g ○ extract) (map (pair w) (f (w, a))) =
map g (f (w, a))
    compose near (f (w, a)) on left.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
w: E
a: A
(map (g ○ extract) ∘ map (pair w)) (f (w, a)) =
map g (f (w, a))
    now rewrite fun_map_map.
  Qed.

  (** **** [xy] *)
  (********************************************************************)
  Lemma kc3_21:
    forall (g: B -> G2 C)
           (f: E * A -> B),
      kc3 (G1 := fun A => A) (g ∘ extract) f = g ∘ f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : E * A -> B),
g ∘ extract ⋆3 f = g ∘ f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : E * A -> B),
g ∘ extract ⋆3 f = g ∘ f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> B
g ∘ extract ⋆3 f = g ∘ f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> B
map (g ∘ extract) ∘ σ ∘ cobind f = g ∘ f
    unfold strength.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> B
map (g ∘ extract) ∘ (fun '(a, t) => map (pair a) t)
∘ cobind f = g ∘ f
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> B
e: E
a: A
(map (g ∘ extract) ∘ (fun '(a, t) => map (pair a) t)
 ∘ cobind f) (e, a) = (g ∘ f) (e, a)
    reflexivity.
  Qed.

  Lemma kc3_12:
    forall (g: E * B -> C) (f: A -> G1 B),
      kc3 (G2 := fun A => A) g (f ∘ extract) =
        fun '(e, a) => map (g ∘ pair e) (f a).
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : A -> G1 B),
g ⋆3 f ∘ extract =
(fun '(e, a) => map (g ∘ pair e) (f a))
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : A -> G1 B),
g ⋆3 f ∘ extract =
(fun '(e, a) => map (g ∘ pair e) (f a))
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> G1 B
g ⋆3 f ∘ extract =
(fun '(e, a) => map (g ∘ pair e) (f a)) unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> G1 B
map g ∘ σ ∘ cobind (f ∘ extract) =
(fun '(e, a) => map (g ∘ pair e) (f a))
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> G1 B
e: E
a: A
(map g ∘ σ ∘ cobind (f ∘ extract)) (e, a) =
map (g ∘ pair e) (f a)
    unfold compose; cbn.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> G1 B
e: E
a: A
map g (map (pair e) (f a)) = map (g ○ pair e) (f a)
    compose near (f a) on left.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> G1 B
e: E
a: A
(map g ∘ map (pair e)) (f a) = map (g ○ pair e) (f a)
    rewrite fun_map_map.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> G1 B
e: E
a: A
map (g ∘ pair e) (f a) = map (g ○ pair e) (f a)
    reflexivity.
  Qed.

  Lemma kc3_01:
    forall (g: B -> C)
           (f: E * A -> B),
      kc3 (G1 := fun A => A) (G2 := fun A => A) (g ∘ extract) f = g ∘ f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> B),
g ∘ extract ⋆3 f = g ∘ f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> B),
g ∘ extract ⋆3 f = g ∘ f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
g ∘ extract ⋆3 f = g ∘ f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
map (g ∘ extract) ∘ σ ∘ cobind f = g ∘ f
    unfold strength; unfold_ops @Map_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
g ∘ extract ∘ (fun '(a, t) => (a, t)) ∘ cobind f =
g ∘ f
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
e: E
a: A
(g ∘ extract ∘ (fun '(a, t) => (a, t)) ∘ cobind f)
  (e, a) = (g ∘ f) (e, a)
    reflexivity.
  Qed.

  Lemma kc3_10:
    forall (g: E * B -> C) (f: A -> B),
      kc3 (G1 := fun A => A) (G2 := fun A => A) g (f ∘ extract) =
        g ∘ map f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : A -> B),
g ⋆3 f ∘ extract = g ∘ map f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : A -> B),
g ⋆3 f ∘ extract = g ∘ map f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
g ⋆3 f ∘ extract = g ∘ map f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
map g ∘ σ ∘ cobind (f ∘ extract) = g ∘ map f
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
e: E
a: A
(map g ∘ σ ∘ cobind (f ∘ extract)) (e, a) =
(g ∘ map f) (e, a)
    reflexivity.
  Qed.

  Lemma kc3_20:
    forall (g: B -> G2 C) (f: A -> B),
      kc3 (E := E) (G1 := fun A => A) (g ∘ extract) (f ∘ extract) =
        g ∘ f ∘ extract.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> B),
g ∘ extract ⋆3 f ∘ extract = g ∘ f ∘ extract
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> B),
g ∘ extract ⋆3 f ∘ extract = g ∘ f ∘ extract
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> B
g ∘ extract ⋆3 f ∘ extract = g ∘ f ∘ extract unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> B
map (g ∘ extract) ∘ σ ∘ cobind (f ∘ extract) =
g ∘ f ∘ extract
    unfold strength; unfold_ops @Map_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> B
g ∘ extract ∘ (fun '(a, t) => (a, t))
∘ cobind (f ∘ extract) = g ∘ f ∘ extract
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> B
e: E
a: A
(g ∘ extract ∘ (fun '(a, t) => (a, t))
 ∘ cobind (f ∘ extract)) (e, a) =
(g ∘ f ∘ extract) (e, a)
    reflexivity.
  Qed.

  Lemma kc3_02:
    forall (g: B -> C) (f: E * A -> B),
      kc3 (E := E) (G1 := fun A => A) (G2 := fun A => A)
        (g ∘ extract) f = g ∘ f.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> B),
g ∘ extract ⋆3 f = g ∘ f
  Proof.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> B),
g ∘ extract ⋆3 f = g ∘ f
    intros.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
g ∘ extract ⋆3 f = g ∘ f unfold kc3.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
map (g ∘ extract) ∘ σ ∘ cobind f = g ∘ f
    unfold strength; unfold_ops @Map_I.
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
g ∘ extract ∘ (fun '(a, t) => (a, t)) ∘ cobind f =
g ∘ f
    ext [e a].
E: Type
T: Type -> Type
Map_inst: Map T
Mapd_inst: Mapd E T
Traverse_inst: Traverse T
Mapdt_inst: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
e: E
a: A
(g ∘ extract ∘ (fun '(a, t) => (a, t)) ∘ cobind f)
  (e, a) = (g ∘ f) (e, a)
    reflexivity.
  Qed.

End decorated_traversable_functor_derived_kleisli_laws.

(** ** Derived Composition Laws *)
(**********************************************************************)
Section composition.

  Context
    {E: Type} {T: Type -> Type}
    `{Mapdt_ET: Mapdt E T}
    `{Mapd_ET: Mapd E T}
    `{Traverse_T: Traverse T}
    `{Map_T: Map T}
    `{! Compat_Map_Mapdt E T}
    `{! Compat_Mapd_Mapdt E T}
    `{! Compat_Traverse_Mapdt E T}
    `{! DecoratedTraversableFunctor E T}.

  Context
    `{Applicative G1}
    `{Applicative G2}
    {A B C: Type}.

  (** *** <<mapdt>> on the right *)
  (********************************************************************)
  Corollary traverse_mapdt: forall (g: B -> G2 C) (f: E * A -> G1 B),
      map (traverse g) ∘ mapdt f = mapdt (G := G1 ∘ G2) (map g ∘ f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : E * A -> G1 B),
map (traverse g) ∘ mapdt f = mapdt (map g ∘ f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : E * A -> G1 B),
map (traverse g) ∘ mapdt f = mapdt (map g ∘ f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
map (traverse g) ∘ mapdt f = mapdt (map g ∘ f)
    rewrite traverse_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
map (mapdt (g ∘ extract)) ∘ mapdt f =
mapdt (map g ∘ f)
    rewrite kdtf_mapdt2.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
mapdt (g ∘ extract ⋆3 f) = mapdt (map g ∘ f)
    rewrite kc3_23.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: E * A -> G1 B
mapdt (map g ∘ f) = mapdt (map g ∘ f)
    reflexivity.
  Qed.

  Corollary mapd_mapdt: forall (g: E * B -> C) (f: E * A -> G1 B),
      map (mapd g) ∘ mapdt f = mapdt (map g ∘ σ ∘ cobind f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> G1 B),
map (mapd g) ∘ mapdt f = mapdt (map g ∘ σ ∘ cobind f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> G1 B),
map (mapd g) ∘ mapdt f = mapdt (map g ∘ σ ∘ cobind f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> G1 B
map (mapd g) ∘ mapdt f = mapdt (map g ∘ σ ∘ cobind f)
    rewrite mapd_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> G1 B
map (mapdt g) ∘ mapdt f = mapdt (map g ∘ σ ∘ cobind f)
    rewrite (kdtf_mapdt2 (G2 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> G1 B
mapdt (g ⋆3 f) = mapdt (map g ∘ σ ∘ cobind f)
    rewrite mapdt_app_id_r.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> G1 B
mapdt (g ⋆3 f) = mapdt (map g ∘ σ ∘ cobind f)
    reflexivity.
  Qed.

  Corollary map_mapdt: forall (g: B -> C) (f: E * A -> G1 B),
      map (map g) ∘ mapdt f = mapdt (map g ∘ f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> G1 B),
map (map g) ∘ mapdt f = mapdt (map g ∘ f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> G1 B),
map (map g) ∘ mapdt f = mapdt (map g ∘ f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
map (map g) ∘ mapdt f = mapdt (map g ∘ f)
    rewrite (map_to_mapdt (T := T)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
map (mapdt (g ∘ extract)) ∘ mapdt f =
mapdt (map g ∘ f)
    rewrite (kdtf_mapdt2 (G2 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
mapdt (g ∘ extract ⋆3 f) = mapdt (map g ∘ f)
    rewrite mapdt_app_id_r.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
mapdt (g ∘ extract ⋆3 f) = mapdt (map g ∘ f)
    rewrite kc3_03.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> G1 B
mapdt (map g ∘ f) = mapdt (map g ∘ f)
    reflexivity.
  Qed.

  (** *** <<mapdt>> on the left *)
  (********************************************************************)
  Corollary mapdt_traverse: forall (g: E * B -> G2 C) (f: A -> G1 B),
      map (mapdt g) ∘ traverse (T := T) f =
        mapdt (E := E) (G := G1 ∘ G2)
          (map g ∘ σ ∘ map (F := prod E) f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> G1 B),
map (mapdt g) ∘ traverse f = mapdt (map g ∘ σ ∘ map f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> G1 B),
map (mapdt g) ∘ traverse f = mapdt (map g ∘ σ ∘ map f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
map (mapdt g) ∘ traverse f = mapdt (map g ∘ σ ∘ map f)
    rewrite traverse_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
map (mapdt g) ∘ mapdt (f ∘ extract) =
mapdt (map g ∘ σ ∘ map f)
    rewrite kdtf_mapdt2.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
mapdt (g ⋆3 f ∘ extract) = mapdt (map g ∘ σ ∘ map f)
    rewrite kc3_32.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> G1 B
mapdt (map g ∘ σ ∘ map f) = mapdt (map g ∘ σ ∘ map f)
    reflexivity.
  Qed.

  Lemma mapdt_mapd: forall (g: E * B -> G2 C) (f: E * A -> B),
      mapdt g ∘ mapd f = mapdt (g ⋆1 f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : E * A -> B),
mapdt g ∘ mapd f = mapdt (g ⋆1 f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : E * A -> B),
mapdt g ∘ mapd f = mapdt (g ⋆1 f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
mapdt g ∘ mapd f = mapdt (g ⋆1 f)
    rewrite mapd_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
mapdt g ∘ mapdt f = mapdt (g ⋆1 f)
    change (mapdt g)
      with (map (F := fun A => A) (mapdt g)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
map (mapdt g) ∘ mapdt f = mapdt (g ⋆1 f)
    rewrite (kdtf_mapdt2 (G1 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
mapdt (g ⋆3 f) = mapdt (g ⋆1 f)
    rewrite mapdt_app_id_l.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
mapdt (g ⋆3 f) = mapdt (g ⋆1 f)
    rewrite kc3_31.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: E * A -> B
mapdt (g ⋆1 f) = mapdt (g ⋆1 f)
    reflexivity.
  Qed.

  Lemma mapdt_map: forall (g: E * B -> G2 C) (f: A -> B),
      mapdt g ∘ map f = mapdt (g ∘ map f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> B),
mapdt g ∘ map f = mapdt (g ∘ map f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> G2 C) (f : A -> B),
mapdt g ∘ map f = mapdt (g ∘ map f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
mapdt g ∘ map f = mapdt (g ∘ map f)
    rewrite map_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
mapdt g ∘ mapdt (f ∘ extract) = mapdt (g ∘ map f)
    change (mapdt g)
      with (map (F := fun A => A) (mapdt g)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
map (mapdt g) ∘ mapdt (f ∘ extract) =
mapdt (g ∘ map f)
    rewrite (kdtf_mapdt2 (G1 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
mapdt (g ⋆3 f ∘ extract) = mapdt (g ∘ map f)
    rewrite mapdt_app_id_l.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
mapdt (g ⋆3 f ∘ extract) = mapdt (g ∘ map f)
    rewrite kc3_30.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> G2 C
f: A -> B
mapdt (g ∘ map f) = mapdt (g ∘ map f)
    reflexivity.
  Qed.

  (** *** Other cases *)
  (********************************************************************)
  Corollary map_mapd: forall (g: B -> C) (f: E * A -> B),
      map g ∘ mapd f = mapd (g ∘ f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> B),
map g ∘ mapd f = mapd (g ∘ f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> C) (f : E * A -> B),
map g ∘ mapd f = mapd (g ∘ f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
map g ∘ mapd f = mapd (g ∘ f)
    rewrite map_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
mapdt (g ∘ extract) ∘ mapd f = mapd (g ∘ f)
    do 2 rewrite mapd_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
mapdt (g ∘ extract) ∘ mapdt f = mapdt (g ∘ f)
    change (mapdt ?g)
      with (map (F := fun A => A) (mapdt (G := fun A => A) g)) at 1.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
map (mapdt (g ∘ extract)) ∘ mapdt f = mapdt (g ∘ f)
    rewrite (kdtf_mapdt2 (G1 := fun A => A) (G2 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
mapdt (g ∘ extract ⋆3 f) = mapdt (g ∘ f)
    rewrite mapdt_app_id_l.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
mapdt (g ∘ extract ⋆3 f) = mapdt (g ∘ f)
    rewrite kc3_01.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> C
f: E * A -> B
mapdt (g ∘ f) = mapdt (g ∘ f)
    reflexivity.
  Qed.

  Corollary mapd_map: forall (g: E * B -> C) (f: A -> B),
      mapd g ∘ map f = mapd (g ∘ map f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : A -> B),
mapd g ∘ map f = mapd (g ∘ map f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : A -> B),
mapd g ∘ map f = mapd (g ∘ map f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
mapd g ∘ map f = mapd (g ∘ map f)
    do 2 rewrite mapd_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
mapdt g ∘ map f = mapdt (g ∘ map f)
    rewrite map_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
mapdt g ∘ mapdt (f ∘ extract) = mapdt (g ∘ map f)
    change (mapdt ?g)
      with (map (F := fun A => A) (mapdt (G := fun A => A) g)) at 1.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
map (mapdt g) ∘ mapdt (f ∘ extract) =
mapdt (g ∘ map f)
    rewrite (kdtf_mapdt2 (G1 := fun A => A) (G2 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
mapdt (g ⋆3 f ∘ extract) = mapdt (g ∘ map f)
    rewrite mapdt_app_id_l.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
mapdt (g ⋆3 f ∘ extract) = mapdt (g ∘ map f)
    rewrite kc3_11.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: A -> B
mapdt (g ⋆1 f ∘ extract) = mapdt (g ∘ map f)
    reflexivity.
  Qed.

  Corollary mapd_mapd: forall (g: E * B -> C) (f: E * A -> B),
      mapd g ∘ mapd f = mapd (g ⋆1 f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> B),
mapd g ∘ mapd f = mapd (g ⋆1 f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : E * B -> C) (f : E * A -> B),
mapd g ∘ mapd f = mapd (g ⋆1 f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapd g ∘ mapd f = mapd (g ⋆1 f)
    do 2 rewrite mapd_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapdt g ∘ mapdt f = mapd (g ⋆1 f)
    change (mapdt ?g)
      with (map (F := fun A => A) (mapdt (G := fun A => A) g)) at 1.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
map (mapdt g) ∘ mapdt f = mapd (g ⋆1 f)
    rewrite (kdtf_mapdt2 (G1 := fun A => A) (G2 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapdt (g ⋆3 f) = mapd (g ⋆1 f)
    rewrite mapdt_app_id_l.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapdt (g ⋆3 f) = mapd (g ⋆1 f)
    rewrite kc3_11.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapdt (g ⋆1 f) = mapd (g ⋆1 f)
    rewrite mapd_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapdt (g ⋆1 f) = mapdt (g ⋆1 f)
    reflexivity.
  Qed.

  Corollary traverse_traverse: forall (g: B -> G2 C) (f: A -> G1 B),
      map (F := G1) (traverse g) ∘ traverse f =
        traverse (G := G1 ∘ G2) (g ⋆2 f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (g ⋆2 f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (g ⋆2 f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (g ⋆2 f)
    do 3 rewrite traverse_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (mapdt (g ∘ extract)) ∘ mapdt (f ∘ extract) =
mapdt ((g ⋆2 f) ∘ extract)
    rewrite kdtf_mapdt2.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
mapdt (g ∘ extract ⋆3 f ∘ extract) =
mapdt ((g ⋆2 f) ∘ extract)
    rewrite kc3_22.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
mapdt (map g ∘ f ∘ extract) =
mapdt ((g ⋆2 f) ∘ extract)
    reflexivity.
  Qed.

  Lemma map_map: forall {A B C: Type} (f: A -> B) (g: B -> C),
      map g ∘ map f = map (F := T) (g ∘ f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0, C0: Type
f: A0 -> B0
g: B0 -> C0
map g ∘ map f = map (g ∘ f)
    do 3 rewrite map_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0, C0: Type
f: A0 -> B0
g: B0 -> C0
mapdt (g ∘ extract) ∘ mapdt (f ∘ extract) =
mapdt (g ∘ f ∘ extract)
    change_left
      (map (F := fun A => A)
         (mapdt (T := T) (g ∘ extract)) ∘ mapdt (T := T) (f ∘ extract)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0, C0: Type
f: A0 -> B0
g: B0 -> C0
map (mapdt (g ∘ extract)) ∘ mapdt (f ∘ extract) =
mapdt (g ∘ f ∘ extract)
    rewrite (kdtf_mapdt2 (G1 := fun A => A) (G2 := fun A => A)).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0, C0: Type
f: A0 -> B0
g: B0 -> C0
mapdt (g ∘ extract ⋆3 f ∘ extract) =
mapdt (g ∘ f ∘ extract)
    rewrite mapdt_app_id_l.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0, C0: Type
f: A0 -> B0
g: B0 -> C0
mapdt (g ∘ extract ⋆3 f ∘ extract) =
mapdt (g ∘ f ∘ extract)
    rewrite kc3_00.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0, B0, C0: Type
f: A0 -> B0
g: B0 -> C0
mapdt (g ∘ f ∘ extract) = mapdt (g ∘ f ∘ extract)
    reflexivity.
  Qed.

  (** *** Identity laws *)
  (********************************************************************)
  Lemma traverse_id: forall A: Type,
      traverse (G := fun A => A) id = @id (T A).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, traverse id = id
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, traverse id = id
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
traverse id = id
    rewrite traverse_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
mapdt (id ∘ extract) = id
    change (id ∘ ?f) with f.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
mapdt extract = id
    now rewrite kdtf_mapdt1.
  Qed.

  Lemma mapd_id: forall A: Type,
      mapd extract = @id (T A).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, mapd extract = id
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, mapd extract = id
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
mapd extract = id
    rewrite mapd_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
mapdt extract = id
    rewrite kdtf_mapdt1.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
id = id
    reflexivity.
  Qed.

  Lemma map_id: forall A: Type,
      map (@id A) = @id (T A).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, map id = id
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall A : Type, map id = id
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
map id = id
    rewrite map_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
mapdt (id ∘ extract) = id
    change (id ∘ ?f) with f.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
mapdt extract = id
    rewrite kdtf_mapdt1.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C, A0: Type
id = id
    reflexivity.
  Qed.

  (** *** Naturality in applicative morphisms *)
  (********************************************************************)
  Lemma traverse_morphism:
    forall `{ApplicativeMorphism G1 G2 ϕ},
    forall (A B: Type) (f: A -> G1 B),
      ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f).
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (H1 : Map G1) (H2 : Mult G1) (H3 : Pure G1)
  (H4 : Map G2) (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
  Proof.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
forall (H1 : Map G1) (H2 : Mult G1) (H3 : Pure G1)
  (H4 : Map G2) (H5 : Mult G2) (H6 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 B),
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
    intros.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H7: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
ϕ (T B0) ∘ traverse f = traverse (ϕ B0 ∘ f)
    infer_applicative_instances.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H7: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
ϕ (T B0) ∘ traverse f = traverse (ϕ B0 ∘ f)
    rewrite traverse_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H7: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
ϕ (T B0) ∘ mapdt (f ∘ extract) = traverse (ϕ B0 ∘ f)
    rewrite traverse_to_mapdt.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H7: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
ϕ (T B0) ∘ mapdt (f ∘ extract) =
mapdt (ϕ B0 ∘ f ∘ extract)
    rewrite kdtf_morph.
E: Type
T: Type -> Type
Mapdt_ET: Mapdt E T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Map_T: Map T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
H1: Map G1
H2: Mult G1
H3: Pure G1
H4: Map G2
H5: Mult G2
H6: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H7: ApplicativeMorphism G1 G2 ϕ
A0, B0: Type
f: A0 -> G1 B0
app1: Applicative G1
app2: Applicative G2
mapdt (ϕ B0 ∘ (f ∘ extract)) =
mapdt (ϕ B0 ∘ f ∘ extract)
    reflexivity.
  Qed.

End composition.

(** ** Derived Typeclass Instances *)
(**********************************************************************)
Module DerivedInstances.
  Section instances.

    Context
      {E: Type} {T: Type -> Type}
      `{Map_T: Map T}
      `{Mapd_ET: Mapd E T}
      `{Traverse_T: Traverse T}
      `{Mapdt_ET: Mapdt E T}
      `{! Compat_Map_Mapdt E T}
      `{! Compat_Mapd_Mapdt E T}
      `{! Compat_Traverse_Mapdt E T}
      `{! DecoratedTraversableFunctor E T}.

    #[export] Instance DecoratedFunctor_DecoratedTraversableFunctor:
      DecoratedFunctor E T.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
DecoratedFunctor E T
    Proof.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
DecoratedFunctor E T
      constructor; intros.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
A: Type
mapd extract = id
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapd g ∘ mapd f = mapd (g ⋆1 f)
      -
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
A: Type
mapd extract = id apply mapd_id.
      -
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
A, B, C: Type
g: E * B -> C
f: E * A -> B
mapd g ∘ mapd f = mapd (g ⋆1 f) apply mapd_mapd.
    Qed.

    #[export] Instance TraversableFunctor_DecoratedTraversableFunctor:
      TraversableFunctor T.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
TraversableFunctor T
    Proof.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
TraversableFunctor T
      constructor; intros.
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
A: Type
traverse id = id
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (g ⋆2 f)
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
      -
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
A: Type
traverse id = id apply traverse_id.
      -
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (g ⋆2 f) apply traverse_traverse.
      -
E: Type
T: Type -> Type
Map_T: Map T
Mapd_ET: Mapd E T
Traverse_T: Traverse T
Mapdt_ET: Mapdt E T
Compat_Map_Mapdt0: Compat_Map_Mapdt E T
Compat_Mapd_Mapdt0: Compat_Mapd_Mapdt E T
Compat_Traverse_Mapdt0: Compat_Traverse_Mapdt E T
DecoratedTraversableFunctor0: DecoratedTraversableFunctor
  E T
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morphism: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f) apply traverse_morphism.
    Qed.

    #[export] Instance Functor_DecoratedTraversableFunctor:
      Functor T :=
      TraversableFunctor.DerivedInstances.Functor_TraversableFunctor.

  End instances.
End DerivedInstances.

(** * Notations *)
(**********************************************************************)
Module Notations.
  Infix "⋆3" := kc3 (at level 60): tealeaves_scope.
End Notations.