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

Import Comonad.Notations.
Import Product.Notations.

#[local] Generalizable Variables G ϕ.

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

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

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

    #[export] Instance Dist_Mapdt: ApplicativeDist T :=
      fun G _ _ _ A =>
        mapdt (T := T) (G := G) (extract (W := (E ×)) (A := G A)).

    #[export] Instance Decorate_Mapdt: Decorate E T :=
      fun A => mapdt (G := fun A => A) (@id (E * A)).

  End operations.
End DerivedOperations.

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

  (* Alectryon doesn't like this
     Import KleisliToCategorical.DecoratedTraversableFunctor.DerivedOperations.
   *)
  Import DerivedOperations.
  Import Kleisli.DecoratedTraversableFunctor.DerivedOperations.
  Import Kleisli.DecoratedTraversableFunctor.DerivedInstances.

  Section instances.

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

    Lemma dec_dec: forall (A: Type),
        dec T ∘ dec T =
          map (F := T) (cojoin (W := (E ×))) ∘ dec T (A := A).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, dec T ∘ dec T = map cojoin ∘ dec T
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, dec T ∘ dec T = map cojoin ∘ dec T
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
dec T ∘ dec T = map cojoin ∘ dec T
      unfold_ops @Decorate_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapdt id ∘ mapdt id = map cojoin ∘ mapdt id
      rewrite <- mapd_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapd id ∘ mapdt id = map cojoin ∘ mapdt id
      rewrite <- mapd_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapd id ∘ mapd id = map cojoin ∘ mapd id
      rewrite mapd_mapd.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapd (id ⋆1 id) = map cojoin ∘ mapd id
      rewrite map_mapd.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapd (id ⋆1 id) = mapd (cojoin ∘ id)
      reflexivity.
    Qed.

    Lemma dec_extract: forall (A: Type),
        map (F := T) (extract (W := (E ×))) ∘ dec T = @id (T A).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, map extract ∘ dec T = id
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, map extract ∘ dec T = id
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
map extract ∘ dec T = id
      unfold_ops @Decorate_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
map extract ∘ mapdt id = id
      rewrite <- mapd_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
map extract ∘ mapd id = id
      rewrite map_mapd.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapd (extract ∘ id) = id
      change (?f ∘ id) with f.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapd extract = id
      rewrite mapd_id.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma dec_natural: Natural (@dec E T _).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
Natural (@dec E T (Decorate_Mapdt E T))
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
Natural (@dec E T (Decorate_Mapdt E T))
      constructor.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
Functor T
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
Functor (T ○ prod E)
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (A B : Type) (f : A -> B),
map f ∘ dec T = dec T ∘ map f
      -
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
Functor T typeclasses eauto.
      -
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
Functor (T ○ prod E) typeclasses eauto.
      -
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (A B : Type) (f : A -> B),
map f ∘ dec T = dec T ∘ map f intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A, B: Type
f: A -> B
map f ∘ dec T = dec T ∘ map f
        unfold_ops @Map_compose.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A, B: Type
f: A -> B
map (map f) ∘ dec T = dec T ∘ map f
        unfold_ops @Decorate_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A, B: Type
f: A -> B
map (map f) ∘ mapdt id = mapdt id ∘ map f
        rewrite <- mapd_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A, B: Type
f: A -> B
map (map f) ∘ mapd id = mapdt id ∘ map f
        rewrite <- mapd_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A, B: Type
f: A -> B
map (map f) ∘ mapd id = mapd id ∘ map f
        rewrite map_mapd.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A, B: Type
f: A -> B
mapd (map f ∘ id) = mapd id ∘ map f
        rewrite mapd_map.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A, B: Type
f: A -> B
mapd (map f ∘ id) = mapd (id ∘ map f)
        reflexivity.
    Qed.

    #[export] Instance DecoratedFunctor_Categorical_Kleisli:
      Categorical.DecoratedFunctor.DecoratedFunctor E T :=
      {| dfun_dec_natural := dec_natural;
         dfun_dec_dec := dec_dec;
         dfun_dec_extract := dec_extract;
      |}.

    (** *** Traversable functor instance *)
    (******************************************************************)
    Lemma dist_natural_T:
      forall (G: Type -> Type) (H2: Map G) (H3: Pure G) (H4: Mult G),
        Applicative G -> Natural (@dist T _ G H2 H3 H4).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
