From Tealeaves Require Import
  Classes.Kleisli.DecoratedTraversableFunctor
  Classes.Coalgebraic.DecoratedTraversableFunctor.

Import Product.Notations.
Import Kleisli.DecoratedTraversableFunctor.Notations.
Import Batch.Notations.
Import Monoid.Notations.

#[local] Generalizable Variables E G T M A B.

#[local] Arguments batch {A} (B)%type_scope _.


(** * Coalgebraic DTFs from Kleisli DTFs *)
(**********************************************************************)

(** ** Derived Operations *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance ToBatch3_Mapdt `{Mapdt E T}
: Coalgebraic.DecoratedTraversableFunctor.ToBatch3 E T :=
  (fun A B => mapdt (G := Batch (E * A) B) (batch B):
     T A -> Batch (E * A) B (T B)).

End DerivedOperations.

Class Compat_ToBatch3_Mapdt
  (E: Type)
  (T: Type -> Type)
  `{Mapdt_inst: Mapdt E T}
  `{ToBatch3_inst: ToBatch3 E T} :=
  compat_toBatch3_mapdt:
    ToBatch3_inst = DerivedOperations.ToBatch3_Mapdt.

Lemma toBatch3_to_mapdt
  `{Compat_ToBatch3_Mapdt E T}:
  forall (A B: Type),
    toBatch3 (E := E) (T := T) =
      mapdt (G := Batch (E * A) B) (batch B).
E: Type
T: Type -> Type
Mapdt_inst: Mapdt E T
ToBatch3_inst: ToBatch3 E T
H: Compat_ToBatch3_Mapdt E T
forall A B : Type, toBatch3 = mapdt (batch B)
Proof.
E: Type
T: Type -> Type
Mapdt_inst: Mapdt E T
ToBatch3_inst: ToBatch3 E T
H: Compat_ToBatch3_Mapdt E T
forall A B : Type, toBatch3 = mapdt (batch B)
  intros.
E: Type
T: Type -> Type
Mapdt_inst: Mapdt E T
ToBatch3_inst: ToBatch3 E T
H: Compat_ToBatch3_Mapdt E T
A, B: Type
toBatch3 = mapdt (batch B)
  rewrite compat_toBatch3_mapdt.
E: Type
T: Type -> Type
Mapdt_inst: Mapdt E T
ToBatch3_inst: ToBatch3 E T
H: Compat_ToBatch3_Mapdt E T
A, B: Type
DerivedOperations.ToBatch3_Mapdt A B = mapdt (batch B)
  reflexivity.
Qed.

#[export] Instance Compat_ToBatch3_Mapdt_Self
  `{Mapdt E T}:
  Compat_ToBatch3_Mapdt E T
    (ToBatch3_inst := DerivedOperations.ToBatch3_Mapdt)
  := ltac:(hnf; reflexivity).

Module DerivedInstances.

  Import DerivedOperations.

  Section to_coalgebraic.

    Context
      `{Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T}
      `{ToBatch3 E T}
      `{! Compat_ToBatch3_Mapdt E T}.

    (** ** <<double_batch3>> as <<batch ⋆3 batch>> *)
    (******************************************************************)
    Lemma double_Batch3_spec: forall A B C,
        double_batch3 (E := E) (A := A) (B := B) C =
          batch C ⋆3 batch B.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
forall A B C : Type,
double_batch3 C = batch C ⋆3 batch B
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
forall A B C : Type,
double_batch3 C = batch C ⋆3 batch B
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
double_batch3 C = batch C ⋆3 batch B unfold double_batch3.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
(fun '(e, a) =>
 (map (batch C ∘ pair e) ∘ batch B) (e, a)) =
batch C ⋆3 batch B now ext [e a].
    Qed.

    (** ** Derived Laws *)
    (******************************************************************)
    Lemma toBatch3_extract_Kleisli: forall (A: Type),
        extract_Batch ∘ mapfst_Batch (extract (W := (E ×))) ∘ toBatch3 =
          @id (T A).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
forall A : Type,
extract_Batch ∘ mapfst_Batch extract ∘ toBatch3 = id
    Proof.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
forall A : Type,
extract_Batch ∘ mapfst_Batch extract ∘ toBatch3 = id
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
extract_Batch ∘ mapfst_Batch extract ∘ toBatch3 = id
      reassociate -> on left.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
extract_Batch ∘ (mapfst_Batch extract ∘ toBatch3) = id
      rewrite toBatch3_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
extract_Batch
∘ (mapfst_Batch extract ∘ mapdt (batch A)) = id
      rewrite (kdtf_morph (T := T)
                 (morphism := ApplicativeMorphism_mapfst_Batch
                                (extract (W := prod E) (A := A)))
                 (batch A)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
extract_Batch ∘ mapdt (mapfst_Batch extract ∘ batch A) =
id
      rewrite (kdtf_morph
                 (G1 := Batch A A)
                 (G2 := fun A => A)
                 (morphism := ApplicativeMorphism_extract_Batch _)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
mapdt
  (extract_Batch ∘ (mapfst_Batch extract ∘ batch A)) =
id
      reassociate <- on left.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
mapdt (extract_Batch ∘ mapfst_Batch extract ∘ batch A) =
id
      assert (cut: extract_Batch ∘ mapfst_Batch extract ∘ batch A
                   =  extract (W := (E ×))).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
extract_Batch ∘ mapfst_Batch extract ∘ batch A =
extract
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
cut: extract_Batch ∘ mapfst_Batch extract ∘ batch A =
extract
mapdt (extract_Batch ∘ mapfst_Batch extract ∘ batch A) =
id
      {
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
extract_Batch ∘ mapfst_Batch extract ∘ batch A =
extract ext [e a].
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
e: E
a: A
(extract_Batch ∘ mapfst_Batch extract ∘ batch A)
  (e, a) = extract (e, a) reflexivity. }
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
cut: extract_Batch ∘ mapfst_Batch extract ∘ batch A =
extract
mapdt (extract_Batch ∘ mapfst_Batch extract ∘ batch A) =
id
      rewrite cut.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
cut: extract_Batch ∘ mapfst_Batch extract ∘ batch A =
extract
mapdt extract = id
      rewrite kdtf_mapdt1.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A: Type
cut: extract_Batch ∘ mapfst_Batch extract ∘ batch A =
extract
id = id
      reflexivity.
    Qed.

    Lemma toBatch3_duplicate_Kleisli: forall (A B C: Type),
        cojoin_Batch3 ∘ toBatch3 (A := A) (B := C) =
          map (F := Batch (E * A) B) (toBatch3) ∘ toBatch3.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
forall A B C : Type,
cojoin_Batch3 ∘ toBatch3 = map toBatch3 ∘ toBatch3
      intros.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
cojoin_Batch3 ∘ toBatch3 = map toBatch3 ∘ toBatch3
      rewrite toBatch3_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
cojoin_Batch3 ∘ mapdt (batch C) =
map toBatch3 ∘ toBatch3
      rewrite (kdtf_morph (T := T) (E := E) (B := C)
                 (G1 := Batch (E * A) C)
                 (G2 := Batch (E * A) B ∘ Batch (E * B) C)
                 (morphism := ApplicativeMorphism_cojoin_Batch3 _ _ _)
                 (ϕ := @cojoin_Batch3 E _ _ A C B)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
mapdt (cojoin_Batch3 ∘ batch C) =
map toBatch3 ∘ toBatch3
      rewrite toBatch3_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
mapdt (cojoin_Batch3 ∘ batch C) =
map (mapdt (batch C)) ∘ toBatch3
      rewrite toBatch3_to_mapdt.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
mapdt (cojoin_Batch3 ∘ batch C) =
map (mapdt (batch C)) ∘ mapdt (batch B)
      rewrite (kdtf_mapdt2 _ _).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
mapdt (cojoin_Batch3 ∘ batch C) =
mapdt (batch C ⋆3 batch B)
      rewrite <- double_Batch3_spec.
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
mapdt (cojoin_Batch3 ∘ batch C) =
mapdt (double_batch3 C)
      rewrite <- (cojoin_Batch3_batch (E := E) (T := T)).
E: Type
T: Type -> Type
H: Mapdt E T
H0: Kleisli.DecoratedTraversableFunctor.DecoratedTraversableFunctor
  E T
H1: ToBatch3 E T
Compat_ToBatch3_Mapdt0: Compat_ToBatch3_Mapdt E T
A, B, C: Type
mapdt (cojoin_Batch3 ∘ batch C) =
mapdt (cojoin_Batch3 ∘ batch C)
      reflexivity.
    Qed.

    #[export] Instance Coalgebraic_DecoratedTraversableFunctor_of_Kleisli:
      Coalgebraic.DecoratedTraversableFunctor.DecoratedTraversableFunctor E T :=
      {| dtf_extract := toBatch3_extract_Kleisli;
         dtf_duplicate := toBatch3_duplicate_Kleisli;
      |}.

  End to_coalgebraic.

End DerivedInstances.