From Tealeaves Require Export
  Classes.Categorical.Applicative
  Classes.Categorical.Monad (Return, ret)
  Classes.Categorical.Comonad (Extract, extract)
  Functors.Early.Batch
  Functors.Early.Reader.

Import Batch.Notations.
Import Product.Notations.
Import Applicative.Notations.

#[local] Generalizable Variables E T A B.

(** * Coalgebraic Decorated Traversable Functors *)
(**********************************************************************)

(** ** The <<toBatch3>> Operation *)
(**********************************************************************)
Class ToBatch3 (E: Type) (T: Type -> Type) :=
  toBatch3: forall A B, T A -> Batch (E * A) B (T B).

#[global] Arguments toBatch3 {E}%type_scope {T}%function_scope
  {ToBatch3} {A B}%type_scope _.

(** ** Operation <<cojoin_Batch3>> *)
(**********************************************************************)
Fixpoint cojoin_Batch3 `{ToBatch3 E T} {A B B' C: Type}
  (b: Batch (E * A) B C): Batch (E * A) B' (Batch (E * B') B C) :=
  match b with
  | Done c => Done (Done c)
  | Step rest (*:Batch (E * A) B (B -> C)*) (e, a)(*:E*A*) =>
      Step (map (F := Batch (E * A) B')
              (fun (continue: Batch (E * B') B (B -> C))
                 (b': B') =>
                 Step continue (e, b')
              ) (cojoin_Batch3 rest:
                Batch (E * A) B' (Batch (E * B') B (B -> C))))
        ((e, a): E * A)
  end.

(** ** <<cojoin_Batch3>> as <<runBatch double_batch3>> *)
(**********************************************************************)
Section section.

  Context
    `{ToBatch3 E T}.

  Definition double_batch3 {A B: Type} (C: Type):
    E * A -> (Batch (E * A) B ∘ Batch (E * B) C) C :=
    fun '(e, a) => (map (F := Batch (E * A) B)
                   (batch (E * B) C ∘ pair e) ∘ batch (E * A) B) (e, a).

  Lemma double_batch3_rw {A B C: Type}:
    forall '(e, a),
      @double_batch3 A B C (e, a) =
        Done (batch (E * B) C ∘ pair e) ⧆ (e, a).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
forall '(e, a),
double_batch3 C (e, a) =
Done (batch (E * B) C ∘ pair e) ⧆ (e, a)
  Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
