This file contains a formalization of distributive laws in the sense of Beck, i.e. a distribution of one monad over another with compatibility properties such that the composition of the two also forms a monad.

From Tealeaves Require Export
  Classes.Categorical.Monad
  Functors.Compose.

#[local] Generalizable Variables T U A B.
#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.
#[local] Arguments join T%function_scope {Join} {A}%type_scope _.
#[local] Arguments ret T%function_scope {Return} {A}%type_scope _.

(** * Beck Distribution Laws *)
(**********************************************************************)
Class BeckDistribution (U T: Type -> Type)
  := bdist: forall {A: Type}, U (T A) -> T (U A).

Arguments bdist U T%function_scope {BeckDistribution} {A}%type_scope _.

#[local] Notation "'δ'" := (bdist): tealeaves_scope.

Section BeckDistributiveLaw.

  Context
    (U T: Type -> Type)
    `{Monad U}
    `{Monad T}
    `{BeckDistribution U T}.

  Class BeckDistributiveLaw :=
    { bdist_monad_l: Monad T;
      bdist_monad_r: Monad U;
      bdist_natural :> Natural (@bdist U T _);
      bdist_join_l:
      `(bdist U T ∘ join U =
          map T (join U) ∘ bdist U T ∘ map U (bdist U T (A := A)));
      bdist_join_r:
      `(bdist U T ∘ map U (join T) =
          join T ∘ map T (bdist U T) ∘ bdist U T (A := T A));
      bdist_unit_l:
      `(bdist U T ∘ ret U (A := T A) = map T (ret U));
      bdist_unit_r:
      `(bdist U T ∘ map U (ret T) = ret T (A := U A));
    }.

End BeckDistributiveLaw.

(** * Beck Distributive Laws Induce a Composite Monad *)
(**********************************************************************)
Section BeckDistributivelaw_composite_monad.

  Context
    `{BeckDistributiveLaw U T}.

  Existing Instance bdist_monad_l.
  Existing Instance bdist_monad_r.

  #[export] Instance Ret_Beck: Return (T ∘ U) :=
    fun A => ret T ∘ ret U.

  (* we join <<T>> before <<U>> *)
  #[export] Instance Join_Beck: Join (T ∘ U) :=
    fun A => map T (join U) ∘ join T ∘ map T (bdist U T).

  Lemma slide_joins:
    `(map T (join U) ∘ join T (A := U (U A))
      = join T ∘ map (T ∘ T) (join U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
forall A : Type,
map T (join U) ∘ join T =
join T ∘ map (T ∘ T) (join U)
  Proof.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
forall A : Type,
map T (join U) ∘ join T =
join T ∘ map (T ∘ T) (join U)
    intros; now rewrite (natural (ϕ := @join T _)).
  Qed.

  Lemma Natural_ret_Beck: Natural (@ret (T ∘ U) _).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
Natural (@ret (T ∘ U) Ret_Beck)
  Proof.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
Natural (@ret (T ∘ U) Ret_Beck)
    constructor; try typeclasses eauto.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
forall (A B : Type) (f : A -> B),
map (T ∘ U) f ∘ ret (T ∘ U) =
ret (T ∘ U) ∘ map (fun A0 : Type => A0) f
    intros A B f.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map (T ∘ U) f ∘ ret (T ∘ U) =
ret (T ∘ U) ∘ map (fun A : Type => A) f unfold_ops @Map_compose @Ret_Beck.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map T (map U f) ∘ (ret T ∘ ret U) =
ret T ∘ ret U ∘ map (fun A : Type => A) f
    reassociate <- on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map T (map U f) ∘ ret T ∘ ret U =
ret T ∘ ret U ∘ map (fun A : Type => A) f
    unfold_compose_in_compose.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map T (map U f) ∘ ret T ∘ ret U =
ret T ∘ ret U ∘ map (fun A : Type => A) f
    rewrite (natural (G := T) (F := fun A => A)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
ret T ∘ map (fun A : Type => A) (map U f) ∘ ret U =
ret T ∘ ret U ∘ map (fun A : Type => A) f
    unfold_ops @Map_I.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
ret T ∘ map U f ∘ ret U = ret T ∘ ret U ∘ f reassociate -> on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
ret T ∘ (map U f ∘ ret U) = ret T ∘ ret U ∘ f
    now rewrite (natural (G := U) (F := fun A => A)).
  Qed.

  #[local] Set Keyed Unification.
  Lemma Natural_join_Beck: Natural (@join (T ∘ U) _).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
Natural (@join (T ∘ U) Join_Beck)
  Proof.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
Natural (@join (T ∘ U) Join_Beck)
    constructor; try typeclasses eauto.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
forall (A B : Type) (f : A -> B),
map (T ∘ U) f ∘ join (T ∘ U) =
join (T ∘ U) ∘ map (T ∘ U ∘ (T ∘ U)) f
    intros A B f.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map (T ∘ U) f ∘ join (T ∘ U) =
join (T ∘ U) ∘ map (T ∘ U ∘ (T ∘ U)) f
    unfold_ops @Map_compose @Join_Beck.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map T (map U f)
∘ (map T (join U) ∘ join T ∘ map T (δ U T)) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    change_left
      (map T (map U f) ∘ map T (join U) ∘ join T ∘ map T (bdist U T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map T (map U f) ∘ map T (join U) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
map T (map U f ∘ join U) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    rewrite (natural (G := T) (F := T ∘ T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T ∘ map (T ∘ T) (map U f ∘ join U)
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    rewrite (natural (G := U) (F := U ∘ U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T ∘ map (T ∘ T) (join U ∘ map (U ∘ U) f)
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    rewrite <- (fun_map_map (F := (T ∘ T))).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T
∘ (map (T ∘ T) (join U) ∘ map (T ∘ T) (map (U ∘ U) f))
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    unfold_ops @Map_compose.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T
∘ (map T (map T (join U))
   ∘ map T (map T (map U (map U f)))) ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    change_left
      ((join T ∘ map T (map T (join U))) ∘
         (map T (map T (map U (map U f))) ∘ map T (bdist U T))).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T ∘ map T (map T (join U))
∘ (map T (map T (map U (map U f))) ∘ map T (δ U T)) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T ∘ map T (map T (join U))
∘ map T (map T (map U (map U f)) ∘ δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    rewrite (natural (G := T ∘ U) (Natural := bdist_natural U T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T ∘ map T (map T (join U))
∘ map T (δ U T ∘ map (U ○ T) (map U f)) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    rewrite <- (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T ∘ map T (map T (join U))
∘ (map T (δ U T) ∘ map T (map (U ○ T) (map U f))) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    (* RHS *)
    rewrite (natural (G := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A, B: Type
f: A -> B
join T ∘ map T (map T (join U))
∘ (map T (δ U T) ∘ map T (map (U ○ T) (map U f))) =
join T ∘ map (T ∘ T) (join U) ∘ map T (δ U T)
∘ map (T ∘ U) (map (T ∘ U) f)
    reflexivity.
  Qed.
  #[local] Unset Keyed Unification.

  Lemma join_ret_Beck {A}:
    join (T ∘ U) ∘ ret (T ∘ U) = @id ((T ∘ U) A).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ ret (T ∘ U) = id
  Proof.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ ret (T ∘ U) = id
    intros.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ ret (T ∘ U) = id unfold_ops @Join_Beck @Ret_Beck.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map T (δ U T)
∘ (ret T ∘ ret U) = id
    reassociate ->.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (δ U T) ∘ (ret T ∘ ret U)) = id reassociate <- near (map T (bdist U T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (δ U T) ∘ ret T ∘ ret U) = id
    rewrite (natural (F := fun A => A)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (ret T ∘ map (fun A : Type => A) (δ U T) ∘ ret U) =
id unfold_ops @Map_I.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ (ret T ∘ δ U T ∘ ret U) = id
    repeat reassociate ->.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (join T ∘ (ret T ∘ (δ U T ∘ ret U))) =
id reassociate <- near (join T).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (join T ∘ ret T ∘ (δ U T ∘ ret U)) =
id
    rewrite (mon_join_ret).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (id ∘ (δ U T ∘ ret U)) = id
    unfold_compose_in_compose.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (id ∘ (δ U T ∘ ret U)) = id rewrite (bdist_unit_l U T).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (id ∘ map T (ret U)) = id
    change (id ∘ ?f) with f.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ map T (ret U) = id rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U ∘ ret U) = id
    rewrite (mon_join_ret (T := U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T id = id
    now rewrite (fun_map_id (F := T)).
  Qed.

  Lemma join_map_ret_Beck {A}:
    join (T ∘ U) ∘ map (T ∘ U) (ret (T ∘ U)) = @id (T (U A)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ map (T ∘ U) (ret (T ∘ U)) = id
  Proof.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ map (T ∘ U) (ret (T ∘ U)) = id
    intros.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ map (T ∘ U) (ret (T ∘ U)) = id unfold_ops @Join_Beck @Ret_Beck.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U) (ret T ∘ ret U) = id
    rewrite (natural (G := T)
               (Natural := mon_join_natural (T := T))).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map (T ∘ T) (join U) ∘ map T (δ U T)
∘ map (T ∘ U) (ret T ∘ ret U) = id
    unfold_ops @Map_compose.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map T (map T (join U)) ∘ map T (δ U T)
∘ map T (map U (ret T ∘ ret U)) = id
    do 2 reassociate ->.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ (map T (map T (join U))
   ∘ (map T (δ U T) ∘ map T (map U (ret T ∘ ret U)))) =
id
    #[local] Set Keyed Unification.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ (map T (map T (join U))
   ∘ (map T (δ U T) ∘ map T (map U (ret T ∘ ret U)))) =
id
    rewrite 2(fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T
    (map T (join U) ∘ (δ U T ∘ map U (ret T ∘ ret U))) =
id
    #[local] Unset Keyed Unification.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T
    (map T (join U) ∘ (δ U T ∘ map U (ret T ∘ ret U))) =
id
    rewrite <- (fun_map_map (F := U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T
    (map T (join U)
     ∘ (δ U T ∘ (map U (ret T) ∘ map U (ret U)))) = id
    reassociate <- near (bdist U T).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T
    (map T (join U)
     ∘ (δ U T ∘ map U (ret T) ∘ map U (ret U))) = id
    rewrite (bdist_unit_r U T).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T (map T (join U) ∘ (ret T ∘ map U (ret U))) =
id
    reassociate <-.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T (map T (join U) ∘ ret T ∘ map U (ret U)) = id rewrite (natural (G := T) (F := fun A => A)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T
    (ret T ∘ map (fun A : Type => A) (join U)
     ∘ map U (ret U)) = id
    unfold_ops @Map_I.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map T (ret T ∘ join U ∘ map U (ret U)) = id
    reassociate ->.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map T (ret T ∘ (join U ∘ map U (ret U))) = id rewrite (mon_join_map_ret (T := U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map T (ret T ∘ id) = id
    rewrite <-(fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ (map T (ret T) ∘ map T id) = id reassociate <-.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map T (ret T) ∘ map T id = id
    rewrite (mon_join_map_ret (T := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
id ∘ map T id = id
    now rewrite (fun_map_id (F := T)).
  Qed.

  Lemma join_join_Beck {A}:
    join (T ∘ U) ∘ join (T ∘ U) =
      join (T ∘ U) ∘ map (T ∘ U) (join (T ∘ U) (A:=A)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ join (T ∘ U) =
join (T ∘ U) ∘ map (T ∘ U) (join (T ∘ U))
  Proof.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ join (T ∘ U) =
join (T ∘ U) ∘ map (T ∘ U) (join (T ∘ U))
    intros.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join (T ∘ U) ∘ join (T ∘ U) =
join (T ∘ U) ∘ map (T ∘ U) (join (T ∘ U)) unfold_ops @Join_Beck @Ret_Beck.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map T (δ U T)
∘ (map T (join U) ∘ join T ∘ map T (δ U T)) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Pull one <<join U>> to the same side as the other *)
    repeat change (?x ∘ (?y ∘ ?z)) with (x ∘ y ∘ z).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map T (join U) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    change (?x ∘ map T (bdist U T) ∘ map T (join U) ∘ ?y)
      with (x ∘ (map T (bdist U T) ∘ map T (join U)) ∘ y).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (δ U T) ∘ map T (join U)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map T (δ U T ∘ join U)
∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (bdist_join_l U T).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T (map T (join U) ∘ δ U T ∘ map U (δ U T))
∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite <- (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (map T (join U) ∘ δ U T)
   ∘ map T (map U (δ U T))) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite <- (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (map T (join U)) ∘ map T (δ U T)
   ∘ map T (map U (δ U T))) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    repeat reassociate <- on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map T (map T (join U))
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Re-associate <<join U>> *)
    change (?x ∘ join T ∘ map T (map T (join U)) ∘ ?y)
      with (x ∘ (join T ∘ map (T ∘ T) (join U)) ∘ y).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (join T ∘ map (T ∘ T) (join U))
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite <- (natural (ϕ := @join T _ )).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (map T (join U) ∘ join T)
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    repeat reassociate <- on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ map T (join U) ∘ join T
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U ∘ join U) ∘ join T ∘ map T (δ U T)
∘ map T (map U (δ U T)) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (mon_join_join (T := U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U ∘ map U (join U)) ∘ join T
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite <- (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ map T (map U (join U)) ∘ join T
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    change (?x ∘ map T (map U (join U)) ∘ join T ∘ ?y)
      with (x ∘ (map T (map U (join U)) ∘ join T) ∘ y).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (map T (map U (join U)) ∘ join T)
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (natural (ϕ := @join T _ )).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U)
∘ (join T ∘ map (T ∘ T) (map U (join U)))
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    repeat reassociate <- on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map (T ∘ T) (map U (join U))
∘ map T (δ U T) ∘ map T (map U (δ U T)) ∘ join T
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Pull one <<join T>> to next to the other (past distributions) *)
    change
      (?x ∘ map (T ∘ T) (map U (join U)) ∘ map T (bdist U T) ∘ ?y)
      with
      (x ∘ (map T (map (T ∘ U) (join U)) ∘ map T (bdist U T)) ∘ y).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (map (T ∘ U) (join U)) ∘ map T (δ U T))
∘ map T (map U (δ U T)) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T (map (T ∘ U) (join U) ∘ δ U T)
∘ map T (map U (δ U T)) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    reassociate -> near (map T (map U (bdist U T))).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (map (T ∘ U) (join U) ∘ δ U T)
   ∘ map T (map U (δ U T))) ∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
∘ join T ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    change (?x ∘ map T (?etc) ∘ join T ∘ ?y)
      with (x ∘ (map T (etc) ∘ join T) ∘ y).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T
     (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
   ∘ join T) ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (natural (ϕ := @join T _ )) at 1.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (join T
   ∘ map (T ∘ T)
       (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T)))
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    reassociate <- on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ join T
∘ map (T ∘ T)
    (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Re-associate <<join T>> *)
    reassociate -> near (join T).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (join T ∘ join T)
∘ map (T ∘ T)
    (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (mon_join_join (T := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ (join T ∘ map T (join T))
∘ map (T ∘ T)
    (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    reassociate <-.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T ∘ map T (join T)
∘ map (T ∘ T)
    (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Unite everything under the top-level <<map T>> *)
    change (?x ∘ map T (join T) ∘ map (T ∘ T) (?etc) ∘ ?y)
      with (x ∘ (map T (join T) ∘ map T (map T etc)) ∘ y).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T (join T)
   ∘ map T
       (map T
          (map (T ∘ U) (join U) ∘ δ U T
           ∘ map U (δ U T)))) ∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T
    (join T
     ∘ map T
         (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T)))
∘ map T (δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    change (?x ∘ ?y ∘ ?z = ?etc) with (x ∘ (y ∘ z) = etc).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ (map T
     (join T
      ∘ map T
          (map (T ∘ U) (join U) ∘ δ U T
           ∘ map U (δ U T))) ∘ map T (δ U T)) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T
    (join T
     ∘ map T
         (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
     ∘ δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map (T ∘ U)
    (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Unite everything under the top-level <<map T>> on the RHS too *)
    change (map (T ∘ U) ?etc) with (map T (map U etc)) at 2.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T
    (join T
     ∘ map T
         (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
     ∘ δ U T) =
map T (join U) ∘ join T ∘ map T (δ U T)
∘ map T
    (map U (map T (join U) ∘ join T ∘ map T (δ U T)))
    reassociate -> on right.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T
    (join T
     ∘ map T
         (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
     ∘ δ U T) =
map T (join U) ∘ join T
∘ (map T (δ U T)
   ∘ map T
       (map U
          (map T (join U) ∘ join T ∘ map T (δ U T))))
    unfold_compose_in_compose.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T
    (join T
     ∘ map T
         (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
     ∘ δ U T) =
map T (join U) ∘ join T
∘ (map T (δ U T)
   ∘ map T
       (map U
          (map T (join U) ∘ join T ∘ map T (δ U T))))
    rewrite (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (join U) ∘ join T
∘ map T
    (join T
     ∘ map T
         (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
     ∘ δ U T) =
map T (join U) ∘ join T
∘ map T
    (δ U T
     ∘ map U (map T (join U) ∘ join T ∘ map T (δ U T)))
    (* Simplify remaining goal by cancelling out equals *)
    fequal.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T
  (join T
   ∘ map T
       (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
   ∘ δ U T) =
map T
  (δ U T
   ∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))) fequal.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ map T (map (T ∘ U) (join U) ∘ δ U T ∘ map U (δ U T))
∘ δ U T =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Move join over distributions *)
    repeat rewrite <- (fun_map_map (F := T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T
∘ (map T (map (T ∘ U) (join U)) ∘ map T (δ U T)
   ∘ map T (map U (δ U T))) ∘ δ U T =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    repeat reassociate <-.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map T (map (T ∘ U) (join U)) ∘ map T (δ U T)
∘ map T (map U (δ U T)) ∘ δ U T =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    change (map T (map (T ∘ U) (@join U _ ?A)))
      with (map (T ∘ T) (map U (@join U _ A))).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map (T ∘ T) (map U (join U)) ∘ map T (δ U T)
∘ map T (map U (δ U T)) ∘ δ U T =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    #[local] Set Keyed Unification.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
join T ∘ map (T ∘ T) (map U (join U)) ∘ map T (δ U T)
∘ map T (map U (δ U T)) ∘ δ U T =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite <- (natural (ϕ := @join T _ ) (map U (join U))).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ join T ∘ map T (δ U T)
∘ map T (map U (δ U T)) ∘ δ U T =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    reassociate -> near (map T (bdist U T)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ (join T ∘ map T (δ U T))
∘ map T (map U (δ U T)) ∘ δ U T =
δ U T
∘ map U (map T (join U) ∘ (join T ∘ map T (δ U T)))
    reassociate -> on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ (join T ∘ map T (δ U T))
∘ (map T (map U (δ U T)) ∘ δ U T) =
δ U T
∘ map U (map T (join U) ∘ (join T ∘ map T (δ U T)))
    change (map T (map U (@bdist U T _ ?A)))
      with (map (T ∘ U) (@bdist U T _ A)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ (join T ∘ map T (δ U T))
∘ (map (T ∘ U) (δ U T) ∘ δ U T) =
δ U T
∘ map U (map T (join U) ∘ (join T ∘ map T (δ U T)))
    rewrite (natural (ϕ := @bdist U T _ ) (bdist U T) (G := T ∘ U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ (join T ∘ map T (δ U T))
∘ (δ U T ∘ map (U ○ T) (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ (join T ∘ map T (δ U T)))
    #[local] Unset Keyed Unification.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ (join T ∘ map T (δ U T))
∘ (δ U T ∘ map (U ○ T) (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ (join T ∘ map T (δ U T)))
    unfold_ops @Map_compose.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ (join T ∘ map T (δ U T))
∘ (δ U T ∘ map U (map T (δ U T))) =
δ U T
∘ map U (map T (join U) ∘ (join T ∘ map T (δ U T)))
    do 3 reassociate <-.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ join T ∘ map T (δ U T)
∘ δ U T ∘ map U (map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    change (?x ∘ join T ∘ map T (bdist U T) ∘ bdist U T ∘ ?y)
      with (x ∘ (join T ∘ map T (bdist U T) ∘ bdist U T) ∘ y).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U))
∘ (join T ∘ map T (δ U T) ∘ δ U T)
∘ map U (map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite <- (bdist_join_r U T).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ (δ U T ∘ map U (join T))
∘ map U (map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    (* Make some final naturality pulls *)
    repeat reassociate <-.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map T (map U (join U)) ∘ δ U T ∘ map U (join T)
∘ map U (map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    change (map T (map U ?f)) with (map (T ∘ U) f).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
map (T ∘ U) (join U) ∘ δ U T ∘ map U (join T)
∘ map U (map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (natural (ϕ := @bdist U T _ )).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
δ U T ∘ map (U ○ T) (join U) ∘ map U (join T)
∘ map U (map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    unfold_ops @Map_compose.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
δ U T ∘ map U (map T (join U)) ∘ map U (join T)
∘ map U (map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    reassociate -> on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
δ U T ∘ map U (map T (join U))
∘ (map U (join T) ∘ map U (map T (δ U T))) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    rewrite (fun_map_map (F := U)).
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
δ U T ∘ map U (map T (join U))
∘ map U (join T ∘ map T (δ U T)) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    reassociate -> on left.
U, T: Type -> Type
H: Map U
H0: Return U
H1: Join U
H3: Map T
H4: Return T
H5: Join T
H7: BeckDistribution U T
H2: BeckDistributiveLaw U T
A: Type
δ U T
∘ (map U (map T (join U))
   ∘ map U (join T ∘ map T (δ U T))) =
δ U T
∘ map U (map T (join U) ∘ join T ∘ map T (δ U T))
    now rewrite (fun_map_map (F := U)).
  Qed.

  #[export, program] Instance Monad_Beck: Monad (T ∘ U) :=
    {| mon_ret_natural := Natural_ret_Beck;
       mon_join_natural := Natural_join_Beck;
       mon_join_ret := fun A => join_ret_Beck;
       mon_join_map_ret := fun A => join_map_ret_Beck;
       mon_join_join := fun A => join_join_Beck;
    |}.

End BeckDistributivelaw_composite_monad.