Tealeaves.Functors.Early.Batch

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

Import Applicative.Notations.
Import TraversableFunctor.Notations.

#[local] Generalizable Variables ψ ϕ W F G M A B C D X Y O.

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

The Batch Functor

Inductive Batch (A B C: Type): Type :=
| Done: C → Batch A B C
| Step: Batch A B (B → C) → A → Batch A B C.

#[global] Arguments Done {A B C}%type_scope _.
#[global] Arguments Step {A B C}%type_scope _ _.

#[local] Arguments Done: clear implicits.
#[local] Arguments Step: clear implicits.

#[local] Infix "⧆" :=
  (Step _ _ _) (at level 51, left associativity): tealeaves_scope.

#[global] Notation "'BATCH1' B C" :=
  (fun A ⇒ Batch A B C) (at level 0, B at level 0, C at level 0).
#[global] Notation "'BATCH2' A C" :=
  (fun B ⇒ Batch A B C) (at level 3).

Map Operations

Fixpoint map_Batch
  {A B: Type} (C1 C2: Type) (f: C1 → C2)
  (b: Batch A B C1): Batch A B C2 :=
  match b with
  | Done _ _ _ c ⇒
      Done A B C2 (f c)
  | Step _ _ _ rest a ⇒
      Step A B C2 (@map_Batch A B (B → C1) (B → C2) (compose f) rest) a
  end.

#[export] Instance Map_Batch {A B: Type}:
  Map (Batch A B) := @map_Batch A B.

Fixpoint mapfst_Batch
  {B C: Type} (A1 A2: Type) (f: A1 → A2)
  (b: Batch A1 B C): Batch A2 B C :=
  match b with
  | Done _ _ _ c ⇒ Done A2 B C c
  | Step _ _ _ rest a ⇒
      Step A2 B C (mapfst_Batch A1 A2 f rest) (f a)
  end.

#[export] Instance Map_Batch1 {B C: Type}:
  Map (BATCH1 B C) := @mapfst_Batch B C.

Fixpoint mapsnd_Batch
  {A: Type} (B1 B2: Type) {C: Type}
  (f: B1 → B2) (b: Batch A B2 C): Batch A B1 C :=
  match b with
  | Done _ _ _ c ⇒ Done A B1 C c
  | Step _ _ _ rest c ⇒
      Step A B1 C
        (map (Batch A B1) (precompose f)
           (mapsnd_Batch B1 B2 f rest)) c
  end.

Rewriting Principles

Lemma map_Batch_rw1 {A B C1 C2: Type} `(f: C1 → C2) (c: C1):
  map (Batch A B) f (Done A B C1 c) = Done A B C2 (f c).
Proof.
  reflexivity.
Qed.

Lemma map_Batch_rw2 {A B C1 C2: Type}
  `(f: C1 → C2) (a: A) (rest: Batch A B (B → C1)):
  map (Batch A B) f (rest ⧆ a) = map (Batch A B) (compose f) rest ⧆ a.
Proof.
  reflexivity.
Qed.

