Avoiding the postulate of defining non-unary functions over types

Question

I am trying to define functions with more than one argument over factor types. Using currying, I can reduce the problem to defining functions on a pointwise productoidoid:

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 validity of ×-quot without postulating extensionality?

Answer 1

You needed an extension because the value of the P parameter for rec that you selected was the type of function. If you avoid this and use the Quotient type as P , you can do this:

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

And another way to prove this by 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 ℓ} → ∀ {AB : 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 ℓ} → ∀ {AB : Setoid c ℓ} → Quotient (A ⇨ B ⇨ A ×-setoid B) comma = [ comma0 ] _×-quot₂_ : ∀ {c ℓ} {AB : 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 kind of monad. What a pleasant discovery! :)