From Tealeaves Require Export
  Tactics.Prelude.

(** This file defines the monoidal-category-theoretic structure on the
    category of types and functions given by the Cartesian product
    [prod]. It supplies generally useful definitions like [copy] and
    [map_snd] related to the product functor. *)

#[local] Generalizable All Variables.

(** * Monoidal Category-Theoretic Structure on <<Type>> *)
(**********************************************************************)

(** ** Reassociating Cartesian Products *)
(**********************************************************************)
Section associator.

  Context
    {X Y Z W: Type}.

  (* Recall Coq's notation "_ * _" associates to the left. *)
  Definition associator: (X * Y) * Z -> X * (Y * Z) :=
    fun p => match p with
             | ((x, y), z) => (x, (y, z))
             end.

  Definition associator_inv: (X * (Y * Z)) -> (X * Y) * Z :=
    fun p => match p with
             | (x, (y, z)) => ((x, y), z)
             end.

  Theorem associator_iso_1:
    associator_inv ∘ associator = id.
X, Y, Z, W: Type
associator_inv ∘ associator = id
  Proof.
X, Y, Z, W: Type
associator_inv ∘ associator = id
    now ext [[? ?] ?].
  Qed.

  Theorem associator_iso_2:
    associator ∘ associator_inv = id.
X, Y, Z, W: Type
associator ∘ associator_inv = id
  Proof.
X, Y, Z, W: Type
associator ∘ associator_inv = id
    now ext [? [? ?]].
  Qed.

End associator.

(** ** Notations *)
(**********************************************************************)
Module Notations.
  Notation "'α'" := (associator): tealeaves_scope.
  Notation "'α^-1'" := (associator_inv): tealeaves_scope.
  Notation "( X  × )" := (prod X) (only parsing): function_scope.
End Notations.

Import Notations.

(** ** Monoidal Category Theory Laws *)
(**********************************************************************)
Definition map_tensor `(f: X -> Z) `(g: Y -> W) `(p: X * Y): Z * W :=
  match p with
  | (x, y) => (f x, g y)
  end.

Definition map_fst {Y} `(f: X -> Z): X * Y -> Z * Y :=
  map_tensor f id.

Definition map_snd {X} `(f: Y -> W): X * Y -> X * W :=
  map_tensor id f.

Definition map_both `(f: X -> Z): X * X -> Z * Z :=
  map_tensor f f.

Definition left_unitor {X}: unit * X -> X := snd.

Definition left_unitor_inv {X}: X -> unit * X := pair tt.

Definition right_unitor {X}: (X * unit) -> X := fst.

Definition right_unitor_inv {X}: X -> X * unit := fun x => (x, tt).

Theorem unitors_1: forall A,
    left_unitor_inv ∘ left_unitor = @id (unit * A).
forall A : Type, left_unitor_inv ∘ left_unitor = id
Proof.
forall A : Type, left_unitor_inv ∘ left_unitor = id
  introv; now ext [[] ?].
Qed.

Theorem unitors_2: forall A, left_unitor ∘ left_unitor_inv = @id A.
forall A : Type, left_unitor ∘ left_unitor_inv = id
Proof.
forall A : Type, left_unitor ∘ left_unitor_inv = id
  introv.
A: Type
left_unitor ∘ left_unitor_inv = id now ext a.
Qed.

Theorem unitors_3: forall A, right_unitor_inv ∘ right_unitor =
                          @id (A * unit).
forall A : Type, right_unitor_inv ∘ right_unitor = id
Proof.
forall A : Type, right_unitor_inv ∘ right_unitor = id
  introv; now ext [? []].
Qed.

Theorem unitors_4: forall A, right_unitor ∘ right_unitor_inv = @id A.
forall A : Type, right_unitor ∘ right_unitor_inv = id
Proof.
forall A : Type, right_unitor ∘ right_unitor_inv = id
  introv; now ext a.
Qed.

Theorem triangle {X Y}:
  map_fst (X := X * unit) (Y := Y) right_unitor =
    map_snd left_unitor ∘ α.
X, Y: Type
map_fst right_unitor = map_snd left_unitor ∘ α
Proof.
X, Y: Type
map_fst right_unitor = map_snd left_unitor ∘ α
  now ext [[? ?] ?].
Qed.

Theorem pentagon {X Y Z W}:
  map_snd α ∘ α ∘ map_fst (Y := W) (@associator X Y Z) = α ∘ α.
X, Y, Z, W: Type
map_snd α ∘ α ∘ map_fst α = α ∘ α
Proof.
X, Y, Z, W: Type
map_snd α ∘ α ∘ map_fst α = α ∘ α
  now ext [[[? ?] ?] ?].
Qed.

Definition braiding {X Y: Type}: X * Y -> Y * X :=
  fun p => match p with
        | (x, y) => (y, x)
        end.

Theorem braiding_symmetry {X Y}:
  braiding ∘ braiding = @id (X * Y).
X, Y: Type
braiding ∘ braiding = id
Proof.
X, Y: Type
braiding ∘ braiding = id
  now ext [? ?].
Qed.

(** ** Currying and Uncurrying *)
(**********************************************************************)
Definition uncurry {X Y Z}: (X -> Y -> Z) -> (X * Y -> Z) :=
  fun f p => let '(x, y) := p in f x y.

Definition curry {X Y Z}: (X * Y -> Z) -> (X -> Y -> Z) :=
  fun f x y => f (x, y).

Lemma curry_iso {X Y Z}: forall (f: X -> Y -> Z),
    f = curry (uncurry f).
X, Y, Z: Type
forall f : X -> Y -> Z, f = curry (uncurry f)
Proof.
X, Y, Z: Type
forall f : X -> Y -> Z, f = curry (uncurry f)
  now intros.
Qed.

Lemma curry_iso_inv {X Y Z}: forall (f: X * Y -> Z),
    f = uncurry (curry f).
X, Y, Z: Type
forall f : X * Y -> Z, f = uncurry (curry f)
Proof.
X, Y, Z: Type
forall f : X * Y -> Z, f = uncurry (curry f)
  intros.
X, Y, Z: Type
f: X * Y -> Z
f = uncurry (curry f) now ext [? ?].
Qed.

(** ** Deletions/Projections *)
(**********************************************************************)
Lemma product_delete_l {X Y Z}: forall (f: X -> Z) (p: X * Y),
    snd (map_fst f p) = snd p.
X, Y, Z: Type
forall (f : X -> Z) (p : X * Y),
snd (map_fst f p) = snd p
Proof.
X, Y, Z: Type
forall (f : X -> Z) (p : X * Y),
snd (map_fst f p) = snd p
  now intros ? [? ?].
Qed.

Lemma product_delete_r {X Y W}: forall (f: Y -> W) (p: X * Y),
    fst (map_snd f p) = fst p.
X, Y, W: Type
forall (f : Y -> W) (p : X * Y),
fst (map_snd f p) = fst p
Proof.
X, Y, W: Type
forall (f : Y -> W) (p : X * Y),
fst (map_snd f p) = fst p
  now intros ? [? ?].
Qed.

Lemma snd_map_snd {X Y Z}: forall (f: Y -> Z) (p: X * Y),
    snd (map_snd f p) = f (snd p).
X, Y, Z: Type
forall (f : Y -> Z) (p : X * Y),
snd (map_snd f p) = f (snd p)
Proof.
X, Y, Z: Type
forall (f : Y -> Z) (p : X * Y),
snd (map_snd f p) = f (snd p)
  now intros ? [? ?].
Qed.

Lemma fst_map_fst {X Y W}: forall (f: X -> W) (p: X * Y),
    fst (map_fst f p) = f (fst p).
X, Y, W: Type
forall (f : X -> W) (p : X * Y),
fst (map_fst f p) = f (fst p)
Proof.
X, Y, W: Type
forall (f : X -> W) (p : X * Y),
fst (map_fst f p) = f (fst p)
  now intros ? [? ?].
Qed.

(** ** Miscellaneous *)
(**********************************************************************)
Definition swap_middle {X Y Z W}:
  (X * Y) * (Z * W) -> (X * Z) * (Y * W) :=
  fun p =>
    associator_inv
      (map_snd associator
         (map_snd (map_fst braiding)
            (map_snd associator_inv
               (associator p)))).

Lemma product_map_slide {X Y Z W}:
  forall (f: X -> Z) (g: Y -> W) (p: X * Y),
    map_fst f (map_snd g p) = map_snd g (map_fst f p).
X, Y, Z, W: Type
forall (f : X -> Z) (g : Y -> W) (p : X * Y),
map_fst f (map_snd g p) = map_snd g (map_fst f p)
Proof.
X, Y, Z, W: Type
forall (f : X -> Z) (g : Y -> W) (p : X * Y),
map_fst f (map_snd g p) = map_snd g (map_fst f p)
  now intros ? ? [? ?].
Qed.

Lemma product_map_slide_pf {X Y Z W}: forall (f: X -> Z) (g: Y -> W),
    map_fst f ∘ map_snd g = map_snd g ∘ map_fst f.
X, Y, Z, W: Type
forall (f : X -> Z) (g : Y -> W),
map_fst f ∘ map_snd g = map_snd g ∘ map_fst f
Proof.
X, Y, Z, W: Type
forall (f : X -> Z) (g : Y -> W),
map_fst f ∘ map_snd g = map_snd g ∘ map_fst f
  intros.
X, Y, Z, W: Type
f: X -> Z
g: Y -> W
map_fst f ∘ map_snd g = map_snd g ∘ map_fst f now ext [x y].
Qed.

Definition dup_left {A B}: A * B -> A * (A * B) :=
  fun '(a, b) => (a, (a, b)).

(** ** Commuting Maps *)
(**********************************************************************)
Lemma map_fst_compose {A B C X: Type}: forall (f: A -> B) (g: B -> C),
    map_fst g ∘ map_fst f = map_fst (Y := X) (g ∘ f).
A, B, C, X: Type
forall (f : A -> B) (g : B -> C),
map_fst g ∘ map_fst f = map_fst (g ∘ f)
Proof.
A, B, C, X: Type
forall (f : A -> B) (g : B -> C),
map_fst g ∘ map_fst f = map_fst (g ∘ f)
  intros.
A, B, C, X: Type
f: A -> B
g: B -> C
map_fst g ∘ map_fst f = map_fst (g ∘ f) ext [a x].
A, B, C, X: Type
f: A -> B
g: B -> C
a: A
x: X
(map_fst g ∘ map_fst f) (a, x) =
map_fst (g ∘ f) (a, x) reflexivity.
Qed.

Lemma map_snd_compose {A B C X: Type}: forall (f: A -> B) (g: B -> C),
    map_snd g ∘ map_snd f = map_snd (X := X) (g ∘ f).
A, B, C, X: Type
forall (f : A -> B) (g : B -> C),
map_snd g ∘ map_snd f = map_snd (g ∘ f)
Proof.
A, B, C, X: Type
forall (f : A -> B) (g : B -> C),
map_snd g ∘ map_snd f = map_snd (g ∘ f)
  intros.
A, B, C, X: Type
f: A -> B
g: B -> C
map_snd g ∘ map_snd f = map_snd (g ∘ f) ext [x a].
A, B, C, X: Type
f: A -> B
g: B -> C
x: X
a: A
(map_snd g ∘ map_snd f) (x, a) =
map_snd (g ∘ f) (x, a) reflexivity.
Qed.

Lemma map_fst_map_snd {A B C D: Type}: forall (f: A -> B) (g: C -> D),
    map_snd g ∘ map_fst f = map_fst f ∘ map_snd g.
A, B, C, D: Type
forall (f : A -> B) (g : C -> D),
map_snd g ∘ map_fst f = map_fst f ∘ map_snd g
Proof.
A, B, C, D: Type
forall (f : A -> B) (g : C -> D),
map_snd g ∘ map_fst f = map_fst f ∘ map_snd g
  intros.
A, B, C, D: Type
f: A -> B
g: C -> D
map_snd g ∘ map_fst f = map_fst f ∘ map_snd g ext [a c].
A, B, C, D: Type
f: A -> B
g: C -> D
a: A
c: C
(map_snd g ∘ map_fst f) (a, c) =
(map_fst f ∘ map_snd g) (a, c) reflexivity.
Qed.