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

#[local] Generalizable Variables ϕ G.

(** * Categorical Traversable Functors from Kleisli Traversable Functors *)
(**********************************************************************)

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

  #[export] Instance Dist_Traverse (T: Type -> Type) `{Traverse T}
 : ApplicativeDist T := fun G _ _ _ A => traverse (@id (G A)).

End DerivedOperations.

(** ** Compatibility Classes *)
(**********************************************************************)
Class Compat_Dist_Traverse
    (F: Type -> Type)
    `{Traverse_F: Traverse F}
    `{Dist_F: ApplicativeDist F} :=
  compat_dist_traverse:
    Dist_F = @DerivedOperations.Dist_Traverse F Traverse_F.

#[export] Instance compat_dist_traverse_self
    (F: Type -> Type)
    `{Traverse_F: Traverse F}:
  Compat_Dist_Traverse F (Dist_F := DerivedOperations.Dist_Traverse F).
F: Type -> Type
Traverse_F: Traverse F
Compat_Dist_Traverse F
Proof.
F: Type -> Type
Traverse_F: Traverse F
Compat_Dist_Traverse F
  reflexivity.
Qed.


Lemma dist_to_traverse {F}
    `{Traverse_F: Traverse F}
    `{Map_F: Map F}
    `{Dist_F: ApplicativeDist F}
    `{Compat: ! Compat_Dist_Traverse F}:
  forall {G} `{Map_G: Map G} `{Pure_G: Pure G} `{Mult_G: Mult G} (A: Type) (t: F (G A)),
    @dist F Dist_F G Map_G Pure_G Mult_G A = traverse (G := G) id.
F: Type -> Type
Traverse_F: Traverse F
Map_F: Map F
Dist_F: ApplicativeDist F
Compat: Compat_Dist_Traverse F
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G) (A : Type),
F (G A) -> dist F G = traverse id
Proof.
F: Type -> Type
Traverse_F: Traverse F
Map_F: Map F
Dist_F: ApplicativeDist F
Compat: Compat_Dist_Traverse F
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G) (A : Type),
F (G A) -> dist F G = traverse id
  now rewrite compat_dist_traverse.
Qed.

(** ** Derived Instances *)
(**********************************************************************)
Module DerivedInstances.

  Section proofs.

    Context
      (T: Type -> Type)
      `{Kleisli.TraversableFunctor.TraversableFunctor T}.
      (* Alectryon doesn't like this
      Import KleisliToCategorical.TraversableFunctor.DerivedOperations.
      *)
      Import DerivedOperations.
      Import Kleisli.TraversableFunctor.DerivedOperations.
      Import Kleisli.TraversableFunctor.DerivedInstances.

    Lemma dist_natural_T:
      forall (G: Type -> Type)
        (H2: Map G) (H3: Pure G) (H4: Mult G),
        Applicative G -> Natural (@dist T _ G H2 H3 H4).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
Natural (@dist T (Dist_Traverse T) G H2 H3 H4)
    Proof.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G : Type -> Type) (H2 : Map G) (H3 : Pure G)
  (H4 : Mult G),
Applicative G ->
Natural (@dist T (Dist_Traverse T) G H2 H3 H4)
      intros.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
Natural (@dist T (Dist_Traverse T) G H2 H3 H4) constructor.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
Functor (T ○ G)
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
Functor (G ○ T)
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ dist T G = dist T G ∘ map f
      -
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
Functor (T ○ G) typeclasses eauto.
      -
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
Functor (G ○ T) typeclasses eauto.
      -
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ dist T G = dist T G ∘ map f intros.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
A, B: Type
f: A -> B
map f ∘ dist T G = dist T G ∘ map f unfold_ops @Map_compose @Dist_Traverse @Map_Traverse.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
A, B: Type
f: A -> B
map (traverse f) ∘ traverse id =
traverse id ∘ traverse (map f)
        rewrite (trf_traverse_traverse (G1 := G) (G2 := fun A => A)).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
A, B: Type
f: A -> B
traverse (kc2 f id) = traverse id ∘ traverse (map f)
        change (traverse (@id (G B))) with
          (map (F := fun A => A) (traverse (@id (G B)))).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
A, B: Type
f: A -> B
traverse (kc2 f id) =
map (traverse id) ∘ traverse (map f)
        rewrite (trf_traverse_traverse (G1 := fun A => A) (G2 := G)).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
A, B: Type
f: A -> B
traverse (kc2 f id) = traverse (kc2 id (map f))
        (* (These rewrites are hidden) *)
        rewrite (Mult_compose_identity1 G).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
A, B: Type
f: A -> B
traverse (kc2 f id) = traverse (kc2 id (map f))
        rewrite (Mult_compose_identity2 G).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G: Type -> Type
H2: Map G
H3: Pure G
H4: Mult G
H0: Applicative G
A, B: Type
f: A -> B
traverse (kc2 f id) = traverse (kc2 id (map f))
        reflexivity.
    Qed.

    Lemma dist_morph_T: forall G1 G2 `{ApplicativeMorphism G1 G2 ϕ},
      forall A: Type, dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
    Proof.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1
      intros.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
