TraversableFunctor.v

From Tealeaves Require Import
  Classes.Categorical.TraversableFunctor.

#[local] Generalizable Variables T F U G X Y ϕ.

#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.

(** * Monoid Structure of Traversable Functors *)
(**********************************************************************)

(** ** The Identity Functor is Traversable *)
(**********************************************************************)
#[export] Instance Dist_I:
  ApplicativeDist (fun A => A) := fun F map mult pure A a => a.

#[export, program] Instance Traversable_I:
  TraversableFunctor (fun A => A).

Next Obligation.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
Natural
  (@dist (fun A : Type => A) Dist_I G Map_G Pure_G
     Mult_G)
  constructor; try typeclasses eauto.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
forall (A B : Type) (f : A -> B),
map (G ∘ (fun A0 : Type => A0)) f
∘ dist (fun A0 : Type => A0) G =
dist (fun A0 : Type => A0) G
∘ map ((fun A0 : Type => A0) ∘ G) f
  intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: A -> B
map (G ∘ (fun A : Type => A)) f
∘ dist (fun A : Type => A) G =
dist (fun A : Type => A) G
∘ map ((fun A : Type => A) ∘ G) f ext a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: A -> B
a: ((fun A : Type => A) ∘ G) A
(map (G ∘ (fun A : Type => A)) f
 ∘ dist (fun A : Type => A) G) a =
(dist (fun A : Type => A) G
 ∘ map ((fun A : Type => A) ∘ G) f) a unfold transparent tcs.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H1: Applicative G
A, B: Type
f: A -> B
a: ((fun A : Type => A) ∘ G) A
(map G f ∘ (fun a : G A => a)) a =
Map_compose (fun A : Type => A) G A B f a
  reflexivity.
Qed.

Next Obligation.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A: Type
dist (fun A : Type => A) (G1 ∘ G2) =
map G1 (dist (fun A : Type => A) G2)
∘ dist (fun A : Type => A) G1
  unfold transparent tcs.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A: Type
(fun a : (G1 ∘ G2) A => a) =
map G1 (fun a : G2 A => a) ∘ (fun a : G1 (G2 A) => a) ext a.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A: Type
a: (G1 ∘ G2) A
a =
(map G1 (fun a : G2 A => a) ∘ (fun a : G1 (G2 A) => a))
  a
  symmetry.G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H1: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H2: Applicative G2
A: Type
a: (G1 ∘ G2) A
(map G1 (fun a : G2 A => a) ∘ (fun a : G1 (G2 A) => a))
  a = a now rewrite (fun_map_id (F := G1)).
Qed.

