agda - 在商类型上定义非一元函数时避免外延假设

Question

我试图在商类型上定义具有多个参数的函数。使用柯里化(Currying)，我可以将问题减少到在逐点积 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 的合理性？没有假设外延性？

Answer 1

您需要扩展性，因为 P 的值rec 的参数你选择的是一个函数类型。如果你避免这种情况并使用 Quotient键入 P相反，您可以这样做:

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

还有另一种证明方式，通过 _<$>_ (我首先做了并决定不扔掉):

  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

另一个版本的 _<$>_ , 现在使用 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) 

在这里很明显那里有某种单子(monad)。多么好的发现! :)