dist T G2 ∘ map (ϕ A) = ϕ (T A) ∘ dist T G1 unfold_ops @Dist_Traverse @Map_Traverse.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
traverse id ∘ traverse (ϕ A) = ϕ (T A) ∘ traverse id
      change (traverse (@id (G2 A))) with
        (map (F := fun A => A) (traverse (@id (G2 A)))).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
map (traverse id) ∘ traverse (ϕ A) =
ϕ (T A) ∘ traverse id
      infer_applicative_instances.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
map (traverse id) ∘ traverse (ϕ A) =
ϕ (T A) ∘ traverse id
      rewrite (trf_traverse_traverse (G1 := fun A => A)).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
traverse (kc2 id (ϕ A)) = ϕ (T A) ∘ traverse id
      change (map (fun A => A) id ∘ ?f) with f.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
traverse (kc2 id (ϕ A)) = ϕ (T A) ∘ traverse id
      rewrite (trf_traverse_morphism (T := T)).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
traverse (kc2 id (ϕ A)) = traverse (ϕ A ∘ id)
      fequal.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
app1: Applicative G1
app2: Applicative G2
Mult_compose (fun A : Type => A) G2 = H4 now rewrite (Mult_compose_identity2 G2).
    Qed.

    Lemma dist_unit_T: forall A: Type,
        dist T (fun A0: Type => A0) = @id (T A).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall A : Type, dist T (fun A0 : Type => A0) = id
    Proof.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall A : Type, dist T (fun A0 : Type => A0) = id
      intros.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
dist T (fun A0 : Type => A0) = id unfold_ops @Dist_Traverse.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
A: Type
traverse id = id
      apply (trf_traverse_id (T := T)).
    Qed.

    Lemma dist_linear_T:
      forall (G1: Type -> Type)
        (H2: Map G1) (H3: Pure G1) (H4: Mult G1),
        Applicative G1 ->
      forall (G2: Type -> Type)
        (H6: Map G2) (H7: Pure G2) (H8: Mult G2),
        Applicative G2 ->
      forall A: Type,
        dist T (G1 ∘ G2) (A := A) =
          map (F := G1) (dist T G2) ∘ dist T G1.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H6 : Map G2)
  (H7 : Pure G2) (H8 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
    Proof.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
forall (G1 : Type -> Type) (H2 : Map G1)
  (H3 : Pure G1) (H4 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H6 : Map G2)
  (H7 : Pure G2) (H8 : Mult G2),
Applicative G2 ->
forall A : Type,
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1
      intros.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
dist T (G1 ∘ G2) = map (dist T G2) ∘ dist T G1 unfold_ops @Dist_Traverse.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
traverse id = map (traverse id) ∘ traverse id
      rewrite (trf_traverse_traverse).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
traverse id = traverse (kc2 id id)
      unfold kc2.
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
traverse id = traverse (map id ∘ id)
      rewrite (fun_map_id (F := G1)).
T: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
G1: Type -> Type
H2: Map G1
H3: Pure G1
H4: Mult G1
H0: Applicative G1
G2: Type -> Type
H6: Map G2
H7: Pure G2
H8: Mult G2
H1: Applicative G2
A: Type
traverse id = traverse (id ∘ id)
      reflexivity.
    Qed.

    #[export] Instance TraversableFunctor_Categorical_Kleisli:
      Categorical.TraversableFunctor.TraversableFunctor T :=
      {| dist_natural := dist_natural_T;
         dist_morph := dist_morph_T;
         dist_unit := dist_unit_T;
         dist_linear := dist_linear_T;
      |}.

  End proofs.

End DerivedInstances.