From Tealeaves Require Import
  Classes.Categorical.Monad
  Classes.Categorical.DecoratedMonad (shift)
  Classes.Kleisli.DecoratedTraversableFunctor
  Classes.Kleisli.DecoratedTraversableMonad
  Functors.Early.Subset
  Functors.Early.Ctxset
  Functors.Early.List.

Import DecoratedTraversableFunctor.Notations.
Import Functor.Notations.
Import List.ListNotations.
Import Product.Notations.
Import Subset.Notations.
Import Applicative.Notations.
Import Strength.Notations.
Import Monoid.Notations.

#[local] Generalizable Variables W M A B G ϕ.

Definition env (E: Type) (A: Type) := list (E * A).

(** * Decorated Traversable Functor Instance (Kleisli)] *)
(**********************************************************************)
Section env.

  Context
    (E: Type).

  (** ** Operation <<mapdt>> and Derived Operations *)
  (********************************************************************)
  Fixpoint mapdt_env (G: Type -> Type) `{Map G} `{Pure G} `{Mult G}
    `(f: E * A -> G B) (Γ: env E A): G (env E B) :=
    match Γ with
    | nil => pure (@nil (E * B))
    | (e, a) :: rest =>
        pure (@List.cons (E * B))
          <⋆> σ (e, f (e, a))
          <⋆> mapdt_env G f rest
    end.

  Fixpoint traverse_env (G: Type -> Type) `{Map G} `{Pure G} `{Mult G}
    `(f: A -> G B) (l: env E A): G (env E B) :=
    match l with
    | nil => pure (@nil (E * B))
    | (e, a) :: xs =>
        pure (@List.cons (E * B))
          <⋆> σ (e, f a)
          <⋆> traverse_env G f xs
    end.

  Fixpoint mapd_env `(f: E * A -> B) (Γ: env E A): env E B :=
    match Γ with
    | nil => @nil (E * B)
    | (e, a) :: rest =>
        (e, f (e, a)) :: mapd_env f rest
    end.

  Fixpoint map_env `(f: A -> B) (Γ: env E A): env E B :=
    match Γ with
    | nil => @nil (E * B)
    | (e, a) :: rest =>
        (e, f a) :: map_env f rest
    end.

  #[export] Instance Mapdt_env: Mapdt E (env E) := @mapdt_env.
  #[export] Instance Traverse_env: Traverse (env E) := @traverse_env.
  #[export] Instance Mapd_env: Mapd E (env E) := @mapd_env.
  #[export] Instance Map_env: Map (env E) := @map_env.

End env.

Ltac simple_env_tactic :=
  intros;
  let l := fresh "l" in
  let e := fresh "e" in
  let a := fresh "a" in
  let rest := fresh "rest" in
  let IHrest := fresh "IHrest" in
  ext l;
  ( induction l as [|[e a] rest IHrest] ||
  induction l as [|a rest IHrest] );
  [ reflexivity |
    try (cbn; now rewrite IHrest)].

(** ** Rewriting Laws for <<mapdt>> *)
(**********************************************************************)
Section mapdt_rewriting_lemmas.

  Context
    `{Applicative G}
    (E A B: Type).

  Lemma mapdt_env_nil: forall `(f: E * A -> G B),
      mapdt f (@nil (E * A)) = pure nil.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall f : E * A -> G B, mapdt f [] = pure []
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall f : E * A -> G B, mapdt f [] = pure []
    reflexivity.
  Qed.

  Lemma mapdt_env_one:
    forall (f: E * A -> G B) (e: E) (a: A),
      mapdt f (ret (T := list) (e, a)) =
        map (ret (T := list) ∘ pair e) (f (e, a)).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall (f : E * A -> G B) (e : E) (a : A),
mapdt f (ret (e, a)) = map (ret ∘ pair e) (f (e, a))
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall (f : E * A -> G B) (e : E) (a : A),
mapdt f (ret (e, a)) = map (ret ∘ pair e) (f (e, a))
    intros.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
mapdt f (ret (e, a)) = map (ret ∘ pair e) (f (e, a))
    cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure cons <⋆> map (pair e) (f (e, a)) <⋆> pure [] =
map (ret ∘ pair e) (f (e, a))
    rewrite map_to_ap.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure cons <⋆> (pure (pair e) <⋆> f (e, a)) <⋆> pure [] =
map (ret ∘ pair e) (f (e, a))
    rewrite <- ap4.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure compose <⋆> pure cons <⋆> pure (pair e) <⋆>
f (e, a) <⋆> pure [] = map (ret ∘ pair e) (f (e, a))
    rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure (compose cons) <⋆> pure (pair e) <⋆> f (e, a) <⋆>
pure [] = map (ret ∘ pair e) (f (e, a))
    rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure (cons ∘ pair e) <⋆> f (e, a) <⋆> pure [] =
