From Tealeaves Require Import
  Functors.Early.Batch
  Classes.Kleisli.TraversableFunctor
  Classes.Coalgebraic.TraversableFunctor.

Import Batch.Notations.
Import Kleisli.TraversableFunctor.Notations.

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

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

(** * Coalgebraic Traversable Functors From Kleisli Traversable Functors *)
(**********************************************************************)

(** ** Derived <<ToBatch>> Operation *)
(**********************************************************************)
Module DerivedOperations.

  #[export] Instance ToBatch_Traverse `{Traverse T}:
  Coalgebraic.TraversableFunctor.ToBatch T :=
  (fun A B => traverse (G := Batch A B) (batch B):
     T A -> Batch A B (T B)).

End DerivedOperations.

Class Compat_ToBatch_Traverse
  (T: Type -> Type)
  `{Traverse_inst: Traverse T}
  `{ToBatch_inst: ToBatch T} :=
  compat_toBatch_traverse:
    ToBatch_inst = DerivedOperations.ToBatch_Traverse.

Lemma toBatch_to_traverse
  `{Compat_ToBatch_Traverse T}:
  forall A B, toBatch (T := T) =
           traverse (G := Batch A B) (batch B).
T: Type -> Type
Traverse_inst: Traverse T
ToBatch_inst: ToBatch T
H: Compat_ToBatch_Traverse T
forall A B : Type, toBatch = traverse (batch B)
Proof.
T: Type -> Type
Traverse_inst: Traverse T
ToBatch_inst: ToBatch T
H: Compat_ToBatch_Traverse T
forall A B : Type, toBatch = traverse (batch B)
  intros.
T: Type -> Type
Traverse_inst: Traverse T
ToBatch_inst: ToBatch T
H: Compat_ToBatch_Traverse T
A, B: Type
toBatch = traverse (batch B)
  rewrite compat_toBatch_traverse.
T: Type -> Type
Traverse_inst: Traverse T
ToBatch_inst: ToBatch T
H: Compat_ToBatch_Traverse T
A, B: Type
DerivedOperations.ToBatch_Traverse A B =
traverse (batch B)
  reflexivity.
Qed.

#[export] Instance Compat_ToBatch_Traverse_Self
  `{Traverse T}: Compat_ToBatch_Traverse T
                   (ToBatch_inst := DerivedOperations.ToBatch_Traverse)
  := ltac:(hnf; reflexivity).

(** ** Derived Laws *)
(**********************************************************************)
Module DerivedInstances.
  Section instances.


    Context
      `{Traverse T}
      `{ToBatch T}
      `{! Kleisli.TraversableFunctor.TraversableFunctor T}
      `{! Compat_ToBatch_Traverse T}.

    (** *** Coalgebra laws *)
    (******************************************************************)
    Lemma toBatch_extract_Kleisli: forall (A: Type),
        extract_Batch ∘ toBatch = @id (T A).
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A : Type, extract_Batch ∘ toBatch = id
    Proof.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A : Type, extract_Batch ∘ toBatch = id
      intros.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
extract_Batch ∘ toBatch = id
      rewrite toBatch_to_traverse.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
extract_Batch ∘ traverse (batch A) = id
      rewrite (trf_traverse_morphism (ϕ := @extract_Batch A)).
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
traverse (extract_Batch ∘ batch A) = id
      rewrite extract_Batch_batch.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
traverse id = id
      rewrite trf_traverse_id.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A: Type
id = id
      reflexivity.
    Qed.

    Lemma toBatch_duplicate_Kleisli: forall (A B C: Type),
        cojoin_Batch ∘ toBatch =
          map (F := Batch A B) (toBatch (A' := C)) ∘ toBatch (A' := B).
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A B C : Type,
cojoin_Batch ∘ toBatch = map toBatch ∘ toBatch
    Proof.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
forall A B C : Type,
cojoin_Batch ∘ toBatch = map toBatch ∘ toBatch
      intros.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, C: Type
cojoin_Batch ∘ toBatch = map toBatch ∘ toBatch
      rewrite toBatch_to_traverse.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, C: Type
cojoin_Batch ∘ traverse (batch C) =
map toBatch ∘ toBatch
      rewrite (trf_traverse_morphism (ϕ := @cojoin_Batch A B C)).
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, C: Type
traverse (cojoin_Batch ∘ batch C) =
map toBatch ∘ toBatch
      rewrite cojoin_Batch_batch.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, C: Type
traverse double_batch = map toBatch ∘ toBatch
      rewrite toBatch_to_traverse.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, C: Type
traverse double_batch =
map (traverse (batch C)) ∘ toBatch
      rewrite toBatch_to_traverse.
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, C: Type
traverse double_batch =
map (traverse (batch C)) ∘ traverse (batch B)
      rewrite (trf_traverse_traverse
                 (G1 := Batch A B) (G2 := Batch B C)).
T: Type -> Type
H: Traverse T
H0: ToBatch T
H1: Kleisli.TraversableFunctor.TraversableFunctor T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
A, B, C: Type
traverse double_batch = traverse (batch C ⋆2 batch B)
      reflexivity.
    Qed.

    #[export] Instance Coalgebraic_Traversable_of_Kleisli:
      Coalgebraic.TraversableFunctor.TraversableFunctor T :=
      {| trf_extract := toBatch_extract_Kleisli;
         trf_duplicate := toBatch_duplicate_Kleisli;
      |}.

  End instances.
End DerivedInstances.