```module Product where

open import Equality
open import Level

----------------------------------------------------------------------
-- Dependent product
----------------------------------------------------------------------
infix  1 Σ
infixr 3 _,_
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 3 _×_
_×_ : {ℓ 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 6 ⟨_,_⟩
⟨_,_⟩ :
{ℓ 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)
```