map (ret ∘ pair e) (f (e, a))
    rewrite ap3.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure (evalAt []) <⋆>
(pure (cons ∘ pair e) <⋆> f (e, a)) =
map (ret ∘ pair e) (f (e, a))
    rewrite <- ap4.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure compose <⋆> pure (evalAt []) <⋆>
pure (cons ∘ pair e) <⋆> f (e, a) =
map (ret ∘ pair e) (f (e, a))
    rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure (compose (evalAt [])) <⋆> pure (cons ∘ pair e) <⋆>
f (e, a) = map (ret ∘ pair e) (f (e, a))
    rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
pure (evalAt [] ∘ (cons ∘ pair e)) <⋆> f (e, a) =
map (ret ∘ pair e) (f (e, a))
    rewrite <- map_to_ap.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
map (evalAt [] ∘ (cons ∘ pair e)) (f (e, a)) =
map (ret ∘ pair e) (f (e, a))
    reflexivity.
  Qed.

  Lemma mapdt_env_cons:
    forall (f: E * A -> G B) (e: E) (a: A) (l: env E A),
      mapdt f ((e, a) :: l) =
        pure cons <⋆> σ (e, f (e, a)) <⋆> mapdt f l.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall (f : E * A -> G B) (e : E) (a : A)
  (l : env E A),
mapdt f ((e, a) :: l) =
pure cons <⋆> σ (e, f (e, a)) <⋆> mapdt f l
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall (f : E * A -> G B) (e : E) (a : A)
  (l : env E A),
mapdt f ((e, a) :: l) =
pure cons <⋆> σ (e, f (e, a)) <⋆> mapdt f l
    reflexivity.
  Qed.

  Lemma mapdt_env_app:
    forall (f: E * A -> G B) (l1 l2: env E A),
      mapdt f (l1 ++ l2) =
        pure (@app (E * B)) <⋆> mapdt f l1 <⋆> mapdt f l2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall (f : E * A -> G B) (l1 l2 : env E A),
mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆> mapdt f l2
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
forall (f : E * A -> G B) (l1 l2 : env E A),
mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆> mapdt f l2
    intros.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
l1, l2: env E A
mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆> mapdt f l2
    induction l1.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
