Avoiding extensionality postulate when defining non-unary functions over quotient types

Question

I'm trying to define functions with more than one arguments over quotient types. Using currying, I can reduce the problem to defining functions over the pointwise product 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 _ _

My question is, is there a way to prove the soundness of ×-quot without postulating extensionality?

Answer 1

You were needing extensionality because the value of P parameter for rec you have chosen was a function type. If you avoid that and use a Quotient type as P instead, you can do it:

module Quotients 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
  open import Function.Equality

  map-quot : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Quotient A → Quotient B
  map-quot f = rec _ (λ x → [ f ⟨$⟩ x ]) (λ x≈y → [ cong f x≈y ]-cong)

  map-quot-cong : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → 
    let open Setoid (A ⇨ B) renaming (_≈_ to _≐_) in
    (f₁ f₂ : A ⟶ B) → (f₁ ≐ f₂) → (x : Quotient A) → map-quot f₁ x ≡ map-quot f₂ x
  map-quot-cong {A = A} {B = B} f₁ f₂ eq x = 
     elim _ 
     (λ x → map-quot f₁ x ≡ map-quot f₂ x)
     (λ x' → [ eq (Setoid.refl A) ]-cong)
     (λ x≈y → proof-irrelevance _ _)
     x

  _×-quot₁_ : ∀ {c ℓ} {A B : Setoid c ℓ} → Quotient A → Quotient B → Quotient (A ×-setoid B)
  _×-quot₁_ {A = A} {B = B} qx qy = rec A (λ x → map-quot (f x) qy)
                       (λ {x} {x′} x≈x′ → map-quot-cong (f x) (f x′) (λ eq → x≈x′ , eq) qy) qx
    where
     module A = Setoid A
     f = λ x → record { _⟨$⟩_ = _,_ x; cong = λ eq → (A.refl , eq) }

And another way of proving it, going through _<$>_ (which I did first and decided not to throw away):

  infixl 3 _<$>_
  _<$>_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → Quotient (A ⇨ B) → Quotient A → Quotient B
  _<$>_ {A = A} {B = B} qf qa = 
      rec (A ⇨ B) {P = Quotient B} 
      (λ x → map-quot x qa) 
      (λ {f₁} {f₂} f₁≈f₂ → map-quot-cong f₁ f₂ f₁≈f₂ qa) qf 

  comma0 : ∀ {c ℓ} → ∀ {A B : Setoid c ℓ} → Setoid.Carrier (A ⇨ B ⇨ A ×-setoid B)
  comma0 {A = A} {B = B} = record 
    { _⟨$⟩_ = λ x → record 
      { _⟨$⟩_ = λ y → x , y
      ; cong = λ eq → Setoid.refl A , eq 
      }
    ; cong = λ eqa eqb → eqa , eqb
    }

  comma : ∀ {c ℓ} → ∀ {A B : Setoid c ℓ} → Quotient (A ⇨ B ⇨ A ×-setoid B)
  comma = [ comma0 ]

  _×-quot₂_ : ∀ {c ℓ} {A B : Setoid c ℓ} → Quotient A → Quotient B → Quotient (A ×-setoid B)
  a ×-quot₂ b = comma <$> a <$> b

And another version of _<$>_, now using join:

  map-quot-f : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} 
      → Quotient A → (A ⇨ B) ⟶ (P.setoid (Quotient B))
  map-quot-f qa = record { _⟨$⟩_ = λ f → map-quot f qa; cong = λ eq → map-quot-cong _ _ eq qa }

  join : ∀ {c ℓ} → {S : Setoid c ℓ} → Quotient (P.setoid (Quotient S)) → Quotient S
  join {S = S} q = rec (P.setoid (Quotient S)) (λ x → x) (λ eq → eq) q

  infixl 3 _<$>_
  _<$>_ : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → Quotient (A ⇨ B) → Quotient A → Quotient B
  _<$>_ {A = A} {B = B} qf qa = join (map-quot (map-quot-f qa) qf) 

Here it becomes obvious that there is some sort of monad in there. What a nice discovery! :)