在商数类型上定义非一元函数时,避免使用扩展性假设

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。多么好的发现！:)