```module Quotient.Product where

open import Quotient
open import Relation.Binary
open import Function
open import Algebra.FunctionProperties using (Op₁; Op₂)

private
module Dummy₁ {c l} {A : Setoid c l} where
open Setoid A renaming (Carrier to A₀)

lift₁ : (f : Op₁ A₀) → f Preserves _≈_ ⟶ _≈_
→ Op₁ (Quotient A)
lift₁ f P = rec _ ([_] ∘ f) (λ x≈y → [ P x≈y ]-cong)
open Dummy₁ public

open import Data.Product
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Binary.Product.Pointwise

_×-quot_ : ∀ {c l c′ l′} → (A : Setoid c l) → (B : Setoid c′ l′) → Set _
A ×-quot B = Quotient (A ×-setoid B)

private
open import Relation.Binary.PropositionalEquality using (Extensionality)
open import Level using (suc) renaming (zero to ℓ₀)
postulate
extensionality : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′

curry-quot : ∀ {c ℓ ℓ′} → ∀ {A B : Setoid c ℓ} {C : Set ℓ′}
→ (A ×-quot B → C) → (Quotient A → Quotient B → C)
curry-quot {A = A} {B = B} {C = C} f =
rec _ f₁ (λ x∼y → extensionality (elim _ (λ t → lem x∼y t) (λ x∼y → proof-irrelevance _ _)))
where
module SA = Setoid A
module SB = Setoid B
module SP = Setoid (A ×-setoid B)

f₁ : Setoid.Carrier A → Quotient B → C
f₁ x = rec _ (λ t → f [ x , t ]) (λ t≈u → cong f [ SA.refl , t≈u ]-cong)

lem : {x y : Setoid.Carrier A} → (x∼y : SA._≈_ x y) → ∀ t → f₁ x [ t ] ≡ f₁ y [ t ]
lem {x} {y} x∼y t = cong f [ (x∼y , SB.refl) ]-cong

private
module Dummy₂ {c l} {A : Setoid c l} where
open Setoid A renaming (Carrier to A₀)

lift₂ : (f : Op₂ A₀) → f Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
→ Op₂ (Quotient A)
lift₂ f P = curry-quot f′
where
f′ : A ×-quot A → Quotient A
f′ = rec _ ([_] ∘ uncurry f) (λ {xt} {yu} eq → [ (P (proj₁ eq) (proj₂ eq)) ]-cong)
open Dummy₂ public

```