(** ** Traversable Functors are Closed under Composition *)
(**********************************************************************)
Section TraversableFunctor_compose.

  Context
    `{TraversableFunctor T}
    `{TraversableFunctor U}.

  #[export] Instance Dist_compose: ApplicativeDist (T ∘ U) :=
    fun G Gmap mult pure A =>
      dist T G ∘ map T (dist U G (A := A)).

  Lemma dist_unit_compose: forall A,
      dist (T ∘ U) (fun A => A) = @id (T (U A)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall A : Type,
dist (T ∘ U) (fun A0 : Type => A0) = id
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall A : Type,
dist (T ∘ U) (fun A0 : Type => A0) = id
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
A: Type
dist (T ∘ U) (fun A : Type => A) = id unfold transparent tcs.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
A: Type
dist T (fun A : Type => A)
∘ map T (dist U (fun A : Type => A)) = id
    rewrite (dist_unit (F := T)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
A: Type
id ∘ map T (dist U (fun A : Type => A)) = id
    rewrite (dist_unit (F := U)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
A: Type
id ∘ map T id = id
    now rewrite (fun_map_id (F := T)).
  Qed.

  Lemma dist_natural_compose:
    forall `{Applicative G} `(f: X -> Y),
      map (G ∘ (T ∘ U)) f ∘ dist (T ∘ U) G =
        dist (T ∘ U) G ∘ map ((T ∘ U) ∘ G) f.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (X Y : Type) (f : X -> Y),
map (G ∘ (T ∘ U)) f ∘ dist (T ∘ U) G =
dist (T ∘ U) G ∘ map (T ∘ U ∘ G) f
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (X Y : Type) (f : X -> Y),
map (G ∘ (T ∘ U)) f ∘ dist (T ∘ U) G =
dist (T ∘ U) G ∘ map (T ∘ U ∘ G) f
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
map (G ∘ (T ∘ U)) f ∘ dist (T ∘ U) G =
dist (T ∘ U) G ∘ map (T ∘ U ∘ G) f unfold transparent tcs.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
map G (map T (map U f))
∘ (dist T G ∘ map T (dist U G)) =
dist T G ∘ map T (dist U G) ∘ map T (map U (map G f))
    change_left (map (G ∘ T) (map U f) ∘ dist T G ∘ map T (dist U G)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
map (G ∘ T) (map U f) ∘ dist T G ∘ map T (dist U G) =
dist T G ∘ map T (dist U G) ∘ map T (map U (map G f))
    #[local] Set Keyed Unification.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
map (G ∘ T) (map U f) ∘ dist T G ∘ map T (dist U G) =
dist T G ∘ map T (dist U G) ∘ map T (map U (map G f))
    rewrite (natural (ϕ := @dist T _ G _ _ _ ) (F := T ∘ G)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G ∘ map (T ∘ G) (map U f) ∘ map T (dist U G) =
dist T G ∘ map T (dist U G) ∘ map T (map U (map G f))
    #[local] Unset Keyed Unification.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G ∘ map (T ∘ G) (map U f) ∘ map T (dist U G) =
dist T G ∘ map T (dist U G) ∘ map T (map U (map G f))
    unfold_ops @Map_compose.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G ∘ map T (map G (map U f)) ∘ map T (dist U G) =
dist T G ∘ map T (dist U G) ∘ map T (map U (map G f))
    reassociate -> on left.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G
∘ (map T (map G (map U f)) ∘ map T (dist U G)) =
dist T G ∘ map T (dist U G) ∘ map T (map U (map G f))
    reassociate -> on right.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G
∘ (map T (map G (map U f)) ∘ map T (dist U G)) =
dist T G
∘ (map T (dist U G) ∘ map T (map U (map G f)))
    unfold_compose_in_compose.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G
∘ (map T (map G (map U f)) ∘ map T (dist U G)) =
dist T G
∘ (map T (dist U G) ∘ map T (map U (map G f)))
    rewrite (fun_map_map (F := T)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G ∘ map T (map G (map U f) ∘ dist U G) =
dist T G
∘ (map T (dist U G) ∘ map T (map U (map G f)))
    rewrite (fun_map_map (F := T)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G ∘ map T (map G (map U f) ∘ dist U G) =
dist T G ∘ map T (dist U G ∘ map U (map G f))
    change (map ?F (map ?G ?f)) with (map (F ∘ G) f).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
X, Y: Type
f: X -> Y
dist T G ∘ map T (map (G ∘ U) f ∘ dist U G) =
dist T G ∘ map T (dist U G ∘ map (U ∘ G) f)
    now rewrite <- (natural (ϕ := @dist U _ G _ _ _)).
  Qed.

  Instance dist_natural_compose_:
    forall `{Applicative G},
      Natural (@dist (T ∘ U) _ G _ _ _).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
Natural
  (@dist (T ∘ U) Dist_compose G Map_G Pure_G Mult_G)
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
Natural
  (@dist (T ∘ U) Dist_compose G Map_G Pure_G Mult_G)
    constructor; try typeclasses eauto.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
forall (A B : Type) (f : A -> B),
map (G ○ (T ∘ U)) f ∘ dist (T ∘ U) G =
dist (T ∘ U) G ∘ map (T ∘ U ○ G) f
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H5: Applicative G
A, B: Type
f: A -> B
map (G ○ (T ∘ U)) f ∘ dist (T ∘ U) G =
dist (T ∘ U) G ∘ map (T ∘ U ○ G) f apply dist_natural_compose.
  Qed.

  Lemma dist_morph_compose:
    forall `{ApplicativeMorphism G1 G2 ϕ} (A: Type),
      dist (T ∘ U) G2 ∘ map (T ∘ U) (ϕ A) =
        ϕ (T (U A)) ∘ dist (T ∘ U) G1.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall (G1 G2 : Type -> Type) (H5 : Map G1)
  (H6 : Mult G1) (H7 : Pure G1) (H8 : Map G2)
  (H9 : Mult G2) (H10 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist (T ∘ U) G2 ∘ map (T ∘ U) (ϕ A) =
ϕ (T (U A)) ∘ dist (T ∘ U) G1
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
forall (G1 G2 : Type -> Type) (H5 : Map G1)
  (H6 : Mult G1) (H7 : Pure G1) (H8 : Map G2)
  (H9 : Mult G2) (H10 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist (T ∘ U) G2 ∘ map (T ∘ U) (ϕ A) =
ϕ (T (U A)) ∘ dist (T ∘ U) G1
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist (T ∘ U) G2 ∘ map (T ∘ U) (ϕ A) =
ϕ (T (U A)) ∘ dist (T ∘ U) G1 unfold transparent tcs.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ map T (dist U G2) ∘ map T (map U (ϕ A)) =
ϕ (T (U A)) ∘ (dist T G1 ∘ map T (dist U G1))
    reassociate -> on left.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ (map T (dist U G2) ∘ map T (map U (ϕ A))) =
ϕ (T (U A)) ∘ (dist T G1 ∘ map T (dist U G1))
    unfold_compose_in_compose.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ (map T (dist U G2) ∘ map T (map U (ϕ A))) =
ϕ (T (U A)) ∘ (dist T G1 ∘ map T (dist U G1))
    rewrite (fun_map_map (F := T)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ map T (dist U G2 ∘ map U (ϕ A)) =
ϕ (T (U A)) ∘ (dist T G1 ∘ map T (dist U G1))
    rewrite (dist_morph (F := U)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ map T (ϕ (U A) ∘ dist U G1) =
ϕ (T (U A)) ∘ (dist T G1 ∘ map T (dist U G1))
    rewrite <- (fun_map_map (F := T)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ (map T (ϕ (U A)) ∘ map T (dist U G1)) =
ϕ (T (U A)) ∘ (dist T G1 ∘ map T (dist U G1))
    reassociate <- on left.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1, G2: Type -> Type
H5: Map G1
H6: Mult G1
H7: Pure G1
H8: Map G2
H9: Mult G2
H10: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H11: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ map T (ϕ (U A)) ∘ map T (dist U G1) =
ϕ (T (U A)) ∘ (dist T G1 ∘ map T (dist U G1))
    now rewrite (dist_morph (F := T)).
  Qed.

  Lemma dist_linear_compose:
    forall `{Applicative G1} `{Applicative G2} (A: Type),
      dist (T ∘ U) (G1 ∘ G2) =
        map G1 (dist (T ∘ U) G2) ∘ dist (T ∘ U) G1 (A := G2 A).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
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 : Type,
dist (T ∘ U) (G1 ∘ G2) =
map G1 (dist (T ∘ U) G2) ∘ dist (T ∘ U) G1
  Proof.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
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 : Type,
dist (T ∘ U) (G1 ∘ G2) =
map G1 (dist (T ∘ U) G2) ∘ dist (T ∘ U) G1
    intros.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist (T ∘ U) (G1 ∘ G2) =
map G1 (dist (T ∘ U) G2) ∘ dist (T ∘ U) G1 unfold transparent tcs.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2 ∘ map T (dist U G2))
∘ (dist T G1 ∘ map T (dist U G1))
    rewrite <- (fun_map_map (F := G1)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2) ∘ map G1 (map T (dist U G2))
∘ (dist T G1 ∘ map T (dist U G1))
    reassociate -> on right;
      change (map ?F (map ?G ?f)) with (map (F ∘ G) f);
      reassociate <- near (map (G1 ∘ T) (dist U G2)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2)
∘ (map (G1 ∘ T) (dist U G2) ∘ dist T G1
   ∘ map T (dist U G1))
    #[local] Set Keyed Unification.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2)
∘ (map (G1 ∘ T) (dist U G2) ∘ dist T G1
   ∘ map T (dist U G1))
    rewrite (natural (ϕ := @dist T _ G1 _ _ _)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2)
∘ (dist T G1 ∘ map (T ○ G1) (dist U G2)
   ∘ map T (dist U G1))
    #[local] Unset Keyed Unification.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2)
∘ (dist T G1 ∘ map (T ○ G1) (dist U G2)
   ∘ map T (dist U G1))
    reassociate -> on right;
      unfold_ops @Map_compose;
      rewrite (fun_map_map (F := T)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2)
∘ (dist T G1 ∘ map T (map G1 (dist U G2) ∘ dist U G1))
    #[local] Set Keyed Unification.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2) ∘ map T (dist U (G1 ∘ G2)) =
map G1 (dist T G2)
∘ (dist T G1 ∘ map T (map G1 (dist U G2) ∘ dist U G1))
    rewrite (dist_linear (F := U)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
dist T (G1 ∘ G2)
∘ map T (map G1 (dist U G2) ∘ dist U G1) =
map G1 (dist T G2)
∘ (dist T G1 ∘ map T (map G1 (dist U G2) ∘ dist U G1))
    rewrite (dist_linear (F := T)).T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
map G1 (dist T G2) ∘ dist T G1
∘ map T (map G1 (dist U G2) ∘ dist U G1) =
map G1 (dist T G2)
∘ (dist T G1 ∘ map T (map G1 (dist U G2) ∘ dist U G1))
    #[local] Unset Keyed Unification.T: Type -> Type
H: Map T
H0: ApplicativeDist T
H1: TraversableFunctor T
U: Type -> Type
H2: Map U
H3: ApplicativeDist U
H4: TraversableFunctor U
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H5: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H6: Applicative G2
A: Type
map G1 (dist T G2) ∘ dist T G1
∘ map T (map G1 (dist U G2) ∘ dist U G1) =
map G1 (dist T G2)
∘ (dist T G1 ∘ map T (map G1 (dist U G2) ∘ dist U G1))
    reflexivity.
  Qed.

  #[export] Instance Traversable_compose: TraversableFunctor (T ∘ U) :=
    {| dist_morph := @dist_morph_compose;
       dist_unit := @dist_unit_compose;
       dist_linear := @dist_linear_compose;
    |}.

End TraversableFunctor_compose.

From Tealeaves Require Import
  Classes.Categorical.TraversableMonad.

(** * Monad Operations as Homomorphisms between Traversable Functors *)
(**********************************************************************)
Section traverable_monad_theory.

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

  Lemma dist_ret_spec:
    TraversableMorphism (fun A => A) T (@ret T _).T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
TraversableMorphism (fun A : Type => A) T (@ret T H0)
  Proof.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
TraversableMorphism (fun A : Type => A) T (@ret T H0)
    constructor; try typeclasses eauto.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
map G ret ∘ dist (fun A0 : Type => A0) G =
dist T G ∘ ret
    intros.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H4: Applicative G
A: Type
map G ret ∘ dist (fun A : Type => A) G =
dist T G ∘ ret now rewrite (trvmon_ret).
  Qed.

  Lemma dist_join_spec:
      TraversableMorphism (T ∘ T) T (@join T _).T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
TraversableMorphism (T ∘ T) T (@join T H1)
  Proof.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
TraversableMorphism (T ∘ T) T (@join T H1)
    constructor; try typeclasses eauto.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
map G join ∘ dist (T ∘ T) G = dist T G ∘ join
    intros.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H4: Applicative G
A: Type
map G join ∘ dist (T ∘ T) G = dist T G ∘ join unfold_ops @Dist_compose.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H4: Applicative G
A: Type
map G join ∘ (dist T G ∘ map T (dist T G)) =
dist T G ∘ join
    reassociate <- on left.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H4: Applicative G
A: Type
map G join ∘ dist T G ∘ map T (dist T G) =
dist T G ∘ join
    unfold_compose_in_compose.T: Type -> Type
H: Map T
H0: Return T
H1: Join T
H2: ApplicativeDist T
H3: TraversableMonad T
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H4: Applicative G
A: Type
map G join ∘ dist T G ∘ map T (dist T G) =
dist T G ∘ join
    now rewrite <- (trvmon_join (T := T) (G := G)).
  Qed.

End traverable_monad_theory.