From Tealeaves Require Import
  Classes.Categorical.Applicative.

Import Applicative.Notations.

(** * Cartesian Product Bifunctor *)
(**********************************************************************)

(** ** Bi-map Operation *)
(**********************************************************************)
Section map_pair.

  Definition map_pair
    {A B C D: Type}
    (f: A -> B)
    (g: C -> D):
    A * C -> B * D :=
    map_snd g ∘ map_fst f.

  (** *** Rewriting Laws *)
  (**********************************************************************)
  Lemma map_pair_rw
    {A B C D: Type}
    {f: A -> B}
    {g: C -> D}:
    forall (a: A) (c: C),
      map_pair f g (a, c) = (f a, g c).
A, B, C, D: Type
f: A -> B
g: C -> D
forall (a : A) (c : C),
map_pair f g (a, c) = (f a, g c)
  Proof.
A, B, C, D: Type
f: A -> B
g: C -> D
forall (a : A) (c : C),
map_pair f g (a, c) = (f a, g c)
    reflexivity.
  Qed.

  (** *** Lifting <<map>> to <<map_pair>> *)
  (**********************************************************************)
  Lemma map_fst_to_pair
    {A B C: Type} {f: A -> B}:
    map_fst (Y := C) f = map_pair f id.
A, B, C: Type
f: A -> B
map_fst f = map_pair f id
  Proof.
A, B, C: Type
f: A -> B
map_fst f = map_pair f id
    intros.
A, B, C: Type
f: A -> B
map_fst f = map_pair f id
    ext [a c].
A, B, C: Type
f: A -> B
a: A
c: C
map_fst f (a, c) = map_pair f id (a, c)
    reflexivity.
  Qed.

  Lemma map_snd_to_pair
    {A C D: Type} {g: C -> D}:
    map_snd (X := A) g = map_pair id g.
A, C, D: Type
g: C -> D
map_snd g = map_pair id g
  Proof.
A, C, D: Type
g: C -> D
map_snd g = map_pair id g
    intros.
A, C, D: Type
g: C -> D
map_snd g = map_pair id g
    ext [a c].
A, C, D: Type
g: C -> D
a: A
c: C
map_snd g (a, c) = map_pair id g (a, c)
    reflexivity.
  Qed.

End map_pair.

(** ** Bi-traverse Operation *)
(**********************************************************************)
Section traverse_pair.

  Context
    {G: Type -> Type}
    `{Map G} `{Mult G} `{Pure G}.

  Context
    {A B C D: Type}

    (f: A -> G B) (g: C -> G D).

  Definition traverse_pair: A * C -> G (B * D) :=
    fun '(a, c) => pure pair <⋆> f a <⋆> g c.

  Lemma traverse_pair_rw:
    forall (a: A) (c: C),
      traverse_pair (a, c) =
        pure pair <⋆> f a <⋆> g c.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
A, B, C, D: Type
f: A -> G B
g: C -> G D
forall (a : A) (c : C),
traverse_pair (a, c) = pure pair <⋆> f a <⋆> g c
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
A, B, C, D: Type
f: A -> G B
g: C -> G D
forall (a : A) (c : C),
traverse_pair (a, c) = pure pair <⋆> f a <⋆> g c
    reflexivity.
  Qed.

End traverse_pair.