Lemma mapfst_Batch_rw1 {A1 A2 B C: Type} `(f: A1 → A2) (c: C):
  mapfst_Batch A1 A2 f (Done A1 B C c) = Done A2 B C c.
Proof.
  reflexivity.
Qed.

Lemma mapfst_Batch_rw2 {A1 A2 B C: Type}
  (f: A1 → A2) (a: A1) (b: Batch A1 B (B → C)):
  mapfst_Batch A1 A2 f (b ⧆ a) = mapfst_Batch A1 A2 f b ⧆ f a.
Proof.
  reflexivity.
Qed.

Lemma mapsnd_Batch_rw1 {A B B' C: Type} `(f: B' → B) (c: C):
  mapsnd_Batch B' B f (Done A B C c) = Done A B' C c.
Proof.
  reflexivity.
Qed.

Lemma mapsnd_Batch_rw2 {A B B' C: Type} `(f: B → B')
  (a: A) (b: Batch A B' (B' → C)):
  mapsnd_Batch B B' f (b ⧆ a) =
    map (Batch A B) (precompose f) (mapsnd_Batch B B' f b) ⧆ a.
Proof.
  reflexivity.
Qed.

Functor Laws

Section functoriality.

In the A Argument

  Lemma mapfst_id_Batch: ∀ (B C A: Type),
      mapfst_Batch A A (@id A) = @id (Batch A B C).
  Proof.
    intros. ext b. induction b as [C c|C rest IHrest a].
    - reflexivity.
    - cbn. rewrite IHrest. reflexivity.
  Qed.

  Lemma mapfst_mapfst_Batch:
    ∀ (B C A1 A2 A3: Type) (f: A1 → A2) (g: A2 → A3),
      mapfst_Batch _ _ g ∘ mapfst_Batch _ _ f =
        mapfst_Batch (B := B) (C := C) _ _ (g ∘ f).
  Proof.
    intros.
    ext b. unfold compose. induction b as [C c|C rest IHrest a].
    - reflexivity.
    - cbn. fequal.
      apply IHrest.
  Qed.

  #[export, program] Instance Functor_Batch1 {B C: Type}:
    Functor (BATCH1 B C) :=
    {| fun_map_id := @mapfst_id_Batch B C;
       fun_map_map := @mapfst_mapfst_Batch B C;
    |}.

In the C Argument

  Lemma map_id_Batch: ∀ (A B C: Type),
      map (Batch A B) (@id C) = @id (Batch A B C).
  Proof.
    intros. ext b. induction b as [C c|C rest IHrest a].
    - reflexivity.
    - cbn.
      assert (lemma: compose (@id C) = @id (B → C)).
      { reflexivity. } rewrite lemma.
      now rewrite IHrest.
  Qed.

  Lemma map_map_Batch:
    ∀ (A B C1 C2 C3: Type) (f: C1 → C2) (g: C2 → C3),
      map (Batch A B) g ∘ map (Batch A B) f = map (Batch A B) (g ∘ f).
  Proof.
    intros.
    ext b. unfold compose.
    generalize dependent C3.
    generalize dependent C2.
    induction b; intros.
    - reflexivity.
    - cbn. fequal.
      specialize (IHb (B → C2) (compose f)
                    (B → C3) (compose g)).
      rewrite IHb.
      reflexivity.
  Qed.

  #[export, program] Instance Functor_Batch {A B: Type}:
    Functor (Batch A B) :=
    {| fun_map_id := @map_id_Batch A B;
       fun_map_map := @map_map_Batch A B;
    |}.

Commuting Independent maps

  Lemma mapfst_map_Batch
    {B: Type} `(f: A1 → A2) `(g: C1 → C2) (b: Batch A1 B C1):
    mapfst_Batch A1 A2 f (map (Batch A1 B) g b) =
      map (Batch A2 B) g (mapfst_Batch A1 A2 f b).
  Proof.
    generalize dependent C2.
    generalize dependent B.
    induction b.
    - reflexivity.
    - intros.
      cbn. fequal.
      specialize (IHb (B → C2) (compose g)).
      rewrite IHb.
      reflexivity.
  Qed.

  Lemma mapsnd_map_Batch
    {A: Type} `(f: B1 → B2) `(g: C1 → C2) (b: Batch A B2 C1):
    mapsnd_Batch B1 B2 f (map (Batch A B2) g b) =
      map (Batch A B1) g (mapsnd_Batch B1 B2 f b).
  Proof.
    generalize dependent C2.
    induction b.
    - reflexivity.
    - intros. cbn. fequal.
      rewrite IHb.
      compose near (mapsnd_Batch _ _ f b).
      do 2 rewrite (fun_map_map (F := Batch A B1)).
      do 2 rewrite <- IHb.
      reflexivity.
  Qed.

  Lemma mapfst_mapsnd_Batch:
    ∀ {C: Type} `(f: A1 → A2) `(g: B1 → B2) (b: Batch A1 B2 C),
      mapfst_Batch A1 A2 f (mapsnd_Batch B1 B2 g b) =
        mapsnd_Batch B1 B2 g (mapfst_Batch A1 A2 f b).
  Proof.
    intros.
    generalize dependent f.
    generalize dependent g.
    induction b.
    - reflexivity.
    - intros. cbn. fequal. rewrite mapfst_map_Batch.
      now rewrite IHb.
  Qed.

Functoriality In the B Argument

  Lemma mapsnd_id_Batch: ∀ (A C B: Type),
      mapsnd_Batch B B (@id B) = @id (Batch A B C).
  Proof.
    intros. ext b. induction b as [C c|C rest IHrest a].
    - reflexivity.
    - cbn. rewrite IHrest.
      change (@precompose B B C (@id B)) with (@id (B → C)).
      unfold id.
      rewrite fun_map_id.
      reflexivity.
  Qed.

  Lemma mapsnd_mapsnd_Batch:
    ∀ (A C B1 B2 B3: Type) (f: B1 → B2) (g: B2 → B3),
      mapsnd_Batch _ _ f ∘ mapsnd_Batch _ _ g =
        mapsnd_Batch (A := A) (C := C) _ _ (g ∘ f).
  Proof.
    intros.
    ext b. unfold compose. induction b as [C c|C rest IHrest a].
    - reflexivity.
    - cbn. fequal.
      rewrite mapsnd_map_Batch.
      rewrite IHrest.
      compose near (mapsnd_Batch B1 B3 (g ○ f) rest) on left.
      rewrite map_map_Batch.
      rewrite precompose_precompose.
      reflexivity.
  Qed.

  (* There is no contravariant functor typeclass to instantiate *)

End functoriality.

Applicative Functor Instance

Section Applicative_Batch.

  Context
    {A B: Type}.

Operations

  #[export] Instance Pure_Batch: Pure (@Batch A B) :=
    fun (C: Type) (c: C) ⇒ Done A B C c.

  Fixpoint mult_Batch `(b1: Batch A B C) `(b2: Batch A B D):
    @Batch A B (C × D) :=
    match b2 with
    | Done _ _ _ d ⇒ map (Batch A B) (fun (c: C) ⇒ (c, d)) b1
    | Step _ _ _ rest a ⇒
        Step A B (C × D)
          (map (Batch A B) strength_arrow (mult_Batch b1 rest)) a
    end.

  #[export] Instance Mult_Batch: Mult (@Batch A B) :=
    fun C D '(b1, b2) ⇒ mult_Batch b1 b2.

Examples of operations

  (*
    Section demo.
    Context
    (A B C D: Type)
    (a1 a2 a3: A)
    (c1 c2 c3: C)
    (d1 d2 d3: D)
    (mk1: B -> C)
    (mk1': B -> D)
    (mk2: B -> B -> C).

    Compute Done A B C c1 ⊗ Done A B D d1.
    Compute Done A B C c1 ⊗ (Done A B (B -> D) mk1' ⧆ a1).
    Compute (Done A B _ mk1 ⧆ a1) ⊗ Done A B D d2.
    Compute (Done A B _ mk1 ⧆ a1) ⊗ (Done A B _ mk1' ⧆ a2).
    Compute (Done A B _ mk2 ⧆ a1 ⧆ a2) ⊗ (Done A B _ mk1' ⧆ a3).
    End demo.
   *)

Rewriting Principles

  Lemma mult_Batch_rw1:
    ∀ `(c: C) `(d: D),
      Done A B C c ⊗ Done A B D d = Done A B (C × D) (c, d).
  Proof.
    reflexivity.
  Qed.

  Lemma mult_Batch_rw2:
    ∀ `(d: D) `(b1: Batch A B C),
      b1 ⊗ Done A B D d = map (Batch A B) (pair_right d) b1.
  Proof.
    intros. induction b1; easy.
  Qed.

  Lemma mult_Batch_rw3:
    ∀ (D: Type) (b2: Batch A B (B → D)) (a: A) `(b1: Batch A B C),
      b1 ⊗ (b2 ⧆ a) =
        map (Batch A B) strength_arrow (b1 ⊗ b2) ⧆ a.
  Proof.
    reflexivity.
  Qed.

  Lemma mult_Batch_rw4:
    ∀ `(b2: Batch A B D) `(c: C),
      Done A B C c ⊗ b2 = map (Batch A B) (pair c) b2.
  Proof.
    induction b2.
    - reflexivity.
    - intros. cbn; change (mult_Batch ?x ?y) with (x ⊗ y).
      fequal. rewrite IHb2.
      compose near b2 on left.
      now rewrite (fun_map_map (F := Batch A B)).
  Qed.

  Lemma mult_Batch_rw5:
    ∀ (a: A) `(b1: @Batch A B (B → C)) `(d: D),
      (b1 ⧆ a) ⊗ Done A B D d =
        map (Batch A B) (costrength_arrow ∘ pair_right d) b1 ⧆ a.
  Proof.
    reflexivity.
  Qed.

  Lemma mult_Batch_rw6:
    ∀ `(b2: @Batch A B (B → D)) `(c: C) (a: A),
      Done A B C c ⊗ (b2 ⧆ a) =
        map (Batch A B) (strength_arrow ∘ pair c) b2 ⧆ a.
  Proof.
    intros.
    rewrite mult_Batch_rw3.
    rewrite mult_Batch_rw4.
    compose near b2 on left.
    now rewrite (fun_map_map (F := Batch A B)).
  Qed.

  Lemma mult_Batch_rw7:
    ∀ (a1 a2: A) `(b1: Batch A B (B → C))
      `(b2: Batch A B (B → D)),
      (b1 ⧆ a1) ⊗ (b2 ⧆ a2) =
        (map (Batch A B) strength_arrow ((b1 ⧆ a1) ⊗ b2)) ⧆ a2.
  Proof.
    reflexivity.
  Qed.

Applicative Laws

  Lemma app_pure_natural_Batch:
    ∀ `(f: C1 → C2) (c: C1),
      map (Batch A B) f (pure (Batch A B) c) =
        pure (Batch A B) (f c).
  Proof.
    reflexivity.
  Qed.

  Lemma app_mult_natural_Batch1:
    ∀ (C1 C2 D: Type) (f: C1 → C2)
      (b1: Batch A B C1) (b2: Batch A B D),
      map (Batch A B) f b1 ⊗ b2 = map (Batch A B) (map_fst f) (b1 ⊗ b2).
  Proof.
    intros. generalize dependent C1. induction b2.
    - intros; cbn. compose near b1.
      now do 2 rewrite (fun_map_map (F := Batch A B)).
    - intros; cbn.
      change (mult_Batch ?x ?y) with (x ⊗ y) in ×.
      rewrite IHb2. compose near (b1 ⊗ b2).
      do 2 rewrite (fun_map_map (F := Batch A B)).
      do 2 fequal.
      now ext [? ?].
  Qed.

  Lemma app_mult_natural_Batch2:
    ∀ (C D1 D2: Type) (g: D1 → D2)
      (b1: Batch A B C) (b2: Batch A B D1),
      b1 ⊗ map (Batch A B) g b2 =
        map (Batch A B) (map_snd g) (b1 ⊗ b2).
  Proof.
    intros. generalize dependent D2.
    induction b2 as [ANY any | ANY rest IH x'].
    - intros; cbn. compose near b1 on right.
      rewrite (fun_map_map (F := Batch A B)).
      reflexivity.
    - intros; cbn. fequal.
      change (mult_Batch ?x ?y) with (x ⊗ y).
      compose near (b1 ⊗ rest).
      rewrite (fun_map_map (F := Batch A B)).
      specialize (IH (B → D2) (compose g)).
      rewrite IH.
      compose near (b1 ⊗ rest) on left.
      rewrite (fun_map_map (F := Batch A B)).
      fequal.
      now ext [c mk].
  Qed.

  Lemma app_mult_natural_Batch:
    ∀ (C1 C2 D1 D2: Type) (f: C1 → C2) (g: D1 → D2)
      (b1: Batch A B C1) (b2: Batch A B D1),
      map (Batch A B) f b1 ⊗ map (Batch A B) g b2 =
        map (Batch A B) (map_tensor f g) (b1 ⊗ b2).
  Proof.
    intros.
    rewrite app_mult_natural_Batch1.
    rewrite app_mult_natural_Batch2.
    compose near (b1 ⊗ b2) on left.
    rewrite (fun_map_map (F := Batch A B)).
    fequal.
    now ext [c1 d1].
  Qed.

  Lemma app_assoc_Batch:
    ∀ (C D E: Type)
      (b1: Batch A B C) (b2: Batch A B D) (b3: Batch A B E),
      map (Batch A B) associator ((b1 ⊗ b2) ⊗ b3) = b1 ⊗ (b2 ⊗ b3).
  Proof.
    intros. induction b3.
    - do 2 rewrite mult_Batch_rw2.
      rewrite app_mult_natural_Batch2.
      compose near (b1 ⊗ b2) on left.
      now rewrite (fun_map_map (F := Batch A B)).
    - cbn. repeat change (mult_Batch ?x ?y) with (x ⊗ y).
      fequal.
      rewrite app_mult_natural_Batch2.
      rewrite <- IHb3.
      compose near (b1 ⊗ b2 ⊗ b3).
      do 2 rewrite (fun_map_map (F := Batch A B)).
      compose near (b1 ⊗ b2 ⊗ b3) on right.
      rewrite (fun_map_map (F := Batch A B)).
      fequal.
      now ext [[c d] mk].
  Qed.

  Lemma app_unital_l_Batch:
    ∀ (C: Type) (b: Batch A B C),
      map (Batch A B) left_unitor (pure (Batch A B) tt ⊗ b) = b.
  Proof.
    intros. induction b.
    - reflexivity.
    - cbn. change (mult_Batch ?x ?y) with (x ⊗ y).
      fequal. compose near (pure (Batch A B) tt ⊗ b).
      rewrite (fun_map_map (F := Batch A B)).
      rewrite <- IHb.
      do 3 fequal.
      assumption.
  Qed.

  Lemma app_unital_r_Batch:
    ∀ (C: Type) (b: Batch A B C),
      map (Batch A B) right_unitor (b ⊗ pure (Batch A B) tt) = b.
  Proof.
    intros. induction b.
    - reflexivity.
    - cbn in ×. fequal. rewrite <- IHb at 2.
      compose near b.
      now do 2 rewrite (fun_map_map (F := Batch A B)).
  Qed.

  Lemma app_mult_pure_Batch:
    ∀ (C D: Type) (c: C) (d: D),
      pure (Batch A B) c ⊗ pure (Batch A B) d =
        pure (Batch A B) (c, d).
  Proof.
    intros. reflexivity.
  Qed.

Typeclass Instance

  #[export] Instance Applicative_Batch: Applicative (Batch A B).
  Proof.
    constructor; intros.
    - typeclasses eauto.
    - reflexivity.
    - apply app_mult_natural_Batch.
    - apply app_assoc_Batch.
    - apply app_unital_l_Batch.
    - apply app_unital_r_Batch.
    - reflexivity.
  Qed.

End Applicative_Batch.

mapfst and mapsnd as Applicative Homomorphisms

Lemma mapfst_Batch1 {B C D: Type} `(f: A1 → A2)
  (b1: Batch A1 B C) (b2: Batch A1 B D):
  mapfst_Batch A1 A2 f (b1 ⊗ b2) =
    mapfst_Batch A1 A2 f b1 ⊗ mapfst_Batch A1 A2 f b2.
Proof.
  generalize dependent b1. induction b2.
  - intros. cbn. now rewrite mapfst_map_Batch.
  - cbn. fequal.
    change (mult_Batch ?x ?y) with (x ⊗ y) in *; intros.
    rewrite <- IHb2.
    now rewrite mapfst_map_Batch.
Qed.

Lemma mapfst_Batch2 {B C D: Type} `(f: A1 → A2)
  (b1: Batch A1 B (C → D)) (b2: Batch A1 B C):
  mapfst_Batch A1 A2 f (b1 <⋆> b2) =
    mapfst_Batch A1 A2 f b1 <⋆> mapfst_Batch A1 A2 f b2.
Proof.
  unfold ap. rewrite mapfst_map_Batch.
  now rewrite mapfst_Batch1.
Qed.

#[export] Instance ApplicativeMorphism_mapfst_Batch
  {B: Type} `(f: A1 → A2):
  ApplicativeMorphism (Batch A1 B) (Batch A2 B)
    (fun C ⇒ mapfst_Batch _ _ f).
Proof.
  intros.
  constructor; try typeclasses eauto.
  - intros. now rewrite mapfst_map_Batch.
  - intros. reflexivity.
  - intros. apply mapfst_Batch1.
Qed.

Lemma mapsnd_Batch1 {A C D: Type} `(f: B1 → B2)
  (b1: Batch A B2 C) (b2: Batch A B2 D):
  mapsnd_Batch B1 B2 f (b1 ⊗ b2) =
    mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2.
Proof.
  generalize dependent b1. induction b2.
  - intros. cbn. now rewrite mapsnd_map_Batch.
  - cbn. fequal.
    change (mult_Batch ?x ?y) with (x ⊗ y) in *; intros.
    rewrite mapsnd_map_Batch.
    compose near (mapsnd_Batch B1 B2 f (b1 ⊗ b2)).
    rewrite (fun_map_map (F := Batch A B1)).
    rewrite app_mult_natural_Batch2.
    compose near (mapsnd_Batch B1 B2 f b1 ⊗ mapsnd_Batch B1 B2 f b2).
    rewrite (fun_map_map (F := Batch A B1)).
    rewrite IHb2. do 2 fequal; ext [c rest].
    reflexivity.
Qed.

Lemma mapsnd_Batch2 {A C D: Type} `(f: B1 → B2)
  (b1: Batch A B2 (C → D)) (b2: Batch A B2 C):
  mapsnd_Batch B1 B2 f (b1 <⋆> b2) =
    mapsnd_Batch B1 B2 f b1 <⋆> mapsnd_Batch B1 B2 f b2.
Proof.
  unfold ap. rewrite mapsnd_map_Batch.
  now rewrite mapsnd_Batch1.
Qed.

#[export] Instance ApplicativeMorphism_mapsnd_Batch
  {A B1 B2: Type} `(f: B1 → B2):
  ApplicativeMorphism (Batch A B2) (Batch A B1)
    (fun C ⇒ mapsnd_Batch B1 B2 f).
Proof.
  intros.
  constructor; try typeclasses eauto.
  - intros. now rewrite mapsnd_map_Batch.
  - intros. reflexivity.
  - intros. apply mapsnd_Batch1.
Qed.

The runBatch Operation

Fixpoint runBatch {A B: Type}
  (F: Type → Type) `{Map F} `{Mult F} `{Pure F}
  (ϕ: A → F B) (C: Type) (b: Batch A B C): F C :=
  match b with
  | Done _ _ _ c ⇒ pure F c
  | Step _ _ _ rest a ⇒ runBatch F ϕ (B → C) rest <⋆> ϕ a
  end.

Rewriting Principles

Lemma runBatch_rw1 `{Applicative F} `(ϕ: A → F B) (C: Type) (c: C):
  runBatch F ϕ C (Done A B C c) = pure F c.
Proof.
  reflexivity.
Qed.

Lemma runBatch_rw2 `{Applicative F} `(ϕ: A → F B)
  (a: A) (C: Type) (rest: Batch A B (B → C)):
  runBatch F ϕ C (rest ⧆ a) = runBatch F ϕ (B → C) rest <⋆> ϕ a.
Proof.
  reflexivity.
Qed.

Naturality of runBatch

Section runBatch_naturality.

  Context
    `{Applicative F}.

  Lemma natural_runBatch
    {A B C1 C2: Type} (ϕ: A → F B) (f: C1 → C2) (b: Batch A B C1):
    map F f (runBatch F ϕ C1 b) = runBatch F ϕ C2 (map (Batch A B) f b).
  Proof.
    generalize dependent C2.
    induction b; intros.
    - cbn. now rewrite app_pure_natural.
    - cbn. rewrite map_ap. fequal. now rewrite IHb.
  Qed.

  #[export] Instance Natural_runBatch `(ϕ: A → F B):
    Natural (runBatch F ϕ).
  constructor; try typeclasses eauto.
  intros C D f. ext b. unfold compose.
  rewrite natural_runBatch.
  reflexivity.
  Qed.

  Lemma runBatch_mapfst:
    ∀ `(s: Batch A1 B C) `(ϕ: A2 → F B) (f: A1 → A2),
      runBatch F (ϕ ∘ f) C s = runBatch F ϕ C (mapfst_Batch A1 A2 f s).
  Proof.
    intros; induction s.
    - easy.
    - cbn. now rewrite IHs.
  Qed.

  Lemma runBatch_mapfst':
    ∀ `(ϕ: A2 → F B) `(f: A1 → A2) C,
      runBatch F (ϕ ∘ f) C = runBatch F ϕ C ∘ mapfst_Batch A1 A2 f.
  Proof.
    intros. ext s.
    apply runBatch_mapfst.
  Qed.

  Lemma runBatch_mapsnd:
    ∀ `(s: @Batch A B2 C) `(ϕ: A → F B1) (f: B1 → B2),
      runBatch F (map F f ∘ ϕ) C s =
        runBatch F ϕ C (mapsnd_Batch B1 B2 f s).
  Proof.
    intros. induction s.
    - easy.
    - intros. cbn. unfold compose at 2.
      rewrite <- ap_map. fequal.
      rewrite IHs.
      now rewrite natural_runBatch.
  Qed.

  Context
    `{homomorphism: ApplicativeMorphism F G ψ}.

  Lemma runBatch_morphism `(ϕ: A → F B) `(b: Batch A B C):
    ψ C (runBatch F ϕ C b) = runBatch G (ψ B ∘ ϕ) C b.
  Proof.
    induction b.
    - cbn. now rewrite appmor_pure.
    - cbn. rewrite ap_morphism_1.
      now rewrite IHb.
  Qed.

  Lemma runBatch_morphism' `(ϕ: A → F B):
    ∀ C, ψ C ∘ runBatch F ϕ C = runBatch G (ψ B ∘ ϕ) C.
  Proof.
    intros. ext b. unfold compose. rewrite runBatch_morphism.
    reflexivity.
  Qed.

End runBatch_naturality.

runBatch as an Applicative Homomorphism

Section runBatch_morphism.

  Context
    `{Applicative F}
    `{ϕ: A → F B}.

  Lemma appmor_pure_runBatch: ∀ (a: A),
      runBatch F ϕ A (pure (Batch A B) a) = pure F a.
  Proof.
    easy.
  Qed.

  Lemma appmor_mult_runBatch:
    ∀ {C D} (x: Batch A B C) (y: Batch A B D),
      runBatch F ϕ (C × D) (x ⊗ y) =
        runBatch F ϕ C x ⊗ runBatch F ϕ D y.
  Proof.
    intros. generalize dependent x.
    induction y as [ANY any | ANY rest IH x'].
    - intros. rewrite mult_Batch_rw2.
      rewrite runBatch_rw1. rewrite triangle_4.
      now rewrite natural_runBatch.
    - intros. rewrite runBatch_rw2.
      unfold ap. rewrite (app_mult_natural_r F).
      rewrite <- app_assoc.
      rewrite <- IH. clear IH.
      compose near (runBatch F ϕ _ (x ⊗ rest) ⊗ ϕ x').
      rewrite fun_map_map.
      cbn. unfold ap. change (mult_Batch ?jx ?jy) with (jx ⊗ jy).
      rewrite <- natural_runBatch. rewrite (app_mult_natural_l F).
      compose near (runBatch F ϕ _ (x ⊗ rest) ⊗ ϕ x') on left.
      rewrite fun_map_map. fequal. now ext [[? ?] ?].
  Qed.

  #[export] Instance ApplicativeMorphism_runBatch:
    ApplicativeMorphism (Batch A B) F (runBatch F ϕ).
  Proof.
    constructor; try typeclasses eauto.
    - intros. now rewrite natural_runBatch.
    - intros. easy.
    - intros. apply appmor_mult_runBatch.
  Qed.

End runBatch_morphism.

Batch as a Parameterized Monad

Section parameterised_monad.

Operations batch and join_Batch

  Definition batch (A B: Type): A → Batch A B B :=
    Step A B B (Done A B (B → B) (@id B)).

  Fixpoint join_Batch {A B C D: Type}
    (b: Batch (Batch A B C) C D): Batch A B D :=
    match b with
    | Done _ _ _ d ⇒ Done _ _ _ d
    | Step _ _ _ rest a ⇒
        ap (Batch A B) (@join_Batch A B C (C → D) rest) a
    end.

  Lemma join_Batch_rw1 {A B C D: Type}:
    ∀ (rest: Batch (Batch A B C) C (C → D)) (b: Batch A B C),
      join_Batch (rest ⧆ b) = join_Batch rest <⋆> b.
  Proof.
    reflexivity.
  Qed.

join_Batch as runBatch (Batch A B) id

  Lemma join_Batch_to_runBatch: ∀ (A B C: Type),
      @join_Batch A B C = runBatch (Batch A B) (@id (Batch A B C)).
  Proof.
    intros. ext D b.
    induction b as [D d | D rest IHrest a].
    - reflexivity.
    - rewrite join_Batch_rw1.
      rewrite IHrest.
      reflexivity.
  Qed.

Naturality

  Lemma ret_natural (A1 A2 B: Type) (f: A1 → A2):
    mapfst_Batch A1 A2 f ∘ batch A1 B = batch A2 B ∘ f.
  Proof.
    reflexivity.
  Qed.

  Lemma ret_dinatural (A B1 B2: Type) (f: B1 → B2):
    mapsnd_Batch B1 B2 f ∘ batch A B2 = map (Batch A B1) f ∘ batch A B1.
  Proof.
    reflexivity.
  Qed.

join as an Applicative Homomorphism

  #[export] Instance ApplicativeMorphism_join_Batch:
    ∀ (A B C: Type),
      ApplicativeMorphism (Batch (Batch A B C) C) (Batch A B)
        (@join_Batch A B C).
  Proof.
    intros.
    rewrite (@join_Batch_to_runBatch A B C).
    apply ApplicativeMorphism_runBatch.
  Qed.

Other Laws

  Lemma runBatch_batch:
    ∀ (G: Type → Type) `{Applicative G} (A B: Type) (f: A → G B),
      runBatch G f B ∘ batch A B = f.
  Proof.
    intros. ext a. cbn.
    now rewrite ap1.
  Qed.

  Lemma runBatch_batch_id: ∀ (A B: Type),
      runBatch (Batch A B) (batch A B) B =
        @id (Batch A B B).
  Proof.
    intros. ext b.
    induction b as [C c | C rest IHrest a].
    - reflexivity.
    - cbn. unfold id in ×.
      fequal. rewrite IHrest.
      compose near rest.
      rewrite (fun_map_map (F := Batch A B)).
      compose near rest.
      rewrite (fun_map_map (F := Batch A B)).
      unfold compose, strength_arrow.
      change rest with (id rest) at 2.
      rewrite <- (fun_map_id (F := Batch A B)).
      fequal.
  Qed.

Monad Laws

  Lemma ret_join: ∀ (A B C: Type),
      (@join_Batch A B C C) ∘ batch (Batch A B C) C = @id (Batch A B C).
  Proof.
    intros. ext b. unfold compose, id.
    induction b as [C c | C rest IHrest a].
    - reflexivity.
    - unfold batch.
      unfold join_Batch.
      change (Done A B (C → C) id) with (pure (Batch A B) (@id C)).
      rewrite ap1.
      reflexivity.
  Qed.

  Lemma join_map_ret: ∀ (A B C: Type),
      (@join_Batch A B B C) ∘ mapfst_Batch A (Batch A B B) (batch A B) =
        @id (Batch A B C).
  Proof.
    intros. ext b. unfold compose, id.
    induction b as [C c | C rest IHrest a].
    - reflexivity.
    - cbn. rewrite IHrest. fequal.
      compose near rest on left.
      rewrite (fun_map_map).
      compose near rest on left.
      rewrite (fun_map_map).
      replace (compose (fun '(f, a0) ⇒ f a0)
                 ∘ (strength_arrow ∘ (fun c: B → C ⇒ (c, id))))
        with (@id (B → C)).
      2:{ symmetry.
          ext f b.
          unfold compose, strength_arrow, id.
          reflexivity. }
      rewrite fun_map_id.
      reflexivity.
  Qed.

  #[local] Instance Map_Batch_Fst (B: Type):
    Map (fun A ⇒ Batch A B B) :=
    fun A B f ⇒ mapfst_Batch _ _ f.

  #[local] Instance Return_Batch (B: Type):
    Return (fun A ⇒ Batch A B B) :=
    (fun A ⇒ batch A B).

  #[local] Instance Join_Batch (B: Type):
    Join (fun A ⇒ Batch A B B) :=
    fun A ⇒ @join_Batch A B B B.

  Goal ∀ B, Categorical.Monad.Monad (fun A ⇒ Batch A B B).
  Proof.
    intros. constructor.
    - typeclasses eauto.
    - constructor.
      + typeclasses eauto.
      + typeclasses eauto.
      + unfold_ops @Map_Batch_Fst.
        unfold_ops @Return_Batch.
        unfold_ops @Map_I.
        reflexivity.
    - admit.
    - unfold_ops @Join_Batch Return_Batch.
      intros A. ext b.
      induction b.
      + reflexivity.
      + cbn.
  Abort.

End parameterised_monad.

Batch as a Parameterized Comonad

Section parameterized.

  #[local] Unset Implicit Arguments.

Operations extract_Batch and cojoin_Batch

  Fixpoint extract_Batch {A B: Type} (b: Batch A A B): B :=
    match b with
    | Done _ _ _ b ⇒ b
    | Step _ _ _ rest a ⇒ extract_Batch rest a
    end.

  Fixpoint cojoin_Batch {A B C D: Type} (b: Batch A C D):
    Batch A B (Batch B C D) :=
    match b with
    | Done _ _ _ d ⇒ Done A B (Batch B C D) (Done B C D d)
    | Step _ _ _ rest a ⇒
        Step A B (Batch B C D)
          (map (Batch A B) (Step B C D) (cojoin_Batch rest)) a
    end.

Rewriting Principles

  Lemma extract_Batch_rw0:
    ∀ (A C: Type) (c: C),
      extract_Batch (Done A A C c) = c.
  Proof.
    reflexivity.
  Qed.

  Lemma extract_Batch_rw1:
    ∀ (A B: Type) (rest: Batch A A (A → B)) (a: A),
      extract_Batch (rest ⧆ a) = extract_Batch rest a.
  Proof.
    reflexivity.
  Qed.

  Lemma cojoin_Batch_rw0:
    ∀ (A B C D: Type) (d: D),
      @cojoin_Batch A B C D (Done A C D d) =
        Done A B (Batch B C D) (Done B C D d).
  Proof.
    reflexivity.
  Qed.

  Lemma cojoin_Batch_rw1:
    ∀ (A B C D: Type) (rest: Batch A C (C → D)) (a: A),
      @cojoin_Batch A B C D (rest ⧆ a) =
        map (Batch A B) (Step B C D) (cojoin_Batch rest) ⧆ a.
  Proof.
    reflexivity.
  Qed.

extract_Batch as runBatch (fun A => A) id

  Lemma extract_Batch_to_runBatch: ∀ (A: Type),
      @extract_Batch A = runBatch (fun A ⇒ A) (@id A).
  Proof.
    intros. ext B b.
    induction b.
    - reflexivity.
    - cbn. rewrite IHb.
      reflexivity.
  Qed.

cojoin_Batch as runBatch double_batch

  Definition double_batch {A B C: Type}:
    A → Batch A B (Batch B C C) :=
    map (Batch A B) (batch B C) ∘ (batch A B).

  Lemma double_batch_rw {A B C: Type} (a: A):
    double_batch (B := B) (C := C) a =
      Done A B (B → Batch B C C) (batch B C) ⧆ a.
  Proof.
    reflexivity.
  Qed.

  Lemma double_batch_spec: ∀ (A B C: Type),
      double_batch = batch B C ⋆2 batch A B.
  Proof.
    reflexivity.
  Qed.
  Lemma cojoin_Batch_to_runBatch: ∀ (A B C: Type),
      @cojoin_Batch A B C =
        runBatch (Batch A B ∘ Batch B C) double_batch.
  Proof.
    intros. ext D.
    ext b.
    induction b as [D d | D rest IHrest a].
    - reflexivity.
    - cbn.
      compose near (runBatch (Batch A B ∘ Batch B C) double_batch (C → D) rest).
      rewrite (fun_map_map (F := Batch A B)).
      compose near (runBatch (Batch A B ∘ Batch B C) double_batch (C → D) rest).
      rewrite (fun_map_map (F := Batch A B)).
      compose near (runBatch (Batch A B ∘ Batch B C) double_batch (C → D) rest).
      rewrite (fun_map_map (F := Batch A B)).
      rewrite <- IHrest.
      fequal.
      fequal.
      clear.
      ext rest b. cbn.
      unfold compose, id.
      fequal.
      compose near rest.
      rewrite fun_map_map.
      compose near rest.
      rewrite fun_map_map.
      rewrite fun_map_id.
      reflexivity.
  Qed.

extract_Batch and cojoin_Batch as Applicative Homomorphisms

  #[export] Instance ApplicativeMorphism_extract_Batch:
    ∀ (A: Type),
      ApplicativeMorphism (Batch A A) (fun A ⇒ A) (@extract_Batch A).
  Proof.
    intros.
    rewrite extract_Batch_to_runBatch.
    apply ApplicativeMorphism_runBatch.
  Qed.

  #[export] Instance ApplicativeMorphism_cojoin_Batch:
    ∀ (A B C: Type),
      ApplicativeMorphism (Batch A C) (Batch A B ∘ Batch B C)
        (@cojoin_Batch A B C).
  Proof.
    intros.
    rewrite cojoin_Batch_to_runBatch.
    apply ApplicativeMorphism_runBatch.
  Qed.

Composition with ret/batch

  Lemma extract_Batch_batch: ∀ (A: Type),
      extract_Batch ∘ batch A A = @id A.
  Proof.
    reflexivity.
  Qed.

  Lemma cojoin_Batch_batch: ∀ (A B C: Type),
      @cojoin_Batch A B C C ∘ batch A C =
        double_batch.
  Proof.
    intros.
    rewrite cojoin_Batch_to_runBatch.
    rewrite (runBatch_batch (Batch A B ∘ Batch B C) A C).
    reflexivity.
  Qed.

Naturality

  Lemma extract_natural (A C D: Type) (f: C → D):
    ∀ (b: Batch A A C),
      @extract_Batch A D (map (Batch A A) f b) =
        f (@extract_Batch A C b).
  Proof.
    intros.
    generalize dependent D.
    induction b as [C c | C rest IHrest a]; intros D f.
    - reflexivity.
    - cbn.
      now rewrite IHrest.
  Qed.

  Lemma extract_dinatural (A B C: Type) (f: A → B):
    ∀ (b: Batch A B C),
      @extract_Batch B C (mapfst_Batch A B f b) =
        @extract_Batch A C (mapsnd_Batch A B f b).
  Proof.
    intros.
    induction b as [C c | C rest IHrest a].
    - reflexivity.
    - cbn.
      rewrite IHrest.
      rewrite extract_natural.
      reflexivity.
  Qed.

  Lemma cojoin_natural (A B C D E: Type) (f: D → E):
    ∀ (b: Batch A C D),
      @cojoin_Batch A B C E (map (Batch A C) f b) =
        map (Batch A B) (map (Batch B C) f) (@cojoin_Batch A B C D b).
  Proof.
    intros.
    generalize dependent E.
    induction b as [D d | D rest IHrest a]; intros E f.
    - reflexivity.
    - cbn.
      rewrite IHrest.
      compose near (cojoin_Batch (B := B) rest).
      rewrite (fun_map_map (F := Batch A B)).
      rewrite (fun_map_map (F := Batch A B)).
      reflexivity.
  Qed.

  Lemma cojoin_natural1 (A A' B C D: Type) (f: A → A'):
    ∀ (b: Batch A C D),
      @cojoin_Batch A' B C D (mapfst_Batch _ _ f b) =
        mapfst_Batch _ _ f (@cojoin_Batch A B C D b).
  Proof.
    intros.
    induction b as [D d | D rest IHrest a].
    - reflexivity.
    - cbn.
      rewrite IHrest.
      rewrite <- mapfst_map_Batch.
      reflexivity.
  Qed.

  Lemma cojoin_natural2 (A B C C' D: Type) (f: C → C'):
    ∀ (b: Batch A C' D),
      @cojoin_Batch A B C D (mapsnd_Batch _ _ f b) =
        map (Batch A B) (mapsnd_Batch _ _ f) (@cojoin_Batch A B C' D b).
  Proof.
    intros.
    generalize dependent C.
    induction b as [D d | D rest IHrest a]; intros C f.
    - reflexivity.
    - cbn.
      rewrite cojoin_natural.
      change (map (Batch A B) ?g (map (Batch A B) ?f ?b))
        with ((map (Batch A B) g ∘ map (Batch A B) f) b).
      rewrite (fun_map_map (F := Batch A B)).
      rewrite (fun_map_map (F := Batch A B)).
      rewrite IHrest.
      change (map (Batch A B) ?g (map (Batch A B) ?f ?b))
        with ((map (Batch A B) g ∘ map (Batch A B) f) b).
      rewrite (fun_map_map (F := Batch A B)).
      reflexivity.
  Qed.

  Lemma cojoin_dinatural (A B B' C D: Type) (f: B → B'):
    ∀ (b: Batch A C D),
      map (Batch A B) (mapfst_Batch _ _ f) (@cojoin_Batch A B C D b) =
        (mapsnd_Batch _ _ f) (@cojoin_Batch A B' C D b).
  Proof.
    intros.
    induction b as [D d | D rest IHrest a].
    - reflexivity.
    - cbn.
      compose near (cojoin_Batch (B := B) rest).
      rewrite (fun_map_map (F := Batch A B)).
      rewrite mapsnd_map_Batch.
      compose near (mapsnd_Batch B B' f (cojoin_Batch (B := B') rest)).
      rewrite (fun_map_map (F := Batch A B)).
      rewrite <- IHrest.
      compose near (cojoin_Batch (B := B) rest).
      rewrite (fun_map_map (F := Batch A B)).
      reflexivity.
  Qed.

Comonad Laws

  Lemma extr_cojoin_Batch:
    `(extract_Batch ∘ cojoin_Batch = @id (Batch A B C)).
  Proof.
    intros. ext b. unfold id.
    induction b as [C c | C rest IHrest a].
    - unfold compose. cbn. reflexivity.
    - unfold compose in ×.
      cbn.
      rewrite extract_natural.
      rewrite IHrest.
      reflexivity.
  Qed.

  (* TODO Finish rest of the parameterized comonad structure. *)

End parameterized.

Batch is Traversable in the First Argument

Fixpoint traverse_Batch (B C: Type) (G: Type → Type)
  `{Map G} `{Pure G} `{Mult G} (A A': Type) (f: A → G A')
  (b: Batch A B C): G (Batch A' B C) :=
  match b with
  | Done _ _ _ c ⇒ pure G (Done A' B C c)
  | Step _ _ _ rest a ⇒
      pure G (Step A' B C) <⋆>
        traverse_Batch B (B → C) G A A' f rest <⋆>
        f a
  end.

#[export] Instance Traverse_Batch1:
  ∀ (B C: Type), Traverse (BATCH1 B C) := traverse_Batch.

Rewriting Principles

Lemma traverse_Batch_rw1:
  ∀ (B C: Type)
    (G: Type → Type)
    `{Map G} `{Pure G} `{Mult G}
    (A A': Type) (f: A → G A') (c: C),
    traverse f (Done A B C c) = pure G (Done A' B C c).
Proof.
  reflexivity.
Qed.

Lemma traverse_Batch_rw1':
  ∀ (B C: Type)
    (G: Type → Type)
    `{Map G} `{Pure G} `{Mult G}
    (A A': Type) (f: A → G A'),
    (traverse f ∘ pure (Batch A B)) =
      pure (G ∘ Batch A' B) (A := C).
Proof.
  intros.
  unfold_ops @Pure_Batch.
  unfold_ops @Pure_compose.
  unfold pure at 2.
  unfold compose at 1; ext c.
  rewrite traverse_Batch_rw1.
  reflexivity.
Qed.

Lemma traverse_Batch_rw2:
  ∀`{Map G} `{Pure G} `{Mult G}
   `{! Applicative G}
   (B C: Type)
   (A A': Type) (f: A → G A')
   (k: Batch A B (B → C)) (a: A),
    traverse f (k ⧆ a) =
      map G (Step A' B C) (traverse (G := G) f k) <⋆> f a.
Proof.
  intros. cbn.
  rewrite <- map_to_ap.
  reflexivity.
Qed.

Lemma traverse_Batch_rw2':
  ∀ `{Map G} `{Pure G} `{Mult G}
    `{! Applicative G}
    (B C: Type)
    (A A': Type) (f: A → G A')
    (k: Batch A B (B → C)) (a: A),
    traverse f (k ⧆ a) =
      map G (Step A' B C) (traverse (G := G) f k) <⋆> f a.
Proof.
  intros.
  rewrite traverse_Batch_rw2.
  reflexivity.
Qed.

Lemma traverse_Batch_ap_rw2:
  ∀`{Map G} `{Pure G} `{Mult G}
   `{! Applicative G}
   (B C: Type)
   (A A': Type) (f: A → G A')
   {X Y: Type}
   (lhs: Batch A B (X → Y))
   (rhs: Batch A B X),
    traverse (T := BATCH1 B Y) f (lhs <⋆> rhs) =
      pure G (ap (Batch A' B) (A := X) (B := Y))
        <⋆> traverse (T := BATCH1 B (X → Y)) f lhs
        <⋆> traverse (T := BATCH1 B X) f rhs.
Proof.
  intros.
  destruct lhs.
Abort.

Traversable Functor Laws

Lemma trf_traverse_id_Batch:
  ∀ (B C A: Type),
    traverse (T := BATCH1 B C) (G := fun X: Type ⇒ X) (@id A) = id.
Proof.
  intros. ext b.
  unfold id.
  induction b as [C c | C rest IHrest].
  - cbn. reflexivity.
  - cbn.
    change (Traverse_Batch1 B (B → C)) with
      (@traverse (BATCH1 B (B → C)) _).
    rewrite IHrest.
    reflexivity.
Qed.

Lemma trf_traverse_traverse_Batch (B C: Type):
  ∀ `(H0: Map G1) (H1: Pure G1) (H2: Mult G1),
    Applicative G1 →
    ∀ `(H4: Map G2) (H5: Pure G2) (H6: Mult G2),
      Applicative G2 →
      ∀ (A A' A'': Type) (g: A' → G2 A'') (f: A → G1 A'),
        map G1 (traverse (T := BATCH1 B C) g) ∘
          traverse (T := BATCH1 B C) f =
          traverse (T := BATCH1 B C) (G := G1 ∘ G2) (g ⋆2 f).
Proof.
  intros. ext b.
  unfold id.
  induction b as [C c | C rest IHrest].
  - cbn. unfold compose.
    cbn. rewrite app_pure_natural.
    reflexivity.
  - cbn.
    (* RHS *)
    change (Traverse_Batch1 B (B → C))
      with (@traverse (BATCH1 B (B → C)) _).
    (* cleanup *)
    rewrite (ap_compose1 G2 G1).
    rewrite (ap_compose1 G2 G1).
    rewrite <- map_to_ap.
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    (* <<unfold_ops Pure_compose>> prevents << rewrite <- IHrest>> *)
    unfold pure at 2; unfold Pure_compose at 1.
    rewrite ap2.
    (* deal with <<rest>> *)
    rewrite <- IHrest.
    unfold compose at 4.
    rewrite <- ap_map.
    rewrite app_pure_natural.
    unfold kc2.
    unfold compose at 4.
    rewrite <- ap_map.
    rewrite map_ap.
    rewrite app_pure_natural.
    (* LHS *)
    unfold compose; cbn.
    fold (@traverse (BATCH1 B (B → C)) _).
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    reflexivity.
Qed.

Lemma trf_traverse_morphism_Batch:
  ∀ (B C: Type) (G1 G2: Type → Type)
    `{ApplicativeMorphism G1 G2 ϕ},
  ∀ (A A': Type) (f: A → G1 A'),
    ϕ (BATCH1 B C A') ∘ traverse (T := BATCH1 B C) (G := G1) f =
      traverse (T := BATCH1 B C) (G := G2) (ϕ A' ∘ f).
Proof.
  intros. ext b.
  induction b as [C c | C rest IHrest].
  - unfold compose; cbn.
    now rewrite appmor_pure.
  - cbn.
    unfold compose at 1. cbn.
    change (Traverse_Batch1 B (B → C))
      with (@traverse (BATCH1 B (B → C)) _).
    rewrite <- IHrest.
    rewrite <- (appmor_pure (F := G1) (G := G2)).
    rewrite (ap_morphism_1 (ϕ := ϕ)).
    rewrite (ap_morphism_1 (ϕ := ϕ)).
    reflexivity.
Qed.

Typeclass Instance

#[export] Instance TraversableFunctor_Batch: ∀ (B C: Type),
    TraversableFunctor (BATCH1 B C) :=
  fun B C ⇒
    {| trf_traverse_id := trf_traverse_id_Batch B C;
       trf_traverse_traverse := @trf_traverse_traverse_Batch B C;
       trf_traverse_morphism := @trf_traverse_morphism_Batch B C;
    |}.

Compatibility with map

Lemma map_compat_traverse_Batch1: ∀ (B C: Type),
    @map (BATCH1 B C) _ =
      @traverse (BATCH1 B C) _ (fun A ⇒ A) Map_I Pure_I Mult_I.
Proof.
  intros.
  ext A A' f b.
  induction b as [C c | C rest IHrest a].
  - reflexivity.
  - cbn.
    change (Traverse_Batch1 B (B → C)) with
      (@traverse (BATCH1 B (B → C)) _).
    rewrite <- IHrest.
    reflexivity.
Qed.

#[export] Instance Compat_Map_Traverse_Batch1:
  ∀ B C, @Compat_Map_Traverse (BATCH1 B C) _ _.
Proof.
  intros. hnf.
  ext X Y f.
  change_left (map (BATCH1 B C) f).
  rewrite map_compat_traverse_Batch1.
  reflexivity.
Qed.

runBatch Characterized by traverse

Lemma runBatch_via_traverse {A B: Type}
  {F: Type → Type}
  `{Map F} `{Mult F} `{Pure F} `{! Applicative F}
  (ϕ: A → F B) (C: Type):
  runBatch F ϕ C =
    map F extract_Batch ∘ traverse (G := F) (T := BATCH1 B C) ϕ.
Proof.
  intros. ext b.
  induction b as [C c | C rest IHrest].
  - unfold compose; cbn.
    rewrite app_pure_natural.
    reflexivity.
  - cbn.
    rewrite IHrest.
    unfold compose; cbn.
    fold (@traverse (BATCH1 B (B → C)) _).
    rewrite map_ap.
    rewrite map_ap.
    rewrite app_pure_natural.
    rewrite map_to_ap.
    reflexivity.
Qed.

Notations

Module Notations.
  Infix "⧆" :=
    (Step _ _ _) (at level 51, left associativity): tealeaves_scope.
End Notations.

Arguments

#[global] Arguments runBatch {A B}%type_scope {G}%function_scope
  {H H0 H1} f%function_scope {C}%type_scope b: rename.
#[global] Arguments mapfst_Batch {B C A1 A2}%type_scope
  f%function_scope b.
#[global] Arguments mapsnd_Batch {A B1 B2 C}%type_scope
  f%function_scope b.