From Tealeaves Require Export
  Tactics.Prelude.

#[local] Generalizable All Variables.

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.
  Proof.
    now ext [[? ?] ?].
  Qed.

  Theorem associator_iso_2:
    associator ∘ associator_inv = id.
  Proof.
    now ext [? [? ?]].
  Qed.

End associator.

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

Import Notations.

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: ∀ A,
    left_unitor_inv ∘ left_unitor = @id (unit × A).
Proof.
  introv; now ext [[] ?].
Qed.

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

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

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

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

Theorem pentagon {X Y Z W}:
  map_snd α ∘ α ∘ map_fst (Y := W) (@associator X Y Z) = α ∘ α.
Proof.
  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).
Proof.
  now ext [? ?].
Qed.

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}: ∀ (f: X → Y → Z),
    f = curry (uncurry f).
Proof.
  now intros.
Qed.

Lemma curry_iso_inv {X Y Z}: ∀ (f: X × Y → Z),
    f = uncurry (curry f).
Proof.
  intros. now ext [? ?].
Qed.

Lemma product_delete_l {X Y Z}: ∀ (f: X → Z) (p: X × Y),
    snd (map_fst f p) = snd p.
Proof.
  now intros ? [? ?].
Qed.

Lemma product_delete_r {X Y W}: ∀ (f: Y → W) (p: X × Y),
    fst (map_snd f p) = fst p.
Proof.
  now intros ? [? ?].
Qed.

Lemma snd_map_snd {X Y Z}: ∀ (f: Y → Z) (p: X × Y),
    snd (map_snd f p) = f (snd p).
Proof.
  now intros ? [? ?].
Qed.

Lemma fst_map_fst {X Y W}: ∀ (f: X → W) (p: X × Y),
    fst (map_fst f p) = f (fst p).
Proof.
  now intros ? [? ?].
Qed.

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}:
  ∀ (f: X → Z) (g: Y → W) (p: X × Y),
    map_fst f (map_snd g p) = map_snd g (map_fst f p).
Proof.
  now intros ? ? [? ?].
Qed.

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

Definition dup_left {A B}: A × B → A × (A × B) :=
  fun '(a, b) ⇒ (a, (a, b)).

Lemma map_fst_compose {A B C X: Type}: ∀ (f: A → B) (g: B → C),
    map_fst g ∘ map_fst f = map_fst (Y := X) (g ∘ f).
Proof.
  intros. ext [a x]. reflexivity.
Qed.

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

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