Unikanie postulatu ekstensjonalności podczas definiowania funkcji niejednorodnych w stosunku do typów wartości

Question

Próbuję zdefiniować funkcje z więcej niż jednym argumentem w stosunku do typów ilorazów. Korzystanie currying mogę zmniejszyć problem do definiowania funkcji nad setoid produktu punktowa:

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 _ _ 

Moje pytanie brzmi, czy istnieje sposób, aby udowodnić zasadność ×-quot bez postulując ekstensjonalności?

Answer 1

Potrzebowałeś ekstensjonalności, ponieważ wybrana przez Ciebie wartość parametru P dla rec była typem funkcji. Jeśli tego uniknąć i użyć typu Quotient jak P zamiast tego można to zrobić:

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) } 

a inny sposób udowodnienia go, przechodząc przez _<$>_ (co zrobiłem pierwszy i postanowił nie wyrzucać):

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 

I kolejna wersja _<$>_, teraz za pomocą 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) 

Tutaj staje obvi że tam jest jakaś monada. Cóż za miłe odkrycie! :)