From Tealeaves Require Import
  Classes.Categorical.Applicative
  Categories.TypeFamily.

Import Applicative.Notations.

#[local] Generalizable Variables A B C D W S G T.
#[local] Set Implicit Arguments.

(** * Multisorted <<Batch>> Functor (<<BatchM>>) *)
(**********************************************************************)
Section BatchM.

  Context
    `{ix: Index}
    {T: K -> Type -> Type}
    {W A B: Type}.

  Inductive BatchM C: Type:=
  | Go: C -> BatchM C
  | Ap: forall (k: K), BatchM (T k B -> C) -> W * A -> BatchM C.

  #[local] Infix "⧆":=
    Ap (at level 51, left associativity): tealeaves_multi_scope.

  (** ** Functor Instance *)
  (********************************************************************)
  Fixpoint map_BatchM `{f: C -> D} `(c: BatchM C): BatchM D:=
    match c with
    | Go c => Go (f c)
    | @Ap _ k rest (pair w a) =>
        Ap (@map_BatchM (T k B -> C) (T k B -> D) (compose f) rest) (w, a)
    end.

  #[global] Instance Map_BatchM: Map BatchM:= @map_BatchM.

  Lemma map_id_BatchM: forall (C: Type),
      map (F:= BatchM) id = @id (BatchM C).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall C : Type, map id = id
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall C : Type, map id = id
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
map id = id ext s.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
s: BatchM C
map id s = id s induction s.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
c: C
map id (Go c) = id (Go c)
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
p: W * A
IHs: map id s = id s
map id (s ⧆ p) = id (s ⧆ p)
    -
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
c: C
map id (Go c) = id (Go c) easy.
    -
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
p: W * A
IHs: map id s = id s
map id (s ⧆ p) = id (s ⧆ p) unfold id in *.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
p: W * A
IHs: map (fun x : T k B -> C => x) s = s
map (fun x : C => x) (s ⧆ p) = s ⧆ p destruct p.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
w: W
a: A
IHs: map (fun x : T k B -> C => x) s = s
map (fun x : C => x) (s ⧆ (w, a)) = s ⧆ (w, a)
      now rewrite <- IHs at 2.
  Qed.

  Lemma map_map_BatchM: forall (C D E: Type) (f: C -> D) (g: D -> E),
      map (F:= BatchM) g ∘ map (F:= BatchM) f = map (F:= BatchM) (g ∘ f).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (C D E : Type) (f : C -> D) (g : D -> E),
map g ∘ map f = map (g ∘ f)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (C D E : Type) (f : C -> D) (g : D -> E),
map g ∘ map f = map (g ∘ f)
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, C, D, E: Type
f: C -> D
g: D -> E
map g ∘ map f = map (g ∘ f) unfold compose.
ix: Index
T: K -> Type -> Type
W, A, B, C, D, E: Type
f: C -> D
g: D -> E
map g ○ map f = map (g ○ f) ext s.
ix: Index
T: K -> Type -> Type
W, A, B, C, D, E: Type
f: C -> D
g: D -> E
s: BatchM C
map g (map f s) = map (g ○ f) s generalize dependent E.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
s: BatchM C
forall (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s
    generalize dependent D.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
s: BatchM C
forall (D : Type) (f : C -> D) (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s induction s.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
c: C
forall (D : Type) (f : C -> D) (E : Type) (g : D -> E),
map g (map f (Go c)) = map (g ○ f) (Go c)
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
p: W * A
IHs: forall (D : Type) (f : (T k B -> C) -> D) (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s
forall (D : Type) (f : C -> D) (E : Type) (g : D -> E),
map g (map f (s ⧆ p)) = map (g ○ f) (s ⧆ p)
    -
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
c: C
forall (D : Type) (f : C -> D) (E : Type) (g : D -> E),
map g (map f (Go c)) = map (g ○ f) (Go c) easy.
    -
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
p: W * A
IHs: forall (D : Type) (f : (T k B -> C) -> D) (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s
forall (D : Type) (f : C -> D) (E : Type) (g : D -> E),
map g (map f (s ⧆ p)) = map (g ○ f) (s ⧆ p) intros.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
p: W * A
IHs: forall (D : Type) (f : (T k B -> C) -> D) (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s
D: Type
f: C -> D
E: Type
g: D -> E
map g (map f (s ⧆ p)) = map (g ○ f) (s ⧆ p) destruct p.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
w: W
a: A
IHs: forall (D : Type) (f : (T k B -> C) -> D) (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s
D: Type
f: C -> D
E: Type
g: D -> E
map g (map f (s ⧆ (w, a))) = map (g ○ f) (s ⧆ (w, a)) cbn.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
w: W
a: A
IHs: forall (D : Type) (f : (T k B -> C) -> D) (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s
D: Type
f: C -> D
E: Type
g: D -> E
map (compose g) (map (compose f) s) ⧆ (w, a) =
map (compose (g ○ f)) s ⧆ (w, a) fequal.
ix: Index
T: K -> Type -> Type
W, A, B, C: Type
k: K
s: BatchM (T k B -> C)
w: W
a: A
IHs: forall (D : Type) (f : (T k B -> C) -> D) (E : Type) (g : D -> E),
map g (map f s) = map (g ○ f) s
D: Type
f: C -> D
E: Type
g: D -> E
map (compose g) (map (compose f) s) =
map (compose (g ○ f)) s
      apply IHs.
  Qed.

  #[global, program] Instance Functor_BatchM: Functor BatchM:=
    {| fun_map_id:= map_id_BatchM;
      fun_map_map:= map_map_BatchM;
    |}.

  (** ** Applicative Instance *)
  (********************************************************************)
  #[global] Instance Pure_BatchM: Pure BatchM:=
    fun (C: Type) (c: C) => Go c.

  Fixpoint mult_BatchM `(jc: BatchM C) `(jd: BatchM D): BatchM (C * D) :=
    match jd with
    | Go d => map (F:= BatchM) (fun (c: C) => (c, d)) jc
    | Ap rest (pair w a) =>
        Ap (map (F:= BatchM)
              strength_arrow (mult_BatchM jc rest)) (pair w a)
    end.

  #[global] Instance Mult_BatchM: Mult BatchM:=
    fun C D '(c, d) => mult_BatchM c d.

  Lemma mult_BatchM_rw1:
    forall `(a: A) `(b: B),
      Go a ⊗ Go b = Go (a, b).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (a : A) (b : B), Go a ⊗ Go b = Go (a, b)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (a : A) (b : B), Go a ⊗ Go b = Go (a, b)
    easy.
  Qed.

  Lemma mult_BatchM_rw2:
    forall `(d: D) `(jc: BatchM C),
      jc ⊗ Go d = map (F:= BatchM) (pair_right d) jc.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (D : Type) (d : D) (C : Type) (jc : BatchM C),
jc ⊗ Go d = map (pair_right d) jc
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (D : Type) (d : D) (C : Type) (jc : BatchM C),
jc ⊗ Go d = map (pair_right d) jc
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
jc: BatchM C
jc ⊗ Go d = map (pair_right d) jc induction jc; easy.
  Qed.

  Lemma mult_BatchM_rw3:
    forall `(d: D) `(jc: BatchM C),
      Go d ⊗ jc =
        map (F:= BatchM) (pair d) jc.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (D : Type) (d : D) (C : Type) (jc : BatchM C),
Go d ⊗ jc = map (pair d) jc
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (D : Type) (d : D) (C : Type) (jc : BatchM C),
Go d ⊗ jc = map (pair d) jc
    induction jc.
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
c: C
Go d ⊗ Go c = map (pair d) (Go c)
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
k: K
jc: BatchM (T k B -> C)
p: W * A
IHjc: Go d ⊗ jc = map (pair d) jc
Go d ⊗ (jc ⧆ p) = map (pair d) (jc ⧆ p)
    -
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
c: C
Go d ⊗ Go c = map (pair d) (Go c) easy.
    -
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
k: K
jc: BatchM (T k B -> C)
p: W * A
IHjc: Go d ⊗ jc = map (pair d) jc
Go d ⊗ (jc ⧆ p) = map (pair d) (jc ⧆ p) destruct p.
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
k: K
jc: BatchM (T k B -> C)
w: W
a: A
IHjc: Go d ⊗ jc = map (pair d) jc
Go d ⊗ (jc ⧆ (w, a)) = map (pair d) (jc ⧆ (w, a)) cbn; change (mult_BatchM ?x ?y) with (x ⊗ y).
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
k: K
jc: BatchM (T k B -> C)
w: W
a: A
IHjc: Go d ⊗ jc = map (pair d) jc
map strength_arrow (Go d ⊗ jc) ⧆ (w, a) =
map (compose (pair d)) jc ⧆ (w, a)
      fequal.
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
k: K
jc: BatchM (T k B -> C)
w: W
a: A
IHjc: Go d ⊗ jc = map (pair d) jc
map strength_arrow (Go d ⊗ jc) =
map (compose (pair d)) jc rewrite IHjc.
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
k: K
jc: BatchM (T k B -> C)
w: W
a: A
IHjc: Go d ⊗ jc = map (pair d) jc
map strength_arrow (map (pair d) jc) =
map (compose (pair d)) jc compose near jc on left.
ix: Index
T: K -> Type -> Type
W, A, B, D: Type
d: D
C: Type
k: K
jc: BatchM (T k B -> C)
w: W
a: A
IHjc: Go d ⊗ jc = map (pair d) jc
(map strength_arrow ∘ map (pair d)) jc =
map (compose (pair d)) jc
      now rewrite (fun_map_map (F:= BatchM)).
  Qed.

  Lemma mult_BatchM_rw4:
    forall (w: W) (a: A) (k: K) `(jc: @BatchM (T k B -> C)) `(d: D),
      (jc ⧆ (w, a)) ⊗ Go d =
        map (F:= BatchM) (costrength_arrow ∘ pair_right d) jc ⧆ (w, a).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (w : W) (a : A) (k : K) (C : Type)
  (jc : BatchM (T k B -> C)) (D : Type) (d : D),
(jc ⧆ (w, a)) ⊗ Go d =
map (costrength_arrow ∘ pair_right d) jc ⧆ (w, a)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (w : W) (a : A) (k : K) (C : Type)
  (jc : BatchM (T k B -> C)) (D : Type) (d : D),
(jc ⧆ (w, a)) ⊗ Go d =
map (costrength_arrow ∘ pair_right d) jc ⧆ (w, a)
    easy.
  Qed.

  Lemma mult_BatchM_rw5:
    forall (w: W) (a: A) (k: K) `(jc: @BatchM (T k B -> C)) `(d: D),
      Go d ⊗ (jc ⧆ (w, a)) =
        map (F:= BatchM) (strength_arrow ∘ pair d) jc ⧆ (w, a).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (w : W) (a : A) (k : K) (C : Type)
  (jc : BatchM (T k B -> C)) (D : Type) (d : D),
Go d ⊗ (jc ⧆ (w, a)) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (w : W) (a : A) (k : K) (C : Type)
  (jc : BatchM (T k B -> C)) (D : Type) (d : D),
Go d ⊗ (jc ⧆ (w, a)) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a)
    intros.
ix: Index
T: K -> Type -> Type
W, A, B: Type
w: W
a: A
k: K
C: Type
jc: BatchM (T k B -> C)
D: Type
d: D
Go d ⊗ (jc ⧆ (w, a)) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a) cbn.
ix: Index
T: K -> Type -> Type
W, A, B: Type
w: W
a: A
k: K
C: Type
jc: BatchM (T k B -> C)
D: Type
d: D
map strength_arrow (mult_BatchM (Go d) jc) ⧆ (w, a) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a)
    change (mult_BatchM ?x ?y) with (x ⊗ y).
ix: Index
T: K -> Type -> Type
W, A, B: Type
w: W
a: A
k: K
C: Type
jc: BatchM (T k B -> C)
D: Type
d: D
map strength_arrow (Go d ⊗ jc) ⧆ (w, a) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a)
    rewrite (mult_BatchM_rw3 d).
ix: Index
T: K -> Type -> Type
W, A, B: Type
w: W
a: A
k: K
C: Type
jc: BatchM (T k B -> C)
D: Type
d: D
map strength_arrow (map (pair d) jc) ⧆ (w, a) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a)
    compose near jc on left.
ix: Index
T: K -> Type -> Type
W, A, B: Type
w: W
a: A
k: K
C: Type
jc: BatchM (T k B -> C)
D: Type
d: D
(map strength_arrow ∘ map (pair d)) jc ⧆ (w, a) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a)
    rewrite (fun_map_map (F:= BatchM)).
ix: Index
T: K -> Type -> Type
W, A, B: Type
w: W
a: A
k: K
C: Type
jc: BatchM (T k B -> C)
D: Type
d: D
map (strength_arrow ∘ pair d) jc ⧆ (w, a) =
map (strength_arrow ∘ pair d) jc ⧆ (w, a)
    reflexivity.
  Qed.

  Lemma mult_BatchM_rw6:
    forall (w1 w2: W) (a1 a2: A) (k: K)
      `(jc: BatchM (T k B -> C)) `(jd: BatchM (T k B -> D)),
      (jc ⧆ (w1, a1)) ⊗ (jd ⧆ (w2, a2)) =
        map (F:= BatchM) strength_arrow ((jc ⧆ (w1, a1)) ⊗ jd) ⧆ (w2, a2).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (w1 w2 : W) (a1 a2 : A) (k : K) (C : Type)
  (jc : BatchM (T k B -> C)) (D : Type)
  (jd : BatchM (T k B -> D)),
(jc ⧆ (w1, a1)) ⊗ (jd ⧆ (w2, a2)) =
map strength_arrow ((jc ⧆ (w1, a1)) ⊗ jd) ⧆ (w2, a2)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (w1 w2 : W) (a1 a2 : A) (k : K) (C : Type)
  (jc : BatchM (T k B -> C)) (D : Type)
  (jd : BatchM (T k B -> D)),
(jc ⧆ (w1, a1)) ⊗ (jd ⧆ (w2, a2)) =
map strength_arrow ((jc ⧆ (w1, a1)) ⊗ jd) ⧆ (w2, a2)
    reflexivity.
  Qed.

  Lemma app_pure_natural_BatchM:
    forall (C D: Type) (f: C -> D) (x: C),
      map (F:= BatchM) f (pure (F:= BatchM) x) =
        pure (F:= BatchM) (f x).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (C D : Type) (f : C -> D) (x : C),
map f (pure x) = pure (f x)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (C D : Type) (f : C -> D) (x : C),
map f (pure x) = pure (f x)
    easy.
  Qed.

  Lemma app_mult_natural_BatchM1:
    forall (C D E: Type) (f: C -> D) (x: BatchM C) (y: BatchM E),
      map (F:= BatchM) f x ⊗ y = map (F:= BatchM) (map_fst f) (x ⊗ y).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (C D E : Type) (f : C -> D) (x : BatchM C)
  (y : BatchM E),
map f x ⊗ y = map (map_fst f) (x ⊗ y)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (C D E : Type) (f : C -> D) (x : BatchM C)
  (y : BatchM E),
map f x ⊗ y = map (map_fst f) (x ⊗ y)
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, C, D, E: Type
f: C -> D
x: BatchM C
y: BatchM E
map f x ⊗ y = map (map_fst f) (x ⊗ y) generalize dependent E.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
forall (E : Type) (y : BatchM E),
map f x ⊗ y = map (map_fst f) (x ⊗ y) induction y.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
c: C0
map f x ⊗ Go c = map (map_fst f) (x ⊗ Go c)
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
p: W * A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
map f x ⊗ (y ⧆ p) = map (map_fst f) (x ⊗ (y ⧆ p))
    -
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
c: C0
map f x ⊗ Go c = map (map_fst f) (x ⊗ Go c) intros; cbn.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
c: C0
map (fun c0 : D => (c0, c)) (map f x) =
map (map_fst f) (map (fun c0 : C => (c0, c)) x) compose near x.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
c: C0
(map (fun c0 : D => (c0, c)) ∘ map f) x =
(map (map_fst f) ∘ map (fun c0 : C => (c0, c))) x
      now do 2 rewrite (fun_map_map (F:= BatchM)).
    -
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
p: W * A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
map f x ⊗ (y ⧆ p) = map (map_fst f) (x ⊗ (y ⧆ p)) destruct p.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
w: W
a: A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
map f x ⊗ (y ⧆ (w, a)) =
map (map_fst f) (x ⊗ (y ⧆ (w, a))) cbn; change (mult_BatchM ?x ?y) with (x ⊗ y).
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
w: W
a: A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
map strength_arrow (map f x ⊗ y) ⧆ (w, a) =
map (compose (map_fst f)) (map strength_arrow (x ⊗ y))
⧆ (w, a)
      rewrite IHy.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
w: W
a: A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
map strength_arrow (map (map_fst f) (x ⊗ y)) ⧆ (w, a) =
map (compose (map_fst f)) (map strength_arrow (x ⊗ y))
⧆ (w, a) compose near (x ⊗ y).
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
w: W
a: A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
(map strength_arrow ∘ map (map_fst f)) (x ⊗ y)
⧆ (w, a) =
(map (compose (map_fst f)) ∘ map strength_arrow)
  (x ⊗ y) ⧆ (w, a)
      do 2 rewrite (fun_map_map (F:= BatchM)).
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
w: W
a: A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
map (strength_arrow ∘ map_fst f) (x ⊗ y) ⧆ (w, a) =
map (compose (map_fst f) ∘ strength_arrow) (x ⊗ y)
⧆ (w, a) do 2 fequal.
ix: Index
T: K -> Type -> Type
W, A, B, C, D: Type
f: C -> D
x: BatchM C
C0: Type
k: K
y: BatchM (T k B -> C0)
w: W
a: A
IHy: map f x ⊗ y = map (map_fst f) (x ⊗ y)
strength_arrow ∘ map_fst f =
compose (map_fst f) ∘ strength_arrow
      now ext [? ?].
  Qed.

  Lemma app_mult_natural_BatchM2:
    forall (A B D: Type) (g: B -> D) (x: BatchM A) (y: BatchM B),
      x ⊗ map (F:= BatchM) g y = map (F:= BatchM) (map_snd g) (x ⊗ y).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B D : Type) (g : B -> D) (x : BatchM A)
  (y : BatchM B),
x ⊗ map g y = map (map_snd g) (x ⊗ y)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B D : Type) (g : B -> D) (x : BatchM A)
  (y : BatchM B),
x ⊗ map g y = map (map_snd g) (x ⊗ y)
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, D: Type
g: B0 -> D
x: BatchM A0
y: BatchM B0
x ⊗ map g y = map (map_snd g) (x ⊗ y) generalize dependent D.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
forall (D : Type) (g : B0 -> D),
x ⊗ map g y = map (map_snd g) (x ⊗ y) induction y as [ANY any | ANY k rest IH [w a]].
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
any: ANY
forall (D : Type) (g : ANY -> D),
x ⊗ map g (Go any) = map (map_snd g) (x ⊗ Go any)
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
forall (D : Type) (g : ANY -> D),
x ⊗ map g (rest ⧆ (w, a)) =
map (map_snd g) (x ⊗ (rest ⧆ (w, a)))
    -
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
any: ANY
forall (D : Type) (g : ANY -> D),
x ⊗ map g (Go any) = map (map_snd g) (x ⊗ Go any) intros; cbn.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
any: ANY
D: Type
g: ANY -> D
map (fun c : A0 => (c, g any)) x =
map (map_snd g) (map (fun c : A0 => (c, any)) x) compose near x on right.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
any: ANY
D: Type
g: ANY -> D
map (fun c : A0 => (c, g any)) x =
(map (map_snd g) ∘ map (fun c : A0 => (c, any))) x now rewrite (fun_map_map (F:= BatchM)).
    -
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
forall (D : Type) (g : ANY -> D),
x ⊗ map g (rest ⧆ (w, a)) =
map (map_snd g) (x ⊗ (rest ⧆ (w, a))) intros; cbn.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
D: Type
g: ANY -> D
map strength_arrow
  (mult_BatchM x (map (compose g) rest)) ⧆ (w, a) =
map (compose (map_snd g))
  (map strength_arrow (mult_BatchM x rest)) ⧆ (w, a) fequal.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
D: Type
g: ANY -> D
map strength_arrow
  (mult_BatchM x (map (compose g) rest)) =
map (compose (map_snd g))
  (map strength_arrow (mult_BatchM x rest))
      change (mult_BatchM ?jx ?jy) with (jx ⊗ jy).
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
D: Type
g: ANY -> D
map strength_arrow (x ⊗ map (compose g) rest) =
map (compose (map_snd g))
  (map strength_arrow (x ⊗ rest))
      rewrite IH.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
D: Type
g: ANY -> D
map strength_arrow
  (map (map_snd (compose g)) (x ⊗ rest)) =
map (compose (map_snd g))
  (map strength_arrow (x ⊗ rest)) compose near (x ⊗ rest).
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
D: Type
g: ANY -> D
(map strength_arrow ∘ map (map_snd (compose g)))
  (x ⊗ rest) =
(map (compose (map_snd g)) ∘ map strength_arrow)
  (x ⊗ rest)
      do 2 rewrite (fun_map_map (F:= BatchM)).
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
D: Type
g: ANY -> D
map (strength_arrow ∘ map_snd (compose g)) (x ⊗ rest) =
map (compose (map_snd g) ∘ strength_arrow) (x ⊗ rest) fequal.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: forall (D : Type) (g : (T k B -> ANY) -> D),
x ⊗ map g rest = map (map_snd g) (x ⊗ rest)
D: Type
g: ANY -> D
strength_arrow ∘ map_snd (compose g) =
compose (map_snd g) ∘ strength_arrow
      now ext [a' mk].
  Qed.

  Lemma app_mult_natural_BatchM:
    forall (A B C D: Type) (f: A -> C) (g: B -> D) (x: BatchM A) (y: BatchM B),
      map (F:= BatchM) f x ⊗ map (F:= BatchM) g y = map (F:= BatchM) (map_tensor f g) (x ⊗ y).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : BatchM A) (y : BatchM B),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : BatchM A) (y : BatchM B),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
x: BatchM A0
y: BatchM B0
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y) rewrite app_mult_natural_BatchM1, app_mult_natural_BatchM2.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
x: BatchM A0
y: BatchM B0
map (map_fst f) (map (map_snd g) (x ⊗ y)) =
map (map_tensor f g) (x ⊗ y)
    compose near (x ⊗ y) on left.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
x: BatchM A0
y: BatchM B0
(map (map_fst f) ∘ map (map_snd g)) (x ⊗ y) =
map (map_tensor f g) (x ⊗ y) rewrite (fun_map_map (F:= BatchM)).
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
x: BatchM A0
y: BatchM B0
map (map_fst f ∘ map_snd g) (x ⊗ y) =
map (map_tensor f g) (x ⊗ y) fequal.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
x: BatchM A0
y: BatchM B0
map_fst f ∘ map_snd g = map_tensor f g
    now ext [a b].
  Qed.

  Lemma app_assoc_BatchM:
    forall (A B C: Type) (x: BatchM A) (y: BatchM B) (z: BatchM C),
      map (F:= BatchM) associator ((x ⊗ y) ⊗ z) = x ⊗ (y ⊗ z).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B C : Type) (x : BatchM A) (y : BatchM B)
  (z : BatchM C),
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B C : Type) (x : BatchM A) (y : BatchM B)
  (z : BatchM C),
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C: Type
x: BatchM A0
y: BatchM B0
z: BatchM C
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z) induction z as [ANY any | ANY k rest IH [w a]].
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
any: ANY
map associator (x ⊗ y ⊗ Go any) = x ⊗ (y ⊗ Go any)
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map associator (x ⊗ y ⊗ (rest ⧆ (w, a))) =
x ⊗ (y ⊗ (rest ⧆ (w, a)))
    -
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
any: ANY
map associator (x ⊗ y ⊗ Go any) = x ⊗ (y ⊗ Go any) do 2 rewrite mult_BatchM_rw2.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
any: ANY
map associator (map (pair_right any) (x ⊗ y)) =
x ⊗ map (pair_right any) y
      rewrite (app_mult_natural_BatchM2).
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
any: ANY
map associator (map (pair_right any) (x ⊗ y)) =
map (map_snd (pair_right any)) (x ⊗ y) compose near (x ⊗ y) on left.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
any: ANY
(map associator ∘ map (pair_right any)) (x ⊗ y) =
map (map_snd (pair_right any)) (x ⊗ y)
      now rewrite (fun_map_map (F:= BatchM)).
    -
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map associator (x ⊗ y ⊗ (rest ⧆ (w, a))) =
x ⊗ (y ⊗ (rest ⧆ (w, a))) cbn.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator)
  (map strength_arrow
     (mult_BatchM (mult_BatchM x y) rest)) ⧆ (w, a) =
map strength_arrow
  (mult_BatchM x
     (map strength_arrow (mult_BatchM y rest)))
⧆ (w, a) repeat change (mult_BatchM ?jx ?jy) with (jx ⊗ jy).
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator)
  (map strength_arrow (x ⊗ y ⊗ rest)) ⧆ (w, a) =
map strength_arrow (x ⊗ map strength_arrow (y ⊗ rest))
⧆ (w, a)
      fequal.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator)
  (map strength_arrow (x ⊗ y ⊗ rest)) =
map strength_arrow (x ⊗ map strength_arrow (y ⊗ rest)) rewrite (app_mult_natural_BatchM2).
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator)
  (map strength_arrow (x ⊗ y ⊗ rest)) =
map strength_arrow
  (map (map_snd strength_arrow) (x ⊗ (y ⊗ rest)))
      rewrite <- IH.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator)
  (map strength_arrow (x ⊗ y ⊗ rest)) =
map strength_arrow
  (map (map_snd strength_arrow)
     (map associator (x ⊗ y ⊗ rest))) compose near (x ⊗ y ⊗ rest).
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
(map (compose associator) ∘ map strength_arrow)
  (x ⊗ y ⊗ rest) =
map strength_arrow
  ((map (map_snd strength_arrow) ∘ map associator)
     (x ⊗ y ⊗ rest))
      do 2 rewrite (fun_map_map (F:= BatchM)).
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator ∘ strength_arrow)
  (x ⊗ y ⊗ rest) =
map strength_arrow
  (map (map_snd strength_arrow ∘ associator)
     (x ⊗ y ⊗ rest))
      compose near (x ⊗ y ⊗ rest) on right.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator ∘ strength_arrow)
  (x ⊗ y ⊗ rest) =
(map strength_arrow
 ∘ map (map_snd strength_arrow ∘ associator))
  (x ⊗ y ⊗ rest)
      rewrite (fun_map_map (F:= BatchM)).
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
map (compose associator ∘ strength_arrow)
  (x ⊗ y ⊗ rest) =
map
  (strength_arrow
   ∘ (map_snd strength_arrow ∘ associator))
  (x ⊗ y ⊗ rest)
      fequal.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
x: BatchM A0
y: BatchM B0
ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map associator (x ⊗ y ⊗ rest) = x ⊗ (y ⊗ rest)
compose associator ∘ strength_arrow =
strength_arrow ∘ (map_snd strength_arrow ∘ associator) now ext [[? ?] ?].
  Qed.

  Lemma app_unital_l_BatchM:
    forall (A: Type) (x: BatchM A),
      map (F:= BatchM) left_unitor (pure (F:= BatchM) tt ⊗ x) = x.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A : Type) (x : BatchM A),
map left_unitor (pure tt ⊗ x) = x
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A : Type) (x : BatchM A),
map left_unitor (pure tt ⊗ x) = x
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
map left_unitor (pure tt ⊗ x) = x induction x as [ANY any | ANY k rest IH [w a]].
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
any: ANY
map left_unitor (pure tt ⊗ Go any) = Go any
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map left_unitor (pure tt ⊗ (rest ⧆ (w, a))) =
rest ⧆ (w, a)
    -
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
any: ANY
map left_unitor (pure tt ⊗ Go any) = Go any easy.
    -
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map left_unitor (pure tt ⊗ (rest ⧆ (w, a))) =
rest ⧆ (w, a) cbn.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map (compose left_unitor)
  (map strength_arrow (mult_BatchM (pure tt) rest))
⧆ (w, a) = rest ⧆ (w, a) change (mult_BatchM ?jx ?jy) with (jx ⊗ jy).
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map (compose left_unitor)
  (map strength_arrow (pure tt ⊗ rest)) ⧆ (w, a) =
rest ⧆ (w, a)
      fequal.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map (compose left_unitor)
  (map strength_arrow (pure tt ⊗ rest)) = rest compose near (pure (F:= BatchM) tt ⊗ rest).
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
(map (compose left_unitor) ∘ map strength_arrow)
  (pure tt ⊗ rest) = rest
      rewrite (fun_map_map (F:= BatchM)).
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map (compose left_unitor ∘ strength_arrow)
  (pure tt ⊗ rest) = rest
      rewrite <- IH.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map (compose left_unitor ∘ strength_arrow)
  (pure tt ⊗ map left_unitor (pure tt ⊗ rest)) =
map left_unitor (pure tt ⊗ rest) repeat fequal.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map left_unitor (pure tt ⊗ rest) = rest
map left_unitor (pure tt ⊗ rest) = rest auto.
  Qed.

  Lemma app_unital_r_BatchM:
    forall (A: Type) (x: BatchM A),
      map (F:= BatchM) right_unitor (x ⊗ pure (F:= BatchM) tt) = x.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A : Type) (x : BatchM A),
map right_unitor (x ⊗ pure tt) = x
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A : Type) (x : BatchM A),
map right_unitor (x ⊗ pure tt) = x
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
map right_unitor (x ⊗ pure tt) = x induction x as [ANY any | ANY k rest IH [w a]].
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
any: ANY
map right_unitor (Go any ⊗ pure tt) = Go any
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map right_unitor (rest ⊗ pure tt) = rest
map right_unitor ((rest ⧆ (w, a)) ⊗ pure tt) =
rest ⧆ (w, a)
    -
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
any: ANY
map right_unitor (Go any ⊗ pure tt) = Go any easy.
    -
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map right_unitor (rest ⊗ pure tt) = rest
map right_unitor ((rest ⧆ (w, a)) ⊗ pure tt) =
rest ⧆ (w, a) cbn in *.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map right_unitor
  (map (fun c : T k B -> ANY => (c, tt)) rest) =
rest
map (compose right_unitor)
  (map (compose (fun c : ANY => (c, tt))) rest)
⧆ (w, a) = rest ⧆ (w, a) fequal.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map right_unitor
  (map (fun c : T k B -> ANY => (c, tt)) rest) =
rest
map (compose right_unitor)
  (map (compose (fun c : ANY => (c, tt))) rest) = rest rewrite <- IH at 2.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map right_unitor
  (map (fun c : T k B -> ANY => (c, tt)) rest) =
rest
map (compose right_unitor)
  (map (compose (fun c : ANY => (c, tt))) rest) =
map right_unitor
  (map (fun c : T k B -> ANY => (c, tt)) rest)
      compose near rest.
ix: Index
T: K -> Type -> Type
W, A, B, ANY: Type
k: K
rest: BatchM (T k B -> ANY)
w: W
a: A
IH: map right_unitor
  (map (fun c : T k B -> ANY => (c, tt)) rest) =
rest
(map (compose right_unitor)
 ∘ map (compose (fun c : ANY => (c, tt)))) rest =
(map right_unitor
 ∘ map (fun c : T k B -> ANY => (c, tt))) rest now do 2 rewrite (fun_map_map (F:= BatchM)).
  Qed.

  Lemma app_mult_pure_BatchM:
    forall (A B: Type) (a: A) (b: B),
      pure (F:= BatchM) a ⊗ pure (F:= BatchM) b = pure (F:= BatchM) (a, b).
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b)
  Proof.
ix: Index
T: K -> Type -> Type
W, A, B: Type
forall (A B : Type) (a : A) (b : B),
pure a ⊗ pure b = pure (a, b)
    intros.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0: Type
a: A0
b: B0
pure a ⊗ pure b = pure (a, b) easy.
  Qed.

  #[global, program] Instance App_Path: Applicative BatchM.

  Next Obligation.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
x: BatchM A0
y: BatchM B0
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y) apply app_mult_natural_BatchM. Qed.
  Next Obligation.
ix: Index
T: K -> Type -> Type
W, A, B, A0, B0, C: Type
x: BatchM A0
y: BatchM B0
z: BatchM C
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z) apply app_assoc_BatchM. Qed.
  Next Obligation.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
map left_unitor (pure tt ⊗ x) = x apply app_unital_l_BatchM. Qed.
  Next Obligation.
ix: Index
T: K -> Type -> Type
W, A, B, A0: Type
x: BatchM A0
map right_unitor (x ⊗ pure tt) = x apply app_unital_r_BatchM. Qed.

End BatchM.

#[global] Arguments Ap {ix} {T}%function_scope
  {W A B}%type_scope {C}%type_scope {k} _ _.
#[local] Infix "⧆":= Ap (at level 51, left associativity): tealeaves_scope.

(** *** Examples of operations *)
(**********************************************************************)
Section demo.

  Context
    `{Index}
    (W: Type)
    (S: Type -> Type)
    `{T: K -> Type -> Type}
    (A B C X: Type)
    (a1 a2: A) (b1 b2 b3: B)
    (w1 w2 w3 w4: W)
    (c1 c2 c3 c4: C)
    (mk1: C -> X) (mk2: C -> C -> X) (mk0: X).

(*
  Check Go a1 ⊗ Go a2: @BatchM _ T W False False (A * A).
  Compute Go a1 ⊗ Go a2.
  Compute Go a1 ⊗ (Go mk1 ⧆ (w1, c1)).
  Compute (Go mk1 ⧆ (w1, c1)) ⊗ (Go mk1 ⧆ (w2, c2)).
  Compute (Go mk2 ⧆ (w1, c1) ⧆ (w2, c2)) ⊗ (Go mk1 ⧆ (w3, c3)).
 *)

End demo.

(** ** Functoriality of [BatchM] *)
(**********************************************************************)
Fixpoint mapfst_BatchM
  `{ix: Index}
  {W: Type}
  {T: K -> Type -> Type}
  {A1 A2 B C} (f: A1 -> A2)
  (j: @BatchM ix T W A1 B C):
  @BatchM ix T W A2 B C :=
  match j with
  | Go a => Go a
  | Ap rest p => Ap (mapfst_BatchM f rest) (map_snd f p)
  end.