Natural (@dist T (Dist_Mapdt E T) G H2 H3 H4)
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
Natural (@dist T (Dist_Mapdt E T) G H2 H3 H4)
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
Natural (@dist T (Dist_Mapdt E T) G H2 H3 H4) constructor.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
Functor (T ○ G)
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
Functor (G ○ T)
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ dist T G = dist T G ∘ map f
      -
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
Functor (T ○ G) typeclasses eauto.
      -
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
Functor (G ○ T) typeclasses eauto.
      -
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ dist T G = dist T G ∘ map f intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A, B: Type
f: A -> B
map f ∘ dist T G = dist T G ∘ map f
        unfold_ops @Map_compose.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A, B: Type
f: A -> B
map (map f) ∘ dist T G = dist T G ∘ map (map f)
        unfold_ops @Dist_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A, B: Type
f: A -> B
map (map f) ∘ mapdt extract =
mapdt extract ∘ map (map f)
        rewrite map_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A, B: Type
f: A -> B
mapdt (map f ∘ extract) = mapdt extract ∘ map (map f)
        rewrite mapdt_map.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A, B: Type
f: A -> B
mapdt (map f ∘ extract) =
mapdt (extract ∘ map (map f))
        rewrite <- (natural (ϕ := fun A => extract (A := A))).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A, B: Type
