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

#[local] Generalizable Variables T G ϕ.

(** * Kleisli Traversable Functors from Categorical Traversable Functors *)
(**********************************************************************)

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

  #[export] Instance Traverse_Categorical
    (T: Type -> Type)
    `{Map_T: Map T}
    `{Dist_T: ApplicativeDist T}:
  Traverse T :=
  fun (G: Type -> Type) `{Map G} `{Pure G} `{Mult G}
    (A B: Type) (f: A -> G B) => dist T G ∘ map f.

  #[export] Instance Compat_Map_Traverse_Categorical
    (T: Type -> Type)
    `{Map_T: Map T}
    `{Dist_T: ApplicativeDist T}
    `{Categorical.TraversableFunctor.TraversableFunctor T}
    :
    Compat_Map_Traverse T.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
Compat_Map_Traverse T
  Proof.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
Compat_Map_Traverse T
    unfold Compat_Map_Traverse.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H = DerivedOperations.Map_Traverse T
    unfold DerivedOperations.Map_Traverse.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H = (fun (A B : Type) (f : A -> B) => traverse f)
    ext A B f.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A, B: Type
f: A -> B
H A B f = traverse f
    unfold traverse.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A, B: Type
f: A -> B
H A B f =
Traverse_Categorical T (fun A : Type => A) Map_I
  Pure_I Mult_I A B f
    unfold Traverse_Categorical.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A, B: Type
f: A -> B
H A B f = dist T (fun A : Type => A) ∘ map f
    rewrite dist_unit.
T: Type -> Type
Map_T: Map T
Dist_T: ApplicativeDist T
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A, B: Type
f: A -> B
H A B f = id ∘ map f
    reflexivity.
  Qed.

End DerivedOperations.

(** ** Compatibility Classes *)
(**********************************************************************)
Class Compat_Traverse_Categorical
    (F: Type -> Type)
    `{Traverse_F: Traverse F}
    `{Map_F: Map F}
    `{Dist_F: ApplicativeDist F} :=
  compat_traverse_categorical:
    Traverse_F = @DerivedOperations.Traverse_Categorical F Map_F Dist_F.

#[export] Instance compat_traverse_categorical_self
    (F: Type -> Type)
    `{Map_F: Map F}
    `{Dist_F: ApplicativeDist F}:
  Compat_Traverse_Categorical F (Traverse_F := DerivedOperations.Traverse_Categorical F).
F: Type -> Type
Map_F: Map F
Dist_F: ApplicativeDist F
Compat_Traverse_Categorical F
Proof.
F: Type -> Type
Map_F: Map F
Dist_F: ApplicativeDist F
Compat_Traverse_Categorical F
  reflexivity.
Qed.


Lemma traverse_to_categorical {F}
    `{Traverse_F: Traverse F}
    `{Map_F: Map F}
    `{Dist_F: ApplicativeDist F}
    `{Compat: ! Compat_Traverse_Categorical F}:
  forall {G} `{Map_G: Map G} `{Pure_G: Pure G} `{Mult_G: Mult G} (A B: Type) (t: F A) (f: A -> G B),
    @traverse F Traverse_F G Map_G Pure_G Mult_G A B f =dist F G ∘ map f.
F: Type -> Type
Traverse_F: Traverse F
Map_F: Map F
Dist_F: ApplicativeDist F
Compat: Compat_Traverse_Categorical F
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G) (A B : Type),
F A ->
forall f : A -> G B, traverse f = dist F G ∘ map f
Proof.
F: Type -> Type
Traverse_F: Traverse F
Map_F: Map F
Dist_F: ApplicativeDist F
Compat: Compat_Traverse_Categorical F
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G) (A B : Type),
F A ->
forall f : A -> G B, traverse f = dist F G ∘ map f
  now rewrite compat_traverse_categorical.
Qed.

(** ** Derived Laws *)
(**********************************************************************)
Module DerivedInstances.

  (* Alectryon doesn't like this
     Import CategoricalToKleisli.TraversableFunctor.DerivedOperations.
   *)
  Import DerivedOperations.

  Section with_functor.

    Context
      `{Categorical.TraversableFunctor.TraversableFunctor T}.

    Theorem traverse_id: forall (A: Type),
        traverse (G := fun A => A) id = @id (T A).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall A : Type, traverse id = id
    Proof.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall A : Type, traverse id = id
      intros.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
traverse id = id unfold traverse.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
Traverse_Categorical T (fun A : Type => A) Map_I
  Pure_I Mult_I A A id = id unfold_ops @Traverse_Categorical.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
dist T (fun A : Type => A) ∘ map id = id ext t.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
t: T A
(dist T (fun A : Type => A) ∘ map id) t = id t
      rewrite (dist_unit (F := T)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
t: T A
(id ∘ map id) t = id t
      rewrite (fun_map_id (F := T)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
t: T A
(id ∘ id) t = id t
      reflexivity.
    Qed.

    Theorem traverse_id_purity: forall `{Applicative G} (A: Type),
        traverse (pure (F := G)) = @pure G _ (T A).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G -> forall A : Type, traverse pure = pure
    Proof.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G -> forall A : Type, traverse pure = pure
      intros.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
