From Tealeaves Require Import
  Classes.Categorical.TraversableMonad
  Classes.Kleisli.TraversableMonad
  Adapters.CategoricalToKleisli.TraversableFunctor.

Import Kleisli.TraversableMonad.Notations.

#[local] Generalizable Variables T G ϕ.

(** * Kleisli Traversable Monads from Categorical Traversable Monads *)
(**********************************************************************)

(** ** Operation *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance Bindt_Categorical
    (T: Type -> Type)
    `{Map_T: Map T} `{Join_T: Join T}
    `{Dist_T: ApplicativeDist T}
 : Bindt T T | 1000
  := fun (G: Type -> Type) _ _ _ (A B: Type)
       (f: A -> G (T B)) =>
       map (F := G) join ∘ dist T G ∘ map (F := T) f.

End DerivedOperations.

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

  Import DerivedOperations.

  Section with_monad.

    Context
      `{Categorical.TraversableMonad.TraversableMonad T}.

    (** *** Identity law *)
    (******************************************************************)
    Lemma ktm_bindt1_T:
      forall (A: Type),
        bindt (G := fun A => A) (ret (T := T)) = @id (T A).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall A : Type, bindt ret = id
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall A : Type, bindt ret = id
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
A: Type
bindt ret = id unfold bindt.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
A: Type
Bindt_Categorical T (fun A : Type => A) Map_I Pure_I
  Mult_I A A ret = id unfold_ops @Bindt_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
A: Type
map join ∘ dist T (fun A : Type => A) ∘ map ret = id
      unfold_ops @Map_I.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
A: Type
join ∘ dist T (fun A : Type => A) ∘ map ret = id rewrite (dist_unit (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
A: Type
join ∘ id ∘ map ret = id
      change (?g ∘ id ∘ ?f) with (g ∘ f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
A: Type
join ∘ map ret = id
      now rewrite (mon_join_map_ret (T := T)).
    Qed.

    (** *** Composition law *)
    (******************************************************************)
    Lemma ktm_bindt2_T: forall
        `{Applicative G1} `{Applicative G2}
        (A B C: Type)
        (g: B -> G2 (T C)) (f: A -> G1 (T B)),
        map (bindt g) ∘ bindt f = bindt (G := G1 ∘ G2) (g ⋆6 f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : B -> G2 (T C))
  (f : A -> G1 (T B)),
map (bindt g) ∘ bindt f = bindt (g ⋆6 f)
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (A B C : Type) (g : B -> G2 (T C))
  (f : A -> G1 (T B)),
map (bindt g) ∘ bindt f = bindt (g ⋆6 f)
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (bindt g) ∘ bindt f = bindt (g ⋆6 f) unfold bindt at 1 2 3.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (Bindt_Categorical T G2 Map_G0 Pure_G0 Mult_G0 B C g)
∘ Bindt_Categorical T G1 Map_G Pure_G Mult_G A B f =
Bindt_Categorical T (G1 ∘ G2) (Map_compose G1 G2)
  (Pure_compose G1 G2) (Mult_compose G1 G2) A C
  (g ⋆6 f)
      unfold_ops @Bindt_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ dist T G2 ∘ map g)
∘ (map join ∘ dist T G1 ∘ map f) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate -> on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ dist T G2 ∘ map g)
∘ (map join ∘ dist T G1 ∘ map f) =
map join ∘ (dist T (G1 ∘ G2) ∘ map (g ⋆6 f)) repeat reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ dist T G2 ∘ map g) ∘ map join
∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (fun_map_map (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ dist T G2 ∘ map g ∘ join) ∘ dist T G1
∘ map f = map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate -> near join.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ dist T G2 ∘ (map g ∘ join))
∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f) rewrite (natural (ϕ := @join T _)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ dist T G2 ∘ (join ∘ map g))
∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ dist T G2 ∘ join ∘ map g) ∘ dist T G1
∘ map f = map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f) reassociate -> near join.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map join ∘ (dist T G2 ∘ join) ∘ map g)
∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (trvmon_join (T := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map join ∘ (map join ∘ dist T G2 ∘ map (dist T G2))
   ∘ map g) ∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map join ∘ (map join ∘ dist T G2) ∘ map (dist T G2)
   ∘ map g) ∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map join ∘ map join ∘ dist T G2 ∘ map (dist T G2)
   ∘ map g) ∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (fun_map_map (F := G2)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ join) ∘ dist T G2 ∘ map (dist T G2)
   ∘ map g) ∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (mon_join_join (T := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2)
   ∘ map g) ∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite <- (fun_map_map (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2))
