TraversableFunctor.v

From Tealeaves Require Export
  Classes.Categorical.TraversableFunctor
  Classes.Kleisli.TraversableFunctor
  Adapters.CategoricalToKleisli.TraversableFunctor
  Adapters.KleisliToCategorical.TraversableFunctor.

(** * Categorical ~> Kleisli ~> Categorical *)
(**********************************************************************)
Module traversable_functor_categorical_kleisli_categorical.

  Context
    (T: Type -> Type)
    `{mapT: Map T}
    `{distT: ApplicativeDist T}
    `{! Categorical.TraversableFunctor.TraversableFunctor T}.

  #[local] Instance traverse': Traverse T :=
    DerivedOperations.Traverse_Categorical T.

  Definition map2: Map T :=
    DerivedOperations.Map_Traverse T.
  Definition dist2: ApplicativeDist T :=
    DerivedOperations.Dist_Traverse T.

  Goal mapT = map2.mapT = map2
  Proof.mapT = map2
    unfold map2.mapT = DerivedOperations.Map_Traverse T
    unfold DerivedOperations.Map_Traverse.mapT = (fun (A B : Type) (f : A -> B) => traverse f)
    unfold traverse.mapT =
(fun (A B : Type) (f : A -> B) =>
 traverse' (fun A0 : Type => A0) Map_I Pure_I Mult_I A
   B f)
    unfold traverse'.mapT =
(fun (A B : Type) (f : A -> B) =>
 DerivedOperations.Traverse_Categorical T
   (fun A0 : Type => A0) Map_I Pure_I Mult_I A B f)
    unfold DerivedOperations.Traverse_Categorical.mapT =
(fun A B : Type =>
 compose (dist T (fun A0 : Type => A0)) ○ map)
    ext A B f.A, B: Type
f: A -> B
mapT A B f = dist T (fun A : Type => A) ∘ map f
    rewrite (dist_unit (F := T)).A, B: Type
f: A -> B
mapT A B f = id ∘ map f
    reflexivity.
  Qed.

  Goal distT = dist2.distT = dist2
  Proof.distT = dist2
    unfold dist2.distT = DerivedOperations.Dist_Traverse T
    unfold DerivedOperations.Dist_Traverse.distT =
(fun (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A : Type) => traverse id)
    unfold traverse.distT =
(fun (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A : Type) =>
 traverse' G H H0 H1 (G A) A id)
    unfold traverse'.distT =
(fun (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A : Type) =>
 DerivedOperations.Traverse_Categorical T G H H0 H1
   (G A) A id)
    unfold DerivedOperations.Traverse_Categorical.distT =
(fun (G : Type -> Type) (H : Map G) (H0 : Pure G)
   (H1 : Mult G) (A : Type) => dist T G ∘ map id)
    ext G Hmap Hpure Hmult.G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
distT G Hmap Hpure Hmult =
(fun A : Type => dist T G ∘ map id) ext A.G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
A: Type
distT G Hmap Hpure Hmult A = dist T G ∘ map id
    rewrite (fun_map_id (F := T)).G: Type -> Type
Hmap: Map G
Hpure: Pure G
Hmult: Mult G
A: Type
distT G Hmap Hpure Hmult A = dist T G ∘ id
    reflexivity.
  Qed.

End traversable_functor_categorical_kleisli_categorical.

(** * Kleisli ~> Categorical ~> Kleisli *)
(**********************************************************************)
Module traversable_functor_kleisli_categorical_kleisli.

  Context
    (T: Type -> Type)
    `{traverseT: Traverse T}
    `{@Classes.Kleisli.TraversableFunctor.TraversableFunctor T _}.

  Definition map': Map T :=
    DerivedOperations.Map_Traverse T.

  Definition dist': ApplicativeDist T :=
    DerivedOperations.Dist_Traverse T.

  Definition traverse2: Traverse T :=
    DerivedOperations.Traverse_Categorical T
      (Map_T := map') (Dist_T := dist').

  Goal forall (G: Type -> Type) `{Applicative G},
      @traverseT G _ _ _ = @traverse2 G _ _ _.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
traverseT G Map_G Pure_G Mult_G =
traverse2 G Map_G Pure_G Mult_G
  Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
traverseT G Map_G Pure_G Mult_G =
traverse2 G Map_G Pure_G Mult_G
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
traverseT G Map_G Pure_G Mult_G =
traverse2 G Map_G Pure_G Mult_G
    unfold traverse2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
traverseT G Map_G Pure_G Mult_G =
DerivedOperations.Traverse_Categorical T G Map_G
  Pure_G Mult_G
    unfold DerivedOperations.Traverse_Categorical.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
traverseT G Map_G Pure_G Mult_G =
(fun A B : Type => compose (dist T G) ○ map)
    unfold dist.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
traverseT G Map_G Pure_G Mult_G =
(fun A B : Type =>
 compose (dist' G Map_G Pure_G Mult_G B) ○ map)
    unfold dist'.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
traverseT G Map_G Pure_G Mult_G =
(fun A B : Type =>
 compose
   (DerivedOperations.Dist_Traverse T G Map_G Pure_G
      Mult_G B) ○ map)
    unfold DerivedOperations.Dist_Traverse.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
traverseT G Map_G Pure_G Mult_G =
(fun A B : Type => compose (traverse id) ○ map)
    unfold map, map', dist, dist'.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
traverseT G Map_G Pure_G Mult_G =
(fun A B : Type =>
 compose (traverse id)
 ○ DerivedOperations.Map_Traverse T A (G B))
    ext A B f.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
traverseT G Map_G Pure_G Mult_G A B f =
traverse id
∘ DerivedOperations.Map_Traverse T A (G B) f
    unfold DerivedOperations.Map_Traverse.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
traverseT G Map_G Pure_G Mult_G A B f =
traverse id ∘ traverse f
    change (traverse (T := T) (G := G) (@id (G B))) with
      (map (F := fun A => A) (traverse (T := T) (G := G) (@id (G B)))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
traverseT G Map_G Pure_G Mult_G A B f =
map (traverse id) ∘ traverse f
    rewrite (trf_traverse_traverse (T := T) (G1 := fun A => A)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
traverseT G Map_G Pure_G Mult_G A B f =
traverse (kc2 id f)
    rewrite (traverse_app_id_l).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
traverseT G Map_G Pure_G Mult_G A B f =
traverse (kc2 id f)
    reflexivity.
  Qed.

End traversable_functor_kleisli_categorical_kleisli.

(** * Coalgebraic ~> Kleisli ~> Coalgebraic (TODO) *)
(**********************************************************************)

(** * Kleisli ~> Coalgebraic ~> Kleisli (TODO) *)
(**********************************************************************)