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 に答える