∘ map (map g) ∘ dist T G1 ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate -> near (dist T G1).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2))
∘ (map (map g) ∘ dist T G1) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      change (map (map (F := T ∘ T) g) ∘ dist T G1)
        with (map (F := G1 ∘ T) (map (F := T) g) ∘ dist T G1).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2))
∘ (map (map g) ∘ dist T G1) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      #[local] Set Keyed Unification.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2))
∘ (map (map g) ∘ dist T G1) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (natural (ϕ := @dist T _ G1 _ _ _)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2))
∘ (dist T G1 ∘ map (map g)) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      #[local] Unset Keyed Unification.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2))
∘ (dist T G1 ∘ map (map g)) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map
  (map (join ∘ map join) ∘ dist T G2 ∘ map (dist T G2))
∘ dist T G1 ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f) rewrite <- (fun_map_map (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join) ∘ dist T G2)
∘ map (map (dist T G2)) ∘ dist T G1 ∘ map (map g)
∘ map f = map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate -> near (dist T G1).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join) ∘ dist T G2)
∘ (map (map (dist T G2)) ∘ dist T G1) ∘ map (map g)
∘ map f = map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      (* unfold_ops @Dist_compose. *)
      rewrite <- (fun_map_map (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ (map (map (dist T G2)) ∘ dist T G1) ∘ map (map g)
∘ map f = map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ map (map (dist T G2)) ∘ dist T G1 ∘ map (map g)
∘ map f = map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f) reassociate -> near (dist T G1).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ (map (map (dist T G2)) ∘ dist T G1) ∘ map (map g)
∘ map f = map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      change (map (F := G1) (map (dist (A:=?A) T G2)))
        with (map (F := G1 ∘ T) (dist (A:=A) T G2)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ (map (dist T G2) ∘ dist T G1) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      (* reassociate -> near (dist T G1). *)
      #[local] Set Keyed Unification.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ (map (dist T G2) ∘ dist T G1) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (natural (ϕ := @dist T _ G1 _ _ _)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ (dist T G1 ∘ map (dist T G2)) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      #[local] Unset Keyed Unification.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ (dist T G1 ∘ map (dist T G2)) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      repeat reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ map (dist T G2)
∘ dist T G1 ∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f) reassociate -> near (dist T G1).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join))
∘ (map (dist T G2) ∘ dist T G1) ∘ map (dist T G2)
∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite <- (dist_linear (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (map (join ∘ map join)) ∘ dist T (G1 ∘ G2)
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      change (map (F := G1) (map (F := G2) ?f)) with
        (map (F := G1 ∘ G2) f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map (join ∘ map join) ∘ dist T (G1 ∘ G2)
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite <- (fun_map_map (F := G1 ∘ G2)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ map (map join) ∘ dist T (G1 ∘ G2)
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate -> near (dist T (G1 ∘ G2)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ (map (map join) ∘ dist T (G1 ∘ G2))
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      change (map (F := G1 ∘ G2) (map (F := T) ?f)) with
        (map (F :=(G1 ∘ G2) ∘ T) f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ (map join ∘ dist T (G1 ∘ G2))
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      #[local] Set Keyed Unification.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ (map join ∘ dist T (G1 ∘ G2))
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (natural (ϕ := @dist T _ (G1 ∘ G2) _ _ _)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ (dist T (G1 ∘ G2) ∘ map join)
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2) ∘ map join
∘ map (dist T G2) ∘ map (map g) ∘ map f =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f) reassociate -> near (map f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2) ∘ map join
∘ map (dist T G2) ∘ (map (map g) ∘ map f) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2) ∘ map join
∘ map (dist T G2) ∘ map (map (map g) ∘ f) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate -> near (map (map (map g) ∘ f)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2) ∘ map join
∘ (map (dist T G2) ∘ map (map (map g) ∘ f)) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2) ∘ map join
∘ map (map (dist T G2) ∘ (map (map g) ∘ f)) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate ->.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2)
∘ (map join
   ∘ map (map (dist T G2) ∘ (map (map g) ∘ f))) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate ->.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join
∘ (dist T (G1 ∘ G2)
   ∘ (map join
      ∘ map (map (dist T G2) ∘ (map (map g) ∘ f)))) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join
∘ (dist T (G1 ∘ G2)
   ∘ map
       (map join
        ∘ (map (dist T G2) ∘ (map (map g) ∘ f)))) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2)
∘ map
    (map join ∘ (map (dist T G2) ∘ (map (map g) ∘ f))) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2)