f: A -> B
mapdt (map f ∘ extract) =
mapdt (map (map f) ∘ extract)
        reflexivity.
    Qed.

    Lemma dist_morph_T: forall `{ApplicativeMorphism G1 G2 ϕ},
      forall (A: Type),
        dist T G2 ∘ map (F := T) (ϕ A) = ϕ (T A) ∘ dist T G1.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 G2 : Type -> 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),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 G2 : Type -> 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),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> 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 ϕ
A: Type
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      unfold_ops @Map_compose.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> 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 ϕ
A: Type
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      unfold_ops @Dist_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> 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 ϕ
A: Type
mapdt extract ∘ map (ϕ A) = ϕ (T A) ∘ mapdt extract
      infer_applicative_instances.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> 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 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
mapdt extract ∘ map (ϕ A) = ϕ (T A) ∘ mapdt extract
      rewrite mapdt_map.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> 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 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
mapdt (extract ∘ map (ϕ A)) = ϕ (T A) ∘ mapdt extract
      rewrite <- (natural (ϕ := fun A => extract (W := (E ×)) (A := A))).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> 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 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
mapdt (map (ϕ A) ∘ extract) = ϕ (T A) ∘ mapdt extract
      rewrite (kdtf_morph (E := E) (T := T)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1, G2: Type -> 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 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
mapdt (map (ϕ A) ∘ extract) = mapdt (ϕ A ∘ extract)
      reflexivity.
    Qed.

    Lemma dist_unit_T: forall (A: Type),
        dist T (fun A0: Type => A0) = @id (T A).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, dist T (fun A0 : Type => A0) = id
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall A : Type, dist T (fun A0 : Type => A0) = id
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
dist T (fun A0 : Type => A0) = id
      unfold_ops @Dist_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
A: Type
mapdt extract = id
      now rewrite (kdtf_mapdt1 (E := E) (T := T)).
    Qed.

    (* TODO Typeset this better *)
    Lemma dist_linear_T:
      forall (G1: Type -> Type)
        (H2: Map G1) (H3: Pure G1) (H4: Mult G1),
        Applicative G1 ->
        forall (G2: Type -> Type)
          (H6: Map G2) (H7: Pure G2) (H8: Mult G2),
          Applicative G2 -> forall (A: Type),
            dist T (G1 ∘ G2) (A := A) =
              map (F := G1) (dist T G2) ∘ dist T G1.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H6 : Map G2)
  (H7 : Pure G2) (H8 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H6 : Map G2)
  (H7 : Pure G2) (H8 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H1: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H5: Applicative G2
A: Type
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
      unfold_ops @Dist_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H1: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H5: Applicative G2
A: Type
mapdt extract = map (mapdt extract) ∘ mapdt extract
      rewrite (kdtf_mapdt2 (E := E) (T := T)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H1: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H5: Applicative G2
A: Type
mapdt extract = mapdt (kc3 extract extract)
      change (extract (W := prod E) (A := G2 A)) with
        (id ∘ extract (W := prod E) (A := G2 A)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H1: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H5: Applicative G2
A: Type
mapdt extract = mapdt (kc3 (id ∘ extract) extract)
      rewrite kc3_23.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H1: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H5: Applicative G2
A: Type
mapdt extract = mapdt (map id ∘ extract)
      rewrite (fun_map_id (F := G1)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H1: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H5: Applicative G2
A: Type
mapdt extract = mapdt (id ∘ extract)
      reflexivity.
    Qed.

    #[export] Instance TraversableFunctor_Categorical_DecoratedTraversableFunctor_Kleisli
     : Categorical.TraversableFunctor.TraversableFunctor T :=
      {| dist_natural := dist_natural_T;
         dist_morph := @dist_morph_T;
         dist_unit := dist_unit_T;
         dist_linear := dist_linear_T;
      |}.

    Lemma dtfun_compat_T:
      forall (G: Type -> Type) (H2: Map G) (H3: Pure G) (H4: Mult G),
        Applicative G -> forall (A: Type),
          dist T G ∘ map (F := T) strength ∘ dec (A := G A) T =
            map (F := G) (dec T) ∘ dist T G.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ map strength ∘ dec T =
map (dec T) ∘ dist T G
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
forall A : Type,
dist T G ∘ map strength ∘ dec T =
map (dec T) ∘ dist T G
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
dist T G ∘ map strength ∘ dec T =
map (dec T) ∘ dist T G
      unfold_ops @Dist_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt extract ∘ map strength ∘ dec T =
map (dec T) ∘ mapdt extract
      unfold_ops @Decorate_Mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt extract ∘ map strength ∘ mapdt id =
map (mapdt id) ∘ mapdt extract
      rewrite <- mapd_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt extract ∘ map strength ∘ mapd id =
map (mapdt id) ∘ mapdt extract
      reassociate -> on left.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt extract ∘ (map strength ∘ mapd id) =
map (mapdt id) ∘ mapdt extract
      rewrite map_mapd.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt extract ∘ mapd (strength ∘ id) =
map (mapdt id) ∘ mapdt extract
      rewrite <- mapd_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt extract ∘ mapd (strength ∘ id) =
map (mapd id) ∘ mapdt extract
      rewrite mapdt_mapd.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt (extract ⋆1 strength ∘ id) =
map (mapd id) ∘ mapdt extract
      rewrite mapd_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt (extract ⋆1 strength ∘ id) =
mapdt (map id ∘ strength ∘ cobind extract)
      rewrite (fun_map_id (F := G)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt (extract ⋆1 strength ∘ id) =
mapdt (id ∘ strength ∘ cobind extract)
      rewrite kcom_cobind1.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt (extract ⋆1 strength ∘ id) =
mapdt (id ∘ strength ∘ id)
      change (extract (W := prod E) (A := G (E * A))) with
        (id ∘ (extract (W := prod E) (A := G (E * A)))).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt (id ∘ extract ⋆1 strength ∘ id) =
mapdt (id ∘ strength ∘ id)
      rewrite kc1_01.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H1: Applicative G
A: Type
mapdt (id ∘ (strength ∘ id)) =
mapdt (id ∘ strength ∘ id)
      reflexivity.
    Qed.


    (** ** Typeclass Instance *)
    (******************************************************************)
    #[export] Instance
      DecoratedTraversableFunctor_Categorical_Kleisli:
      Categorical.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T :=
      {| dtfun_compat := dtfun_compat_T;
      |}.

  End instances.
End DerivedInstances.