module foundations.product-type where
open import foundations.universe import foundations.sigma-type as S open S using (Σ) open S using (_,_; fst; snd) public
private variable ℓ ℓ′ : Level _×_ : Type ℓ → Type ℓ′ → Type (ℓ ⊔ ℓ′) A × B = Σ A (λ _ → B)