forall '(e, a),
double_batch3 C (e, a) =
Done (batch (E * B) C ∘ pair e) ⧆ (e, a)
    intros [e a].
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
e: E
a: A
double_batch3 C (e, a) =
Done (batch (E * B) C ∘ pair e) ⧆ (e, a)
    reflexivity.
  Qed.

  Lemma cojoin_Batch3_to_runBatch: forall (A B B': Type),
      (@cojoin_Batch3 E T _ A B B') =
        (fun C => runBatch (G := Batch (E * A) B' ∘ Batch (E * B') _)
                 (double_batch3 B)).
E: Type
T: Type -> Type
H: ToBatch3 E T
forall A B B' : Type,
@cojoin_Batch3 E T H A B B' =
(fun C : Type => runBatch (double_batch3 B))
  Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
forall A B B' : Type,
@cojoin_Batch3 E T H A B B' =
(fun C : Type => runBatch (double_batch3 B))
    intros.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B': Type
@cojoin_Batch3 E T H A B B' =
(fun C : Type => runBatch (double_batch3 B)) ext C b.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
b: Batch (E * A) B C
cojoin_Batch3 b = runBatch (double_batch3 B) b
    induction b as [C c | C rest IHrest [e a]].
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
c: C
cojoin_Batch3 (Done c) =
runBatch (double_batch3 B) (Done c)
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
cojoin_Batch3 (rest ⧆ (e, a)) =
runBatch (double_batch3 B) (rest ⧆ (e, a))
    -
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
c: C
cojoin_Batch3 (Done c) =
runBatch (double_batch3 B) (Done c) cbn.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
c: C
Done (Done c) = pure c reflexivity.
    -
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
cojoin_Batch3 (rest ⧆ (e, a)) =
runBatch (double_batch3 B) (rest ⧆ (e, a)) cbn.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
map
  (fun continue : Batch (E * B') B (B -> C) =>
   Step continue ○ pair e) (cojoin_Batch3 rest)
⧆ (e, a) =
map (compose (map (fun '(f, a) => f a)))
  (map (compose mult)
     (map strength_arrow
        (map
           (fun c : Batch (E * B') B (B -> C) =>
            (c, batch (E * B') B ∘ pair e ∘ id))
           (runBatch (double_batch3 B) rest))))
⧆ (e, a)
      do 3 compose near ((runBatch (double_batch3 (B := B') B) rest)).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
map
  (fun continue : Batch (E * B') B (B -> C) =>
   Step continue ○ pair e) (cojoin_Batch3 rest)
⧆ (e, a) =
(map (compose (map (fun '(f, a) => f a)))
 ∘ (map (compose mult)
    ∘ (map strength_arrow
       ∘ map
           (fun c : Batch (E * B') B (B -> C) =>
            (c, batch (E * B') B ∘ pair e ∘ id)))))
  (runBatch (double_batch3 B) rest) ⧆ (e, a)
      do 3 rewrite (fun_map_map (F := Batch (E * A) B')).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
map
  (fun continue : Batch (E * B') B (B -> C) =>
   Step continue ○ pair e) (cojoin_Batch3 rest)
⧆ (e, a) =
map
  (compose (map (fun '(f, a) => f a))
   ∘ (compose mult
      ∘ (strength_arrow
         ∘ (fun c : Batch (E * B') B (B -> C) =>
            (c, batch (E * B') B ∘ pair e ∘ id)))))
  (runBatch (double_batch3 B) rest) ⧆ (e, a)
      fequal.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
map
  (fun continue : Batch (E * B') B (B -> C) =>
   Step continue ○ pair e) (cojoin_Batch3 rest) =
map
  (compose (map (fun '(f, a) => f a))
   ∘ (compose mult
      ∘ (strength_arrow
         ∘ (fun c : Batch (E * B') B (B -> C) =>
            (c, batch (E * B') B ∘ pair e ∘ id)))))
  (runBatch (double_batch3 B) rest)
      rewrite IHrest.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
map
  (fun continue : Batch (E * B') B (B -> C) =>
   Step continue ○ pair e)
  (runBatch (double_batch3 B) rest) =
map
  (compose (map (fun '(f, a) => f a))
   ∘ (compose mult
      ∘ (strength_arrow
         ∘ (fun c : Batch (E * B') B (B -> C) =>
            (c, batch (E * B') B ∘ pair e ∘ id)))))
  (runBatch (double_batch3 B) rest)
      fequal.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
(fun continue : Batch (E * B') B (B -> C) =>
 Step continue ○ pair e) =
compose (map (fun '(f, a) => f a))
∘ (compose mult
   ∘ (strength_arrow
      ∘ (fun c : Batch (E * B') B (B -> C) =>
         (c, batch (E * B') B ∘ pair e ∘ id))))
      ext b x.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b ⧆ (e, x) =
(compose (map (fun '(f, a) => f a))
 ∘ (compose mult
    ∘ (strength_arrow
       ∘ (fun c : Batch (E * B') B (B -> C) =>
          (c, batch (E * B') B ∘ pair e ∘ id))))) b x unfold compose.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b ⧆ (e, x) =
map (fun '(f, a) => f a)
  (mult
     (strength_arrow
        (b, fun a : B' => batch (E * B') B (e, id a))
        x))
      cbn.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b ⧆ (e, x) =
map (compose (fun '(f, a) => f a))
  (map strength_arrow
     (map (fun c : B -> C => (c, id)) b)) ⧆ (e, id x)
      compose near b.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b ⧆ (e, x) =
map (compose (fun '(f, a) => f a))
  ((map strength_arrow
    ∘ map (fun c : B -> C => (c, id))) b) ⧆ (e, id x)
      rewrite (fun_map_map).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b ⧆ (e, x) =
map (compose (fun '(f, a) => f a))
  (map (strength_arrow ∘ (fun c : B -> C => (c, id)))
     b) ⧆ (e, id x)
      compose near b.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b ⧆ (e, x) =
(map (compose (fun '(f, a) => f a))
 ∘ map (strength_arrow ∘ (fun c : B -> C => (c, id))))
  b ⧆ (e, id x)
      rewrite (fun_map_map).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b ⧆ (e, x) =
map
  (compose (fun '(f, a) => f a)
   ∘ (strength_arrow ∘ (fun c : B -> C => (c, id)))) b
⧆ (e, id x)
      fequal.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b =
map
  (compose (fun '(f, a) => f a)
   ∘ (strength_arrow ∘ (fun c : B -> C => (c, id)))) b
      unfold compose, strength_arrow.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b =
map (fun a : B -> C => fst (a, id) ○ snd (a, id)) b
      rewrite (fun_map_id).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, B', C: Type
rest: Batch (E * A) B (B -> C)
e: E
a: A
IHrest: cojoin_Batch3 rest =
runBatch (double_batch3 B) rest
b: Batch (E * B') B (B -> C)
x: B'
b = id b
      reflexivity.
  Qed.

  Lemma cojoin_Batch3_batch: forall (A B C: Type),
      cojoin_Batch3 (B' := B) ∘ batch (E * A) C =
        double_batch3 C.
E: Type
T: Type -> Type
H: ToBatch3 E T
forall A B C : Type,
cojoin_Batch3 ∘ batch (E * A) C = double_batch3 C
  Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
forall A B C : Type,
cojoin_Batch3 ∘ batch (E * A) C = double_batch3 C
    intros.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
cojoin_Batch3 ∘ batch (E * A) C = double_batch3 C
    rewrite (cojoin_Batch3_to_runBatch).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
runBatch (double_batch3 C) ∘ batch (E * A) C =
double_batch3 C
    pose (runBatch_batch).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
e:= runBatch_batch: forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : A -> G B),
runBatch f ∘ batch A B = f
runBatch (double_batch3 C) ∘ batch (E * A) C =
double_batch3 C
    specialize (e ((Batch (E * A) B ∘ Batch (E * B) C))
                  _ _ _ _).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
e: forall (A0 B0 : Type)
  (f : A0 ->
       (Batch (E * A) B ∘ Batch (E * B) C) B0),
runBatch f ∘ batch A0 B0 = f
runBatch (double_batch3 C) ∘ batch (E * A) C =
double_batch3 C
    specialize (e (E * A) C).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
e: forall
  f : E * A ->
      (Batch (E * A) B ∘ Batch (E * B) C) C,
runBatch f ∘ batch (E * A) C = f
runBatch (double_batch3 C) ∘ batch (E * A) C =
double_batch3 C
    specialize (e (double_batch3 C)).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
e: runBatch (double_batch3 C) ∘ batch (E * A) C =
double_batch3 C
runBatch (double_batch3 C) ∘ batch (E * A) C =
double_batch3 C
    apply e.
  Qed.

  #[export] Instance ApplicativeMorphism_cojoin_Batch3:
    forall (A B C: Type),
      ApplicativeMorphism (Batch (E * A) C)
        (Batch (E * A) B ∘ Batch (E * B) C)
        (@cojoin_Batch3 E _ _ A C B).
E: Type
T: Type -> Type
H: ToBatch3 E T
forall A B C : Type,
ApplicativeMorphism (Batch (E * A) C)
  (Batch (E * A) B ∘ Batch (E * B) C)
  (@cojoin_Batch3 E T H A C B)
  Proof.
E: Type
T: Type -> Type
H: ToBatch3 E T
forall A B C : Type,
ApplicativeMorphism (Batch (E * A) C)
  (Batch (E * A) B ∘ Batch (E * B) C)
  (@cojoin_Batch3 E T H A C B)
    intros.
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
ApplicativeMorphism (Batch (E * A) C)
  (Batch (E * A) B ∘ Batch (E * B) C)
  (@cojoin_Batch3 E T H A C B)
    rewrite (@cojoin_Batch3_to_runBatch A C B).
E: Type
T: Type -> Type
H: ToBatch3 E T
A, B, C: Type
ApplicativeMorphism (Batch (E * A) C)
  (Batch (E * A) B ∘ Batch (E * B) C)
  (fun C0 : Type => runBatch (double_batch3 C))
    apply ApplicativeMorphism_runBatch.
  Qed.

End section.

(** ** Typeclass *)
(**********************************************************************)
Class DecoratedTraversableFunctor
  (E: Type)
  (T: Type -> Type)
  `{ToBatch3 E T} :=
  { dtf_extract: forall (A: Type),
      extract_Batch ∘ mapfst_Batch (extract (W := (E ×))) ∘
        toBatch3 = @id (T A);
    dtf_duplicate: forall (A B C: Type),
      cojoin_Batch3 ∘ toBatch3 (A := A) (B := C) =
        map (F := Batch (E * A) B) (toBatch3) ∘ toBatch3;
  }.