From Tealeaves Require Import
  Classes.Functor2
  Classes.Categorical.Comonad
  Functors.Reader
  Functors.List
  Functors.List_Telescoping_General.

Definition L: Type → Type → Type :=
  fun B A ⇒ list B × A.

Definition cojoin_L {B A: Type}:
    L B A → L (L B B) (L B A) :=
  fun '(ctx, a) ⇒ (decorate_prefix_list ctx, (ctx, a)).

Definition extract_L {B A: Type}:
    L B A → A :=
  fun '(ctx, a) ⇒ a.

Definition map_L {B1 A1 B2 A2: Type} (g: B1 → B2) (f: A1 → A2):
    L B1 A1 → L B2 A2 :=
  fun '(ctx, a) ⇒ (map g ctx, f a).

Definition cobind_L {B1 B2 A1 A2: Type}
  (ρ: Z B1 → B2)
  (σ: L B1 A1 → A2): L B1 A1 → L B2 A2 :=
  map_L ρ σ ∘ cojoin_L.

#[global] Arguments extract_L {B A}%type_scope _.
#[global] Arguments cojoin_L {B A}%type_scope _.
#[global] Arguments map_L {B1 A1 B2 A2}%type_scope g f.

#[export] Instance Extract_L: ∀ B, Extract (L B) :=
  fun B V ⇒ extract (W := prod (list B)).

#[export] Instance Map2_L: Map2 L := @map_L.

#[export] Instance Functor2_L: Functor2 L.
Proof.
  constructor; intros; ext t.
  - induction t; try auto.
    cbn. now rewrite fun_map_id.
  - induction t; try auto.
    cbn.
    compose near a on left.
    rewrite fun_map_map.
    reflexivity.
Qed.

From Tealeaves Require Import
  Classes.Categorical.TraversableFunctor2.

Import Applicative.Notations.

Definition dist2_L
  {B V: Type} {G}
  `{Map G} `{Mult G} `{Pure G}:
  L (G B) (G V) → G (L B V) :=
  fun '(x, y) ⇒ pure (@pair (list B) V) <⋆> dist list G x <⋆> y.

#[export] Instance Dist2_L: ApplicativeDist2 L.
Proof.
  intro G. intros.
  exact (dist2_L X).
Defined.