traverse pure = pure unfold traverse.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
Traverse_Categorical T G Map_G Pure_G Mult_G A A pure =
pure
      unfold_ops @Traverse_Categorical.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
dist T G ∘ map pure = pure
      ext t.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
t: T A
(dist T G ∘ map pure) t = pure t rewrite map_purity_1.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H2: Applicative G
A: Type
t: T A
pure t = pure t
      reflexivity.
    Qed.

    Lemma traverse_traverse `{Applicative G1} `{Applicative G2}:
      forall (A B C: Type) (g: B -> G2 C) (f: A -> G1 B),
        map (F := G1) (traverse (G := G2) g) ∘ traverse (G := G1) f =
          traverse (G := G1 ∘ G2) (map g ∘ f).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
forall (A B C : Type) (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (map g ∘ f)
    Proof.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
forall (A B C : Type) (g : B -> G2 C) (f : A -> G1 B),
map (traverse g) ∘ traverse f = traverse (map g ∘ f)
      introv.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (traverse g) ∘ traverse f = traverse (map g ∘ f) unfold traverse.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map
  (Traverse_Categorical T G2 Map_G0 Pure_G0 Mult_G0 B
     C g)
∘ Traverse_Categorical T G1 Map_G Pure_G Mult_G A B f =
Traverse_Categorical T (G1 ∘ G2) (Map_compose G1 G2)
  (Pure_compose G1 G2) (Mult_compose G1 G2) A C
  (map g ∘ f)
      unfold_ops @Traverse_Categorical.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ (dist T G1 ∘ map f) =
dist T (G1 ∘ G2) ∘ map (map g ∘ f)
      rewrite (dist_linear (F := T)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ (dist T G1 ∘ map f) =
map (dist T G2) ∘ dist T G1 ∘ map (map g ∘ f)
      repeat reassociate <-.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ dist T G1 ∘ map (map g ∘ f)
      rewrite <- (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ dist T G1 ∘ (map (map g) ∘ map f)
      repeat reassociate <-.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ dist T G1 ∘ map (map g) ∘ map f
      reassociate -> near (map (map g)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ (dist T G1 ∘ map (map g)) ∘ map f
      change (map (map g)) with (map (F := T ∘ G1) g).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ (dist T G1 ∘ map g) ∘ map f
      rewrite <- (natural (ϕ := @dist T _ G1 _ _ _)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ (map g ∘ dist T G1) ∘ map f
      unfold_ops @Map_compose.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ (map (map g) ∘ dist T G1) ∘ map f
      reassociate <-.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ map (map g) ∘ dist T G1 ∘ map f
      unfold_compose_in_compose.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H2: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H3: Applicative G2
A, B, C: Type
g: B -> G2 C
f: A -> G1 B
map (dist T G2 ∘ map g) ∘ dist T G1 ∘ map f =
map (dist T G2) ∘ map (map g) ∘ dist T G1 ∘ map f
      now rewrite (fun_map_map (F := G1)).
    Qed.

    Lemma traverse_morphism `{morph: ApplicativeMorphism G1 G2 ϕ}:
      forall (A B: Type) (f: A -> G1 B),
        ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
forall (A B : Type) (f : A -> G1 B),
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
    Proof.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
forall (A B : Type) (f : A -> G1 B),
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f)
      intros.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ traverse f = traverse (ϕ B ∘ f) unfold traverse.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ Traverse_Categorical T G1 H2 H4 H3 A B f =
Traverse_Categorical T G2 H5 H7 H6 A B (ϕ B ∘ f)
      unfold_ops @Traverse_Categorical.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ (dist T G1 ∘ map f) =
dist T G2 ∘ map (ϕ B ∘ f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
ϕ (T B) ∘ dist T G1 ∘ map f =
dist T G2 ∘ map (ϕ B ∘ f)
      rewrite <- (dist_morph (F := T)).
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
dist T G2 ∘ map (ϕ B) ∘ map f =
dist T G2 ∘ map (ϕ B ∘ f)
      reassociate ->.
T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
G1, G2: Type -> Type
H2: Map G1
H3: Mult G1
H4: Pure G1
H5: Map G2
H6: Mult G2
H7: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 B
dist T G2 ∘ (map (ϕ B) ∘ map f) =
dist T G2 ∘ map (ϕ B ∘ f)
      now rewrite (fun_map_map (F := T)).
    Qed.

    #[export] Instance TraversableFunctor_Kleisli_Categorical:
      Classes.Kleisli.TraversableFunctor.TraversableFunctor T :=
      {| trf_traverse_id := @traverse_id;
         trf_traverse_traverse := @traverse_traverse;
         trf_traverse_morphism := @traverse_morphism;
      |}.

  End with_functor.

End DerivedInstances.