module Stdlib.Data.Product;

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

import Stdlib.Trait.Ord as Ord;
open Ord using {Ord};

import Stdlib.Trait.Show as Show;
open Show using {Show};

open import Stdlib.Data.Product.Base public;
open import Stdlib.Data.Bool.Base;
open import Stdlib.Data.String.Base;

module ProductTraits;
  Eq : {A B : Type} -> Eq A -> Eq B -> Eq (A × B);
  Eq (Eq.mkEq eq-a) (Eq.mkEq eq-b) :=
    Eq.mkEq
      λ {
        | (a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2
      };
  
  Ord : {A B : Type} -> Ord A -> Ord B -> Ord (A × B);
  Ord (Ord.mkOrd cmp-a) (Ord.mkOrd cmp-b) :=
    Ord.mkOrd
      λ {
        | (a1, b1) (a2, b2) :=
          case cmp-a a1 a2
            | Ord.LT := Ord.LT
            | Ord.GT := Ord.GT
            | Ord.EQ := cmp-b b1 b2
      };
  
  Show : {A B : Type} -> Show A -> Show B -> Show (A × B);
  Show (Show.mkShow show-a) (Show.mkShow show-b) :=
    Show.mkShow
      λ {
        | (a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"
      };
end;