Как избежать постулата экстенсиональности при определении неунарных функций над частными типами

Я пытаюсь определить функции с более чем одним аргументом над частными типами. Используя каррирование, я могу свести задачу к определению функций над точечным произведением setoid:

module Foo where

open import Quotient
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (proof-irrelevance)

private
  open import Relation.Binary.Product.Pointwise
  open import Data.Product

  _×-quot_ : ∀ {c ℓ} {S : Setoid c ℓ} → Quotient S → Quotient S → Quotient (S ×-setoid S)
  _×-quot_ {S = S} = rec S (λ x → rec S (λ y → [ x , y ])
                           (λ {y} {y′} y≈y′ → [ refl , y≈y′ ]-cong))
                           (λ {x} {x′} x≈x′ → extensionality (elim _ _ (λ _ → [ x≈x′ , refl ]-cong)
                           (λ _ → proof-irrelevance _ _)))
    where
    open Setoid S
    postulate extensionality : P.Extensionality _ _

Мой вопрос в том, есть ли способ доказать правильность ×-quotбез постулирования экстенсиональности?