(** * Operation <<runBatchM>> *)
(**********************************************************************)
Fixpoint runBatchM
  {ix: Index}
  {T: K -> Type -> Type}
  {W A B: Type} {F: Type -> Type}
  `{Map F} `{Mult F} `{Pure F}
  (ϕ: forall (k: K), W * A -> F (T k B))
  `(j: @BatchM ix T W A B C): F C :=
  match j with
  | Go a => pure a
  | @Ap _ _ _ _ _ _ k rest (pair w a) =>
      runBatchM ϕ rest <⋆> ϕ k (w, a)
  end.

Section runBatchM_rw.

  Context
    `{Index}
    `{Applicative G}
    {A B C: Type}
    `(f: forall (k: K), W * A -> G (T k B)).

  Lemma runBatchM_rw1 (c: C):
    runBatchM f (Go c) = pure c.
H: Index
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B, C, W: Type
T: K -> Type -> Type
f: forall k : K, W * A -> G (T k B)
c: C
runBatchM f (Go c) = pure c
  Proof.
H: Index
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B, C, W: Type
T: K -> Type -> Type
f: forall k : K, W * A -> G (T k B)
c: C
runBatchM f (Go c) = pure c
    reflexivity.
  Qed.

  Lemma runBatchM_rw2 (k: K) (w: W) (a: A) (rest: BatchM (T k B -> C)):
    runBatchM f (rest ⧆ (w, a)) = runBatchM f rest <⋆> f k (w, a).
H: Index
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B, C, W: Type
T: K -> Type -> Type
f: forall k : K, W * A -> G (T k B)
k: K
w: W
a: A
rest: BatchM (T k B -> C)
runBatchM f (rest ⧆ (w, a)) =
runBatchM f rest <⋆> f k (w, a)
  Proof.
H: Index
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B, C, W: Type
T: K -> Type -> Type
f: forall k : K, W * A -> G (T k B)
k: K
w: W
a: A
rest: BatchM (T k B -> C)
runBatchM f (rest ⧆ (w, a)) =
runBatchM f rest <⋆> f k (w, a)
    reflexivity.
  Qed.

End runBatchM_rw.

(** ** Naturality of <<runBatchM>> *)
(**********************************************************************)
Section runBatchM_naturality.

  Context
    `{Index}
    (W: Type)
    (S: Type -> Type)
    `{T: K -> Type -> Type}
    (A B C D: Type)
    `{Applicative G}
    (ϕ: forall k, W * A -> G (T k B)).

  Lemma natural_runBatchM (f: C -> D) (j: @BatchM _ T W A B C):
    map (F := G) f (runBatchM ϕ j) =
      runBatchM ϕ (map (F := BatchM) f j).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