∘ map (map join ∘ map (dist T G2) ∘ (map (map g) ∘ f)) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (fun_map_map (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2)
∘ map (map (map join ∘ dist T G2) ∘ (map (map g) ∘ f)) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reassociate <-.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2)
∘ map (map (map join ∘ dist T G2) ∘ map (map g) ∘ f) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      rewrite (fun_map_map (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2)
∘ map (map (map join ∘ dist T G2 ∘ map g) ∘ f) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      #[local] Unset Keyed Unification.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B, C: Type
g: B -> G2 (T C)
f: A -> G1 (T B)
map join ∘ dist T (G1 ∘ G2)
∘ map (map (map join ∘ dist T G2 ∘ map g) ∘ f) =
map join ∘ dist T (G1 ∘ G2) ∘ map (g ⋆6 f)
      reflexivity.
    Qed.

    (** *** Unit law *)
    (******************************************************************)
    Lemma ktm_bindt0_T: forall
        (G1: Type -> Type) `{Map G1} `{Pure G1} `{Mult G1}
        `{! Applicative G1}
        (A B: Type) (f: A -> G1 (T B)),
        bindt f ∘ ret = f.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall (G1 : Type -> Type) (H4 : Map G1)
  (H5 : Pure G1) (H6 : Mult G1),
Applicative G1 ->
forall (A B : Type) (f : A -> G1 (T B)),
bindt f ∘ ret = f
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall (G1 : Type -> Type) (H4 : Map G1)
  (H5 : Pure G1) (H6 : Mult G1),
Applicative G1 ->
forall (A B : Type) (f : A -> G1 (T B)),
bindt f ∘ ret = f
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
bindt f ∘ ret = f unfold_ops @Bindt_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map join ∘ dist T G1 ∘ map f ∘ ret = f
      reassociate -> on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map join ∘ dist T G1 ∘ (map f ∘ ret) = f
      rewrite (natural (Natural := Monad.mon_ret_natural)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map join ∘ dist T G1 ∘ (ret ∘ map f) = f
      unfold_ops @Map_I.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map join ∘ dist T G1 ∘ (ret ∘ f) = f
      reassociate <-; reassociate -> near ret.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map join ∘ (dist T G1 ∘ ret) ∘ f = f
      rewrite (trvmon_ret (T := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map join ∘ map ret ∘ f = f
      rewrite (fun_map_map (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map (join ∘ ret) ∘ f = f
      rewrite (mon_join_ret (T := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
map id ∘ f = f
      rewrite (fun_map_id (F := G1)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
H4: Map G1
H5: Pure G1
H6: Mult G1
Applicative0: Applicative G1
A, B: Type
f: A -> G1 (T B)
id ∘ f = f
      reflexivity.
    Qed.

    (** *** Morphism law *)
    (******************************************************************)
    Lemma ktm_morph_T: forall `{ApplicativeMorphism G1 G2 ϕ},
      forall (A B: Type) (f: A -> G1 (T B)),
        ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall (G1 G2 : Type -> Type) (H4 : Map G1)
  (H5 : Mult G1) (H6 : Pure G1) (H7 : Map G2)
  (H8 : Mult G2) (H9 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 (T B)),
ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f)
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
forall (G1 G2 : Type -> Type) (H4 : Map G1)
  (H5 : Mult G1) (H6 : Pure G1) (H7 : Map G2)
  (H8 : Mult G2) (H9 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : A -> G1 (T B)),
ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f)
      introv morph.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
forall (A B : Type) (f : A -> G1 (T B)),
ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f) intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
ϕ (T B) ∘ bindt f = bindt (ϕ (T B) ∘ f)
      unfold_ops @Bindt_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
ϕ (T B) ∘ (map join ∘ dist T G1 ∘ map f) =
map join ∘ dist T G2 ∘ map (ϕ (T B) ∘ f)
      do 2 reassociate <- on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
ϕ (T B) ∘ map join ∘ dist T G1 ∘ map f =
map join ∘ dist T G2 ∘ map (ϕ (T B) ∘ f)
      unfold compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
(fun a : T A =>
 ϕ (T B) (map join (dist T G1 (map f a)))) =
(fun a : T A =>
 map join (dist T G2 (map (ϕ (T B) ○ f) a))) ext a.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
ϕ (T B) (map join (dist T G1 (map f a))) =
map join (dist T G2 (map (ϕ (T B) ○ f) a))
      rewrite (appmor_natural _ (T B) join).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
map join (ϕ ((T ∘ T) B) (dist T G1 (map f a))) =
map join (dist T G2 (map (ϕ (T B) ○ f) a))
      unfold compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
map join (ϕ (T (T B)) (dist T G1 (map f a))) =
map join (dist T G2 (map (ϕ (T B) ○ f) a)) compose near (map f a).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
map join ((ϕ (T (T B)) ∘ dist T G1) (map f a)) =
map join (dist T G2 (map (ϕ (T B) ○ f) a))
      rewrite <- (dist_morph (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
map join ((dist T G2 ∘ map (ϕ (T B))) (map f a)) =
map join (dist T G2 (map (ϕ (T B) ○ f) a))
      unfold compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
map join (dist T G2 (map (ϕ (T B)) (map f a))) =
map join (dist T G2 (map (ϕ (T B) ○ f) a)) compose near a on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
map join (dist T G2 ((map (ϕ (T B)) ∘ map f) a)) =
map join (dist T G2 (map (ϕ (T B) ○ f) a))
      rewrite (fun_map_map (F := T)).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1, G2: Type -> Type
H4: Map G1
H5: Mult G1
H6: Pure G1
H7: Map G2
H8: Mult G2
H9: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: A -> G1 (T B)
a: T A
map join (dist T G2 (map (ϕ (T B) ∘ f) a)) =
map join (dist T G2 (map (ϕ (T B) ○ f) a))
      reflexivity.
    Qed.

    (** *** Purity law *)
    (******************************************************************)
    Theorem bindt_purity_T
      `{Applicative G1} `{Applicative G2}:
      forall (A B: Type) (f: A -> G1 (T B)),
        bindt (G := G2 ∘ G1) (pure (F := G2) ∘ f) =
          pure (F := G2) ∘ bindt f.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
forall (A B : Type) (f : A -> G1 (T B)),
bindt (pure ∘ f) = pure ∘ bindt f
    Proof.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
forall (A B : Type) (f : A -> G1 (T B)),
bindt (pure ∘ f) = pure ∘ bindt f
      intros.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
bindt (pure ∘ f) = pure ∘ bindt f unfold_ops @Bindt_Categorical.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
map join ∘ dist T (G2 ∘ G1) ∘ map (pure ∘ f) =
pure ∘ (map join ∘ dist T G1 ∘ map f)
      reassociate -> on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
map join ∘ (dist T (G2 ∘ G1) ∘ map (pure ∘ f)) =
pure ∘ (map join ∘ dist T G1 ∘ map f)
      rewrite (map_purity_2 (T := T) (G2 := G2) f).
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
map join ∘ (pure ∘ dist T G1 ∘ map f) =
pure ∘ (map join ∘ dist T G1 ∘ map f)
      do 2 reassociate <- on left.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
map join ∘ pure ∘ dist T G1 ∘ map f =
pure ∘ (map join ∘ dist T G1 ∘ map f)
      do 2 reassociate <- on right.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
map join ∘ pure ∘ dist T G1 ∘ map f =
pure ∘ map join ∘ dist T G1 ∘ map f
      do 2 fequal.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
map join ∘ pure = pure ∘ map join
      unfold_ops @Map_compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
map (map join) ∘ pure = pure ∘ map join
      ext t; unfold compose.
T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: Categorical.TraversableMonad.TraversableMonad T
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H4: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H5: Applicative G2
A, B: Type
f: A -> G1 (T B)
t: G1 (T (T B))
map (map join) (pure t) = pure (map join t)
      now rewrite app_pure_natural.
    Qed.

    (** ** Typeclass Instances *)
    (******************************************************************)
    #[export] Instance TravMon_ToKleisli:
      Kleisli.TraversableMonad.TraversableRightPreModule T T :=
      {|ktm_bindt1 := @ktm_bindt1_T;
        ktm_bindt2 := @ktm_bindt2_T;
        ktm_morph := @ktm_morph_T;
      |}.

    #[export] Instance:
      Kleisli.TraversableMonad.TraversableMonad T :=
      {| ktm_bindt0 := @ktm_bindt0_T;
      |}.

  End with_monad.

End DerivedInstances.