8

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

4

1 回答 1

5

您需要可扩展性，因为您选择的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)

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

于 2012-05-13T16:29:22.673 回答