module Product where

open import Equality 
open import Level

----------------------------------------------------------------------
-- Dependent product
----------------------------------------------------------------------
infix   Σ
infixr  _,_
record Σ {ℓ m : Level}(A : Set ℓ)(B : A → Set m) : Set(ℓ ⊔ m) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

syntax Σ A (λ x → B) = Σ x ∈ A , B

Σext :
  {ℓ m : Level}
  {A : Set ℓ}
  {B : A → Set m}
  {x x' : A}
  {y : B x}
  {y' : B x'}
  (p : x ≡ x')
  (q : subst B p y ≡ y')
  → --------------------
  (x , y) ≡ (x' , y')
Σext refl refl = refl

----------------------------------------------------------------------
-- Cartesian product
----------------------------------------------------------------------
infixr  _×_
_×_ : {ℓ m : Level} → Set ℓ → Set m → Set (ℓ ⊔ m)
A × B = Σ A (λ _ → B)

×ext :
  {ℓ m : Level}
  {A : Set ℓ}
  {B : Set m}
  {x x' : A}
  {y y' : B}
  (p : x ≡ x')
  (q : y ≡ y')
  → -----------------
  (x , y) ≡ (x' , y')
×ext refl refl = refl

≡contr :
  {ℓ : Level}
  {A : Set ℓ}
  {x y : A}
  (p : x ≡ y)
  → ------------------------------------------
  _≡_ {ℓ} {Σ y ∈ A , x ≡ y} (x , refl) (y , p)
≡contr refl = refl

infix  ⟨_,_⟩
⟨_,_⟩ :
   {ℓ m n : Level}
   {A : Set ℓ}
   {B : Set m}
   {C : B → Set n}
   (f : A → B)
   (g : (x : A) → C (f x))
   → ---------------------
   A → Σ B C
⟨ f , g ⟩ x = (f x , g x)