l2: env E A
mapdt f ([] ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f [] <⋆> mapdt f l2
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
a: E * A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
mapdt f ((a :: l1) ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f (a :: l1) <⋆>
mapdt f l2
    -
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
l2: env E A
mapdt f ([] ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f [] <⋆> mapdt f l2 cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
l2: env E A
mapdt f l2 =
pure (app (A:=E * B)) <⋆> pure [] <⋆> mapdt f l2
      rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
l2: env E A
mapdt f l2 = pure (app []) <⋆> mapdt f l2
      rewrite ap1.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
l2: env E A
mapdt f l2 = mapdt f l2
      reflexivity.
    -
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
a: E * A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
mapdt f ((a :: l1) ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f (a :: l1) <⋆>
mapdt f l2 destruct a  as (e, a).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
mapdt f (((e, a) :: l1) ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f ((e, a) :: l1) <⋆>
mapdt f l2
      cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
pure cons <⋆> map (pair e) (f (e, a)) <⋆>
mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆>
(pure cons <⋆> map (pair e) (f (e, a)) <⋆> mapdt f l1) <⋆>
mapdt f l2
      rewrite IHl1.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
pure cons <⋆> map (pair e) (f (e, a)) <⋆>
(pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆> mapdt f l2) =
pure (app (A:=E * B)) <⋆>
(pure cons <⋆> map (pair e) (f (e, a)) <⋆> mapdt f l1) <⋆>
mapdt f l2
      repeat rewrite <- ap4.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure cons <⋆> map (pair e) (f (e, a)) <⋆>
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆> mapdt f l2 =
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure (app (A:=E * B)) <⋆> pure cons <⋆>
map (pair e) (f (e, a)) <⋆> mapdt f l1 <⋆> mapdt f l2
      repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
pure
  ((compose ∘ compose) compose compose compose compose
     cons) <⋆> map (pair e) (f (e, a)) <⋆>
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆> mapdt f l2 =
pure ((compose ∘ compose) (app (A:=E * B)) cons) <⋆>
map (pair e) (f (e, a)) <⋆> mapdt f l1 <⋆> mapdt f l2
      rewrite ap3.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
pure (evalAt (app (A:=E * B))) <⋆>
(pure
   ((compose ∘ compose) compose compose compose
      compose cons) <⋆> map (pair e) (f (e, a))) <⋆>
mapdt f l1 <⋆> mapdt f l2 =
pure ((compose ∘ compose) (app (A:=E * B)) cons) <⋆>
map (pair e) (f (e, a)) <⋆> mapdt f l1 <⋆> mapdt f l2
      repeat rewrite <- ap4.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
pure compose <⋆> pure (evalAt (app (A:=E * B))) <⋆>
pure
  ((compose ∘ compose) compose compose compose compose
     cons) <⋆> map (pair e) (f (e, a)) <⋆> mapdt f l1 <⋆>
mapdt f l2 =
pure ((compose ∘ compose) (app (A:=E * B)) cons) <⋆>
map (pair e) (f (e, a)) <⋆> mapdt f l1 <⋆> mapdt f l2
      repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
E, A, B: Type
f: E * A -> G B
e: E
a: A
l1: list (E * A)
l2: env E A
IHl1: mapdt f (l1 ++ l2) =
pure (app (A:=E * B)) <⋆> mapdt f l1 <⋆>
mapdt f l2
pure
  (evalAt (app (A:=E * B))
   ∘ (compose ∘ compose) compose compose compose
       compose cons) <⋆> map (pair e) (f (e, a)) <⋆>
mapdt f l1 <⋆> mapdt f l2 =
pure ((compose ∘ compose) (app (A:=E * B)) cons) <⋆>
map (pair e) (f (e, a)) <⋆> mapdt f l1 <⋆> mapdt f l2
      reflexivity.
  Qed.

End mapdt_rewriting_lemmas.

#[export] Hint Rewrite
  mapdt_env_nil @mapdt_env_cons mapdt_env_one mapdt_env_app:
  tea_env.

(** ** Compatibility Typeclass Instances *)
(**********************************************************************)
Lemma env_traverse_compat:
  forall (E: Type) `{Applicative G} (A B: Type) (f: A -> G B),
    traverse f = mapdt (E := E) (f ∘ extract).
forall (E : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> G B),
traverse f = mapdt (f ∘ extract)
Proof.
forall (E : Type) (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> G B),
traverse f = mapdt (f ∘ extract)
  simple_env_tactic.
Qed.

Lemma env_mapd_compat: forall (E A B: Type) (f: E * A -> B),
    mapd (T := env E) f = mapdt (E := E) f.
forall (E A B : Type) (f : E * A -> B),
mapd f = mapdt f
Proof.
forall (E A B : Type) (f : E * A -> B),
mapd f = mapdt f
  simple_env_tactic.
Qed.

Lemma env_map_compat: forall (E A B: Type) (f: A -> B),
    map (F := env E) f = mapdt (E := E) (f ∘ extract (W := (E ×))).
forall (E A B : Type) (f : A -> B),
map f = mapdt (f ∘ extract)
Proof.
forall (E A B : Type) (f : A -> B),
map f = mapdt (f ∘ extract)
  simple_env_tactic.
Qed.

#[export] Instance Compat_Traverse_Mapdt_env {E: Type}:
  Compat_Traverse_Mapdt E (env E).
E: Type
Compat_Traverse_Mapdt E (env E)
Proof.
E: Type
Compat_Traverse_Mapdt E (env E)
  hnf.
E: Type
Traverse_env E = DerivedOperations.Traverse_Mapdt intros.
E: Type
Traverse_env E = DerivedOperations.Traverse_Mapdt
  ext G MapG PureG MultG.
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
Traverse_env E G MapG PureG MultG =
DerivedOperations.Traverse_Mapdt G MapG PureG MultG
  ext A B f l.
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
l: env E A
Traverse_env E G MapG PureG MultG A B f l =
DerivedOperations.Traverse_Mapdt G MapG PureG MultG A
  B f l
  unfold Traverse_env.
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
l: env E A
traverse_env E G f l =
DerivedOperations.Traverse_Mapdt G MapG PureG MultG A
  B f l
  change_left (traverse f l).
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
l: env E A
traverse f l =
DerivedOperations.Traverse_Mapdt G MapG PureG MultG A
  B f l
  change_right (mapdt (T := env E) (f ∘ extract (W := (E ×))) l).
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
l: env E A
traverse f l = mapdt (f ∘ extract) l
  induction l.
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
traverse f [] = mapdt (f ∘ extract) []
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: E * A
l: list (E * A)
IHl: traverse f l = mapdt (f ∘ extract) l
traverse f (a :: l) = mapdt (f ∘ extract) (a :: l)
  -
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
traverse f [] = mapdt (f ∘ extract) [] reflexivity.
  -
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: E * A
l: list (E * A)
IHl: traverse f l = mapdt (f ∘ extract) l
traverse f (a :: l) = mapdt (f ∘ extract) (a :: l) cbn.
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
a: E * A
l: list (E * A)
IHl: traverse f l = mapdt (f ∘ extract) l
(let (e, a) := a in
 pure cons <⋆> map (pair e) (f a) <⋆> traverse f l) =
(let (e, a) := a in
 pure cons <⋆> map (pair e) ((f ∘ extract) (e, a)) <⋆>
 mapdt (f ∘ extract) l)
    destruct a as [e a].
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
e: E
a: A
l: list (E * A)
IHl: traverse f l = mapdt (f ∘ extract) l
pure cons <⋆> map (pair e) (f a) <⋆> traverse f l =
pure cons <⋆> map (pair e) ((f ∘ extract) (e, a)) <⋆>
mapdt (f ∘ extract) l
    rewrite IHl.
E: Type
G: Type -> Type
MapG: Map G
PureG: Pure G
MultG: Mult G
A, B: Type
f: A -> G B
e: E
a: A
l: list (E * A)
IHl: traverse f l = mapdt (f ∘ extract) l
pure cons <⋆> map (pair e) (f a) <⋆>
mapdt (f ∘ extract) l =
pure cons <⋆> map (pair e) ((f ∘ extract) (e, a)) <⋆>
mapdt (f ∘ extract) l
    reflexivity.
Qed.

#[export] Instance Compat_Map_Mapdt_env {E: Type}:
  Compat_Map_Mapdt E (env E).
E: Type
Compat_Map_Mapdt E (env E)
Proof.
E: Type
Compat_Map_Mapdt E (env E)
  hnf.
E: Type
Map_env E = DerivedOperations.Map_Mapdt ext A B f l.
E, A, B: Type
f: A -> B
l: env E A
Map_env E A B f l =
DerivedOperations.Map_Mapdt A B f l
  change_left (map f l).
E, A, B: Type
f: A -> B
l: env E A
map f l = DerivedOperations.Map_Mapdt A B f l
  rewrite env_map_compat.
E, A, B: Type
f: A -> B
l: env E A
mapdt (f ∘ extract) l =
DerivedOperations.Map_Mapdt A B f l
  reflexivity.
Qed.

#[export] Instance Compat_Mapd_Mapdt_env {E: Type}:
  Compat_Mapd_Mapdt E (env E).
E: Type
Compat_Mapd_Mapdt E (env E)
Proof.
E: Type
Compat_Mapd_Mapdt E (env E)
  hnf.
E: Type
Mapd_env E = DerivedOperations.Mapd_Mapdt ext A B f l.
E, A, B: Type
f: E * A -> B
l: env E A
Mapd_env E A B f l =
DerivedOperations.Mapd_Mapdt A B f l
  change_left (mapd f l).
E, A, B: Type
f: E * A -> B
l: env E A
mapd f l = DerivedOperations.Mapd_Mapdt A B f l
  rewrite env_mapd_compat.
E, A, B: Type
f: E * A -> B
l: env E A
mapdt f l = DerivedOperations.Mapd_Mapdt A B f l
  reflexivity.
Qed.

(** ** Decorated Traversable Functor Laws *)
(**********************************************************************)
Section env_laws.

  Context
    (E: Type).

  Lemma env_mapdt1:
    forall (A: Type),
      mapdt (extract (W := (E ×))) = @id (env E A).
E: Type
forall A : Type, mapdt extract = id
  Proof.
E: Type
forall A : Type, mapdt extract = id
    intros.
E, A: Type
mapdt extract = id ext l.
E, A: Type
l: env E A
mapdt extract l = id l induction l.
E, A: Type
mapdt extract [] = id []
E, A: Type
a: E * A
l: list (E * A)
IHl: mapdt extract l = id l
mapdt extract (a :: l) = id (a :: l)
    -
E, A: Type
mapdt extract [] = id [] reflexivity.
    -
E, A: Type
a: E * A
l: list (E * A)
IHl: mapdt extract l = id l
mapdt extract (a :: l) = id (a :: l) destruct a.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: mapdt extract l = id l
mapdt extract ((e, a) :: l) = id ((e, a) :: l)
      autorewrite with tea_env.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: mapdt extract l = id l
pure cons <⋆> σ (e, extract (e, a)) <⋆>
mapdt extract l = id ((e, a) :: l)
      rewrite IHl.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: mapdt extract l = id l
pure cons <⋆> σ (e, extract (e, a)) <⋆> id l =
id ((e, a) :: l)
      reflexivity.
  Qed.

  Lemma env_mapdt2
    `{Applicative G1}
    `{Applicative G2}:
    forall (A B C: Type)
      (g: E * B -> G2 C)
      (f: E * A -> G1 B),
      map (mapdt g) ∘ mapdt f =
        mapdt (G := G1 ∘ G2) (g ⋆3 f).
E: Type
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
forall (A B C : Type) (g : E * B -> G2 C)
  (f : E * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
  Proof.
E: Type
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
forall (A B C : Type) (g : E * B -> G2 C)
  (f : E * A -> G1 B),
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f)
    intros.
E: Type
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 -> G1 B
map (mapdt g) ∘ mapdt f = mapdt (g ⋆3 f) ext l.
E: Type
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 -> G1 B
l: env E A
(map (mapdt g) ∘ mapdt f) l = mapdt (g ⋆3 f) l induction l.
E: Type
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 -> G1 B
(map (mapdt g) ∘ mapdt f) [] = mapdt (g ⋆3 f) []
E: Type
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 -> G1 B
a: E * A
l: list (E * A)
IHl: (map (mapdt g) ∘ mapdt f) l = mapdt (g ⋆3 f) l
(map (mapdt g) ∘ mapdt f) (a :: l) =
mapdt (g ⋆3 f) (a :: l)
    -
E: Type
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 -> G1 B
(map (mapdt g) ∘ mapdt f) [] = mapdt (g ⋆3 f) [] unfold compose.
E: Type
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 -> G1 B
map (mapdt g) (mapdt f []) = mapdt (g ⋆3 f) []
      cbn.
E: Type
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 -> G1 B
map (mapdt g) (pure []) = pure []
      compose near (@nil (E * B)).
E: Type
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 -> G1 B
(map (mapdt g) ∘ pure) [] = pure []
      rewrite (natural (ϕ := @pure G1 _)).
E: Type
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 -> G1 B
(pure ∘ map (mapdt g)) [] = pure []
      reflexivity.
    -
E: Type
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 -> G1 B
a: E * A
l: list (E * A)
IHl: (map (mapdt g) ∘ mapdt f) l = mapdt (g ⋆3 f) l
(map (mapdt g) ∘ mapdt f) (a :: l) =
mapdt (g ⋆3 f) (a :: l) unfold compose at 1.
E: Type
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 -> G1 B
a: E * A
l: list (E * A)
IHl: (map (mapdt g) ∘ mapdt f) l = mapdt (g ⋆3 f) l
map (mapdt g) (mapdt f (a :: l)) =
mapdt (g ⋆3 f) (a :: l)
      unfold compose at 1 in IHl.
E: Type
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 -> G1 B
a: E * A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
map (mapdt g) (mapdt f (a :: l)) =
mapdt (g ⋆3 f) (a :: l)
      destruct a as [e a].
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
map (mapdt g) (mapdt f ((e, a) :: l)) =
mapdt (g ⋆3 f) ((e, a) :: l)
      autorewrite with tea_env.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
map (mapdt g)
  (pure cons <⋆> σ (e, f (e, a)) <⋆> mapdt f l) =
pure cons <⋆> σ (e, (g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      unfold strength.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
map (mapdt g)
  (pure cons <⋆> map (pair e) (f (e, a)) <⋆> mapdt f l) =
pure cons <⋆> map (pair e) ((g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      rewrite (map_to_ap (A := B) (G := G1)).
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
map (mapdt g)
  (pure cons <⋆> (pure (pair e) <⋆> f (e, a)) <⋆>
   mapdt f l) =
pure cons <⋆> map (pair e) ((g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      rewrite <- ap4; do 2 rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
map (mapdt g)
  (pure (cons ∘ pair e) <⋆> f (e, a) <⋆> mapdt f l) =
pure cons <⋆> map (pair e) ((g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      rewrite map_to_ap.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (mapdt g) <⋆>
(pure (cons ∘ pair e) <⋆> f (e, a) <⋆> mapdt f l) =
pure cons <⋆> map (pair e) ((g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      rewrite <- ap4; rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g)) <⋆>
(pure (cons ∘ pair e) <⋆> f (e, a)) <⋆> mapdt f l =
pure cons <⋆> map (pair e) ((g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      rewrite <- ap4; do 2 rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure cons <⋆> map (pair e) ((g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      (* RHS *)
      rewrite map_to_ap.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure cons <⋆> (pure (pair e) <⋆> (g ⋆3 f) (e, a)) <⋆>
mapdt (g ⋆3 f) l
      rewrite <- ap4; do 2 rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (cons ∘ pair e) <⋆> (g ⋆3 f) (e, a) <⋆>
mapdt (g ⋆3 f) l
      rewrite <- IHl.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (cons ∘ pair e) <⋆> (g ⋆3 f) (e, a) <⋆>
map (mapdt g) (mapdt f l)
      rewrite map_to_ap.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (cons ∘ pair e) <⋆> (g ⋆3 f) (e, a) <⋆>
(pure (mapdt g) <⋆> mapdt f l)
      rewrite (ap_compose1 G2 G1).
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (ap G2) <⋆>
(pure (cons ∘ pair e) <⋆> (g ⋆3 f) (e, a)) <⋆>
(pure (mapdt g) <⋆> mapdt f l)
      rewrite (ap_compose1 G2 G1).
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (ap G2) <⋆>
(pure (ap G2) <⋆> pure (cons ∘ pair e) <⋆>
 (g ⋆3 f) (e, a)) <⋆> (pure (mapdt g) <⋆> mapdt f l)
      unfold_ops @Pure_compose.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (ap G2) <⋆>
(pure (ap G2) <⋆> pure (pure (cons ∘ pair e)) <⋆>
 (g ⋆3 f) (e, a)) <⋆> (pure (mapdt g) <⋆> mapdt f l)
      rewrite <- ap4.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure compose <⋆>
(pure (ap G2) <⋆>
 (pure (ap G2) <⋆> pure (pure (cons ∘ pair e)) <⋆>
  (g ⋆3 f) (e, a))) <⋆> pure (mapdt g) <⋆> mapdt f l
      rewrite <- ap4; do 3 rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (compose ∘ ap G2) <⋆>
(pure (ap G2 (pure (cons ∘ pair e))) <⋆>
 (g ⋆3 f) (e, a)) <⋆> pure (mapdt g) <⋆> mapdt f l
      rewrite <- ap4; do 2 rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (compose (mapdt g) ∘ (cons ∘ pair e)) <⋆>
f (e, a) <⋆> mapdt f l =
pure (compose ∘ ap G2 ∘ ap G2 (pure (cons ∘ pair e))) <⋆>
(g ⋆3 f) (e, a) <⋆> pure (mapdt g) <⋆> mapdt f l
      unfold kc3, compose, strength.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (fun a : B => mapdt g ○ cons (e, a)) <⋆> f (e, a) <⋆>
mapdt f l =
pure
  (fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
   => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) <⋆>
map g
  (let '(a, t) := cobind f (e, a) in map (pair a) t) <⋆>
pure (mapdt g) <⋆> mapdt f l
      change (cobind f (e, a)) with (e, f (e, a)).
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (fun a : B => mapdt g ○ cons (e, a)) <⋆> f (e, a) <⋆>
mapdt f l =
pure
  (fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
   => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) <⋆>
map g (let '(a, t) := (e, f (e, a)) in map (pair a) t) <⋆>
pure (mapdt g) <⋆> mapdt f l
      do 2 rewrite map_to_ap.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (fun a : B => mapdt g ○ cons (e, a)) <⋆> f (e, a) <⋆>
mapdt f l =
pure
  (fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
   => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) <⋆>
(pure g <⋆> (pure (pair e) <⋆> f (e, a))) <⋆>
pure (mapdt g) <⋆> mapdt f l
      rewrite <- ap4; repeat rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (fun a : B => mapdt g ○ cons (e, a)) <⋆> f (e, a) <⋆>
mapdt f l =
pure
  ((fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
    => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) ∘ g) <⋆>
(pure (pair e) <⋆> f (e, a)) <⋆> pure (mapdt g) <⋆>
mapdt f l
      rewrite <- ap4; repeat rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (fun a : B => mapdt g ○ cons (e, a)) <⋆> f (e, a) <⋆>
mapdt f l =
pure
  ((fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
    => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) ∘ g
   ∘ pair e) <⋆> f (e, a) <⋆> pure (mapdt g) <⋆>
mapdt f l
      rewrite ap3.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (fun a : B => mapdt g ○ cons (e, a)) <⋆> f (e, a) <⋆>
mapdt f l =
pure (evalAt (mapdt g)) <⋆>
(pure
   ((fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
     => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) ∘ g
    ∘ pair e) <⋆> f (e, a)) <⋆> mapdt f l
      rewrite <- ap4; repeat rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
pure (fun a : B => mapdt g ○ cons (e, a)) <⋆> f (e, a) <⋆>
mapdt f l =
pure
  (evalAt (mapdt g)
   ∘ ((fun (a : G2 C)
         (f : env E B -> G2 (list (E * C))) =>
       ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) ∘ g
      ∘ pair e)) <⋆> f (e, a) <⋆> mapdt f l
      repeat fequal.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
(fun a : B => mapdt g ○ cons (e, a)) =
evalAt (mapdt g)
∘ ((fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
    => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) ∘ g
   ∘ pair e)
      ext b l'.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
b: B
l': list (E * B)
mapdt g ((e, b) :: l') =
(evalAt (mapdt g)
 ∘ ((fun (a : G2 C) (f : env E B -> G2 (list (E * C)))
     => ap G2 (pure (cons ○ pair e) <⋆> a) ○ f) ∘ g
    ∘ pair e)) b l' unfold compose.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
b: B
l': list (E * B)
mapdt g ((e, b) :: l') =
evalAt (mapdt g)
  (fun f : env E B -> G2 (list (E * C)) =>
   ap G2 (pure (cons ○ pair e) <⋆> g (e, b)) ○ f) l'
      autorewrite with tea_env.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
b: B
l': list (E * B)
pure cons <⋆> σ (e, g (e, b)) <⋆> mapdt g l' =
evalAt (mapdt g)
  (fun f : env E B -> G2 (list (E * C)) =>
   ap G2 (pure (cons ○ pair e) <⋆> g (e, b)) ○ f) l'
      unfold strength.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
b: B
l': list (E * B)
pure cons <⋆> map (pair e) (g (e, b)) <⋆> mapdt g l' =
evalAt (mapdt g)
  (fun f : env E B -> G2 (list (E * C)) =>
   ap G2 (pure (cons ○ pair e) <⋆> g (e, b)) ○ f) l'
      rewrite map_to_ap.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
b: B
l': list (E * B)
pure cons <⋆> (pure (pair e) <⋆> g (e, b)) <⋆>
mapdt g l' =
evalAt (mapdt g)
  (fun f : env E B -> G2 (list (E * C)) =>
   ap G2 (pure (cons ○ pair e) <⋆> g (e, b)) ○ f) l'
      rewrite <- ap4; repeat rewrite ap2.
E: Type
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 -> G1 B
e: E
a: A
l: list (E * A)
IHl: map (mapdt g) (mapdt f l) = mapdt (g ⋆3 f) l
b: B
l': list (E * B)
pure (cons ∘ pair e) <⋆> g (e, b) <⋆> mapdt g l' =
evalAt (mapdt g)
  (fun f : env E B -> G2 (list (E * C)) =>
   ap G2 (pure (cons ○ pair e) <⋆> g (e, b)) ○ f) l'
      reflexivity.
  Qed.

  Lemma env_mapdt_morph
    `{ApplicativeMorphism G1 G2 ϕ}:
      forall (A B: Type) (f: E * A -> G1 B),
          ϕ (env E B) ∘ mapdt (T := env E) f =
            mapdt (T := env E) (ϕ B ∘ f).
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
forall (A B : Type) (f : E * A -> G1 B),
ϕ (env E B) ∘ mapdt f = mapdt (ϕ B ∘ f)
  Proof.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
forall (A B : Type) (f : E * A -> G1 B),
ϕ (env E B) ∘ mapdt f = mapdt (ϕ B ∘ f)
    intros.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (env E B) ∘ mapdt f = mapdt (ϕ B ∘ f) ext l.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
l: env E A
(ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l induction l.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
(ϕ (env E B) ∘ mapdt f) [] = mapdt (ϕ B ∘ f) []
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
a: E * A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
(ϕ (env E B) ∘ mapdt f) (a :: l) =
mapdt (ϕ B ∘ f) (a :: l)
    -
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
(ϕ (env E B) ∘ mapdt f) [] = mapdt (ϕ B ∘ f) [] unfold compose.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (env E B) (mapdt f []) = mapdt (ϕ B ○ f) [] cbn.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
ϕ (env E B) (pure []) = pure []
      rewrite appmor_pure.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
pure [] = pure []
      reflexivity.
    -
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
a: E * A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
(ϕ (env E B) ∘ mapdt f) (a :: l) =
mapdt (ϕ B ∘ f) (a :: l) destruct a as (e, a).
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
(ϕ (env E B) ∘ mapdt f) ((e, a) :: l) =
mapdt (ϕ B ∘ f) ((e, a) :: l)
      unfold compose at 1.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
ϕ (env E B) (mapdt f ((e, a) :: l)) =
mapdt (ϕ B ∘ f) ((e, a) :: l)
      autorewrite with tea_env.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
ϕ (env E B)
  (pure cons <⋆> σ (e, f (e, a)) <⋆> mapdt f l) =
pure cons <⋆> σ (e, (ϕ B ∘ f) (e, a)) <⋆>
mapdt (ϕ B ∘ f) l
      rewrite <- IHl.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
ϕ (env E B)
  (pure cons <⋆> σ (e, f (e, a)) <⋆> mapdt f l) =
pure cons <⋆> σ (e, (ϕ B ∘ f) (e, a)) <⋆>
(ϕ (env E B) ∘ mapdt f) l
      unfold compose at 2.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
ϕ (env E B)
  (pure cons <⋆> σ (e, f (e, a)) <⋆> mapdt f l) =
pure cons <⋆> σ (e, (ϕ B ∘ f) (e, a)) <⋆>
ϕ (env E B) (mapdt f l)
      rewrite ap_morphism_1.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
ϕ (list (E * B) -> env E B)
  (pure cons <⋆> σ (e, f (e, a))) <⋆>
ϕ (list (E * B)) (mapdt f l) =
pure cons <⋆> σ (e, (ϕ B ∘ f) (e, a)) <⋆>
ϕ (env E B) (mapdt f l)
      rewrite ap_morphism_1.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
ϕ (E * B -> list (E * B) -> env E B) (pure cons) <⋆>
ϕ (E * B) (σ (e, f (e, a))) <⋆>
ϕ (list (E * B)) (mapdt f l) =
pure cons <⋆> σ (e, (ϕ B ∘ f) (e, a)) <⋆>
ϕ (env E B) (mapdt f l)
      rewrite appmor_pure.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
pure cons <⋆> ϕ (E * B) (σ (e, f (e, a))) <⋆>
ϕ (list (E * B)) (mapdt f l) =
pure cons <⋆> σ (e, (ϕ B ∘ f) (e, a)) <⋆>
ϕ (env E B) (mapdt f l)
      unfold strength.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
pure cons <⋆> ϕ (E * B) (map (pair e) (f (e, a))) <⋆>
ϕ (list (E * B)) (mapdt f l) =
pure cons <⋆> map (pair e) ((ϕ B ∘ f) (e, a)) <⋆>
ϕ (env E B) (mapdt f l)
      rewrite appmor_natural.
E: Type
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: G1 ⇒ G2
H5: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: E * A -> G1 B
e: E
a: A
l: list (E * A)
IHl: (ϕ (env E B) ∘ mapdt f) l = mapdt (ϕ B ∘ f) l
pure cons <⋆> map (pair e) (ϕ B (f (e, a))) <⋆>
ϕ (list (E * B)) (mapdt f l) =
pure cons <⋆> map (pair e) ((ϕ B ∘ f) (e, a)) <⋆>
ϕ (env E B) (mapdt f l)
      reflexivity.
  Qed.

End env_laws.

(** ** Typeclass Instance *)
(**********************************************************************)
#[export] Instance DecoratedTraversableFunctor_env (E: Type):
  DecoratedTraversableFunctor E (env E) :=
  {| kdtf_mapdt1 := env_mapdt1 E;
     kdtf_mapdt2 := @env_mapdt2 E;
     kdtf_morph := @env_mapdt_morph E;
  |}.

#[export] Instance Functor_env (E: Type): Functor (env E) :=
  DerivedInstances.Functor_DecoratedTraversableFunctor.

#[export] Instance DecoratedFunctor_env (E: Type):
  DecoratedFunctor E (env E) :=
  DerivedInstances.DecoratedFunctor_DecoratedTraversableFunctor.

#[export] Instance TraversableFunctor_env (E: Type):
  TraversableFunctor (env E) :=
  DerivedInstances.TraversableFunctor_DecoratedTraversableFunctor.

(** ** Alternative Specifications for <<mapd>> *)
(**********************************************************************)
Lemma env_mapd_spec: forall (E A B: Type) (f: E * A -> B),
    mapd (T := env E) f = map (F := list) (cobind (W := (E ×)) f).
forall (E A B : Type) (f : E * A -> B),
mapd f = map (cobind f)
Proof.
forall (E A B : Type) (f : E * A -> B),
mapd f = map (cobind f)
  simple_env_tactic.
Qed.

Lemma env_map_spec:
  forall (E A B: Type) (f: A -> B),
    map (F := env E) f = map (F := list) (map (F := (E ×)) f).
forall (E A B : Type) (f : A -> B),
map f = map (map f)
Proof.
forall (E A B : Type) (f : A -> B),
map f = map (map f)
  simple_env_tactic.
Qed.

Lemma env_map_spec2: forall (E A B: Type) (f: A -> B),
    map (F := env E) f = map (Map := Map_compose list (E ×)) f.
forall (E A B : Type) (f : A -> B), map f = map f
Proof.
forall (E A B : Type) (f : A -> B), map f = map f
  intros.
E, A, B: Type
f: A -> B
map f = map f now rewrite env_map_spec.
Qed.

(** * Decorated Traversable Monad Instance (Kleisli) *)
(**********************************************************************)
Section env.

  Context
    `{Monoid W}.

  #[export] Instance Return_env: Return (env W) :=
    fun A => ret (T := list) ∘ ret (T := (W ×)) (A := A).

  Fixpoint binddt_env (G: Type -> Type) `{Map G} `{Pure G} `{Mult G}
    `(f: W * A -> G (env W B)) (Γ: env W A): G (env W B) :=
    match Γ with
    | nil => pure (@nil (W * B))
    | (w, a) :: rest =>
        pure (@List.app (W * B))
          <⋆> map (F := G) (fun x => shift list (w, x)) (f (w, a))
          <⋆> binddt_env G f rest
    end.

  Fixpoint bindd_env `(f: W * A -> env W B) (Γ: env W A): env W B :=
    match Γ with
    | nil => @nil (W * B)
    | (w, a) :: rest =>
        shift list (w, f (w, a)) ++ bindd_env f rest
    end.

  Fixpoint bind_env `(f: A -> env W B) (l: env W A): env W B :=
    match l with
    | nil => pure (@nil (W * B))
    | (w, a) :: xs =>
        pure (@List.app (W * B))
          <⋆> shift list (w, f a)
          <⋆> bind_env f xs
    end.

  #[export] Instance Binddt_env: Binddt W (env W) (env W) := @binddt_env.
  #[export] Instance Bindd_env: Bindd W (env W) (env W) := @bindd_env.
  #[export] Instance Bind_env: Bind (env W) (env W) := @bind_env.

End env.