Tránh đề xuất tính mở rộng khi xác định các hàm không đơn nhất trên các loại thương số

Question

Tôi đang cố xác định các hàm có nhiều hơn một đối số trên các loại thương. Sử dụng currying, tôi có thể làm giảm vấn đề để xác định chức năng so với setoid sản phẩm pointwise:

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

Câu hỏi của tôi là, là có một cách để chứng minh tính đúng đắn của ×-quot mà không postulating extensionality?

Answer 1

Bạn cần mở rộng vì giá trị của thông số P cho rec bạn đã chọn là loại chức năng. Nếu bạn tránh điều đó và sử dụng một loại Quotient như P thay vào đó, bạn có thể làm điều đó:

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

Và một cách khác để chứng minh điều đó, trải qua _<$>_ (mà tôi đã làm đầu tiên và quyết định không vứt bỏ):

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 

Và một phiên bản khác của _<$>_, bây giờ sử dụng 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) 

Ở đây nó trở nên obvi ous rằng có một số loại monad trong đó. Thật là một khám phá thú vị! :)