f: C -> D
j: BatchM C
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
  Proof.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
f: C -> D
j: BatchM C
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
    generalize dependent D.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
j: BatchM C
forall (D : Type) (f : C -> D),
map f (runBatchM ϕ j) = runBatchM ϕ (map f j) induction j; intros.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
c: C
D0: Type
f: C -> D0
map f (runBatchM ϕ (Go c)) =
runBatchM ϕ (map f (Go c))
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
p: W * A
IHj: forall (D : Type) (f : (T k B -> C) -> D),
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
D0: Type
f: C -> D0
map f (runBatchM ϕ (j ⧆ p)) =
runBatchM ϕ (map f (j ⧆ p))
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
c: C
D0: Type
f: C -> D0
map f (runBatchM ϕ (Go c)) =
runBatchM ϕ (map f (Go c)) cbn.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
c: C
D0: Type
f: C -> D0
map f (pure c) = pure (f c) now rewrite (app_pure_natural).
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
p: W * A
IHj: forall (D : Type) (f : (T k B -> C) -> D),
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
D0: Type
f: C -> D0
map f (runBatchM ϕ (j ⧆ p)) =
runBatchM ϕ (map f (j ⧆ p)) destruct p.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
w: W
a: A
IHj: forall (D : Type) (f : (T k B -> C) -> D),
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
D0: Type
f: C -> D0
map f (runBatchM ϕ (j ⧆ (w, a))) =
runBatchM ϕ (map f (j ⧆ (w, a))) cbn.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
w: W
a: A
IHj: forall (D : Type) (f : (T k B -> C) -> D),
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
D0: Type
f: C -> D0
map f (runBatchM ϕ j <⋆> ϕ k (w, a)) =
runBatchM ϕ (map (compose f) j) <⋆> ϕ k (w, a) rewrite map_ap.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
w: W
a: A
IHj: forall (D : Type) (f : (T k B -> C) -> D),
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
D0: Type
f: C -> D0
map (compose f) (runBatchM ϕ j) <⋆> ϕ k (w, a) =
runBatchM ϕ (map (compose f) j) <⋆> ϕ k (w, a) fequal.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ϕ: forall k : K, W * A -> G (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
w: W
a: A
IHj: forall (D : Type) (f : (T k B -> C) -> D),
map f (runBatchM ϕ j) = runBatchM ϕ (map f j)
D0: Type
f: C -> D0
map (compose f) (runBatchM ϕ j) =
runBatchM ϕ (map (compose f) j)
      now rewrite IHj.
  Qed.

End runBatchM_naturality.

(** ** <<runBatchM>> as an Applicative Homomorphism *)
(**********************************************************************)
Section runBatchM_morphism.

  Context
    `{Index}
    (W: Type)
    (S: Type -> Type)
    `{T: K -> Type -> Type}
    (A B C D: Type)
    `{Applicative G}
    (f: forall k, W * A -> G (T k B)).

  Lemma appmor_pure_runBatchM:
    forall (C: Type) (c: C),
      runBatchM f (pure (F := BatchM) c) = pure c.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (C : Type) (c : C),
runBatchM f (pure c) = pure c
  Proof.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (C : Type) (c : C),
runBatchM f (pure c) = pure c
    easy.
  Qed.

  Lemma appmor_mult_runBatchM:
    forall (C D: Type) (x: BatchM C) (y: BatchM D),
      runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (C D : Type) (x : BatchM C) (y : BatchM D),
runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y
  Proof.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (C D : Type) (x : BatchM C) (y : BatchM D),
runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y
    intros.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, D0: Type
x: BatchM C0
y: BatchM D0
runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y generalize dependent x.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, D0: Type
y: BatchM D0
forall x : BatchM C0,
runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y induction y.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
c: C1
forall x : BatchM C0,
runBatchM f (x ⊗ Go c) =
runBatchM f x ⊗ runBatchM f (Go c)
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
p: W * A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
forall x : BatchM C0,
runBatchM f (x ⊗ (y ⧆ p)) =
runBatchM f x ⊗ runBatchM f (y ⧆ p)
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
c: C1
forall x : BatchM C0,
runBatchM f (x ⊗ Go c) =
runBatchM f x ⊗ runBatchM f (Go c) intros.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
c: C1
x: BatchM C0
runBatchM f (x ⊗ Go c) =
runBatchM f x ⊗ runBatchM f (Go c) rewrite mult_BatchM_rw2.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
c: C1
x: BatchM C0
runBatchM f (map (pair_right c) x) =
runBatchM f x ⊗ runBatchM f (Go c)
      rewrite runBatchM_rw1.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
c: C1
x: BatchM C0
runBatchM f (map (pair_right c) x) =
runBatchM f x ⊗ pure c rewrite triangle_4.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
c: C1
x: BatchM C0
runBatchM f (map (pair_right c) x) =
map (fun b : C0 => (b, c)) (runBatchM f x)
      rewrite natural_runBatchM; auto.
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
p: W * A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
forall x : BatchM C0,
runBatchM f (x ⊗ (y ⧆ p)) =
runBatchM f x ⊗ runBatchM f (y ⧆ p) intros.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
p: W * A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ p)) =
runBatchM f x ⊗ runBatchM f (y ⧆ p) destruct p.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
runBatchM f x ⊗ runBatchM f (y ⧆ (w, a)) rewrite runBatchM_rw2.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
runBatchM f x ⊗ (runBatchM f y <⋆> f k (w, a))
      unfold ap.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
runBatchM f x
⊗ map (fun '(f, a) => f a)
    (runBatchM f y ⊗ f k (w, a)) rewrite (app_mult_natural_r G).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
map (map_snd (fun '(f, a) => f a))
  (runBatchM f x ⊗ (runBatchM f y ⊗ f k (w, a)))
      rewrite <- (app_assoc).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
map (map_snd (fun '(f, a) => f a))
  (map associator
     (runBatchM f x ⊗ runBatchM f y ⊗ f k (w, a)))
      rewrite <- IHy.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
IHy: forall x : BatchM C0,
runBatchM f (x ⊗ y) =
runBatchM f x ⊗ runBatchM f y
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
map (map_snd (fun '(f, a) => f a))
  (map associator (runBatchM f (x ⊗ y) ⊗ f k (w, a))) clear IHy.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
map (map_snd (fun '(f, a) => f a))
  (map associator (runBatchM f (x ⊗ y) ⊗ f k (w, a)))
      compose near (runBatchM f (x ⊗ y) ⊗ f k (w, a)).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
(map (map_snd (fun '(f, a) => f a)) ∘ map associator)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a))
      rewrite (fun_map_map).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
runBatchM f (x ⊗ (y ⧆ (w, a))) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a))
      cbn.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
runBatchM f (map strength_arrow (mult_BatchM x y)) <⋆>
f k (w, a) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (mult_BatchM x y) ⊗ f k (w, a)) unfold ap.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
map (fun '(f, a) => f a)
  (runBatchM f (map strength_arrow (mult_BatchM x y))
   ⊗ f k (w, a)) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (mult_BatchM x y) ⊗ f k (w, a)) change (mult_BatchM ?jx ?jy) with (jx ⊗ jy).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
map (fun '(f, a) => f a)
  (runBatchM f (map strength_arrow (x ⊗ y))
   ⊗ f k (w, a)) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a))
      rewrite <- natural_runBatchM; auto.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
map (fun '(f, a) => f a)
  (map strength_arrow (runBatchM f (x ⊗ y))
   ⊗ f k (w, a)) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a))
      rewrite (app_mult_natural_l G).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
map (fun '(f, a) => f a)
  (map (map_fst strength_arrow)
     (runBatchM f (x ⊗ y) ⊗ f k (w, a))) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a))
      compose near (runBatchM f (x ⊗ y) ⊗ f k (w, a)) on left.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
(map (fun '(f, a) => f a)
 ∘ map (map_fst strength_arrow))
  (runBatchM f (x ⊗ y) ⊗ f k (w, a)) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a))
      rewrite (fun_map_map).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
map ((fun '(f, a) => f a) ∘ map_fst strength_arrow)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a)) =
map (map_snd (fun '(f, a) => f a) ∘ associator)
  (runBatchM f (x ⊗ y) ⊗ f k (w, a)) fequal.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
C0, C1: Type
k: K
y: BatchM (T k B -> C1)
w: W
a: A
x: BatchM C0
(fun '(f, a) => f a) ∘ map_fst strength_arrow =
map_snd (fun '(f, a) => f a) ∘ associator now ext [[? ?] ?].
  Qed.

  #[global] Instance Morphism_store_fold:
    ApplicativeMorphism BatchM G
      (@runBatchM _ T W A B G _ _ _ f).
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
ApplicativeMorphism BatchM G
  (@runBatchM H T W A B G Map_G Mult_G Pure_G f)
  Proof.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
ApplicativeMorphism BatchM G
  (@runBatchM H T W A B G Map_G Mult_G Pure_G f)
    constructor; try typeclasses eauto.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (A0 B0 : Type) (f0 : A0 -> B0) (x : BatchM A0),
runBatchM f (map f0 x) = map f0 (runBatchM f x)
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (A0 : Type) (a : A0),
runBatchM f (pure a) = pure a
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (A0 B0 : Type) (x : BatchM A0) (y : BatchM B0),
runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (A0 B0 : Type) (f0 : A0 -> B0) (x : BatchM A0),
runBatchM f (map f0 x) = map f0 (runBatchM f x) intros.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
A0, B0: Type
f0: A0 -> B0
x: BatchM A0
runBatchM f (map f0 x) = map f0 (runBatchM f x) now rewrite natural_runBatchM.
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (A0 : Type) (a : A0),
runBatchM f (pure a) = pure a intros.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
A0: Type
a: A0
runBatchM f (pure a) = pure a easy.
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
forall (A0 B0 : Type) (x : BatchM A0) (y : BatchM B0),
runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y intros.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
f: forall k : K, W * A -> G (T k B)
A0, B0: Type
x: BatchM A0
y: BatchM B0
runBatchM f (x ⊗ y) = runBatchM f x ⊗ runBatchM f y apply appmor_mult_runBatchM.
  Qed.

End runBatchM_morphism.

(** ** <<runBatchM>> commutes with Applicative Homomorphisms **)
(**********************************************************************)
Section runBatchM_morphism.


  #[local] Generalizable All Variables.

  Context

    `{Index}
    (W: Type)
    (S: Type -> Type)
    `{T: K -> Type -> Type}
    (A B C D: Type)
    `{Applicative G1}
    `{Applicative G2}
    `{! ApplicativeMorphism G1 G2 ψ}
    (f: forall k, W * A -> G1 (T k B)).

  Lemma runBatchM_morphism `(j: @BatchM _ T W A B C):
    @ψ C (runBatchM f j) = runBatchM (fun k => @ψ (T k B) ∘ f k) j.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
j: BatchM C
ψ (runBatchM f j) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j
  Proof.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, C, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
j: BatchM C
ψ (runBatchM f j) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j
    induction j.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
c: C
ψ (runBatchM f (Go c)) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) (Go c)
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
p: W * A
IHj: ψ (runBatchM f j) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j
ψ (runBatchM f (j ⧆ p)) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) (j ⧆ p)
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
c: C
ψ (runBatchM f (Go c)) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) (Go c) cbn.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
c: C
ψ (pure c) = pure c now rewrite (appmor_pure).
    -
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
p: W * A
IHj: ψ (runBatchM f j) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j
ψ (runBatchM f (j ⧆ p)) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) (j ⧆ p) destruct p.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
w: W
a: A
IHj: ψ (runBatchM f j) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j
ψ (runBatchM f (j ⧆ (w, a))) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k)
  (j ⧆ (w, a)) cbn.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
w: W
a: A
IHj: ψ (runBatchM f j) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j
ψ (runBatchM f j <⋆> f k (w, a)) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j <⋆>
(ψ (A:=T k B) ∘ f k) (w, a) rewrite ap_morphism_1.
H: Index
W: Type
S: Type -> Type
T: K -> Type -> Type
A, B, D: Type
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H1: Applicative G2
ψ: forall A : Type, G1 A -> G2 A
ApplicativeMorphism0: ApplicativeMorphism G1 G2 ψ
f: forall k : K, W * A -> G1 (T k B)
C: Type
k: K
j: BatchM (T k B -> C)
w: W
a: A
IHj: ψ (runBatchM f j) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j
ψ (runBatchM f j) <⋆> ψ (f k (w, a)) =
runBatchM (fun k : K => ψ (A:=T k B) ∘ f k) j <⋆>
(ψ (A:=T k B) ∘ f k) (w, a)
      now rewrite IHj.
  Qed.

End runBatchM_morphism.

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