quotient type in cubical type theory

HoTT

はじめてのCubical
http://d.hatena.ne.jp/m-a-o/20131227#p1
の続き。何分できたばっかの処理系なので、上で書いたコードは微妙に動かなくなってしまっているっぽいけど、まぁ少し修正するだけ


実用的には、quotient typeが作れるのは重要な気もするので、その話。一応、examples/quotient.cubを見れば実装は載っているが、少し変更した実装を
https://gist.github.com/vertexoperator/3ca7af8c9a0784af9656fd37dfc3eac0
に作った。

quot : (A:U) -> (R:rel A) -> U
quot A R = Sigma (A->U) (\f->exists A (\c->Id (A->U) (R c) f))

-- canonical projection
canProj : (A:U) (R:rel A) -> A -> quot A R
canProj A R a = (R a , pr)
  where
    pr : exists A (\c -> Id (A->U) (R c) (R a))
    pr = inc (Sigma A (\c-> Id (A->U) (R c) (R a))) (a, refl (A->U) (R a))

というのが定義で、こちらの方が分かりやすい(と思う)。canProj A R cは、x:Aがcと同値かどうか判定する関数となる。


前提として、どういう性質を持てば、quotient typeなのかというと、一つは

(x y:A) -> R x y -> Id (quot A R) (canProj A R x) (canProj A R y)

というのが、言えてほしい。これは、同値な元は、quotient type上では等しい元に射影されるという、当然の要請

もう一つは、quotientの普遍性で

(f : A -> B) -> ((x y : A) -> R x y -> Id B (f x) (f y)) -> (quot A R -> B)

という性質。f:A->Bという関数が、同値な元を等しい元に移すなら、quot A R -> Bが作れる。大体、quotient typeがから写像を作るには、いつでも、この関数に頼ることになる。ほんとは、普遍性というからには、存在だけでなく、一意性も言わないといけないけど、そのへんは省略

上の2つの性質を、前提条件も含めて、正確に書くと、

relQuot : (A:U) (R:rel A) -> equivalence A R -> propRel A R -> (x y:A) -> R x y -> 
          Id (quot A R) (canProj A R x) (canProj A R y)

univQuot : (A B : U) (R : rel A) (f : A -> B) -> set B -> resp A B R f -> 
        (eqR : equivalence A R) (pR : propRel A R) (x : quot A R) -> B

という形になる。ただし

resp : (A B : U) (R : rel A) (f : A -> B) -> U
resp A B R f = (x y : A) -> R x y -> Id B (f x) (f y)


もう一つ

setQuot : (A : U) (R:rel A) -> equivalence A R -> propRel A R -> set (quot A R))

というのも言えてほしいけど、証明してない(できるはずだけど)



証明自体は、面倒だけど直感的と思う。relQuoteの方は、propositional extensionality + functional extensionalityと、あと

eqPropFam : (A : U) (B : A -> U) (h : propFam A B) (au bv : Sigma A B) -> Id A au.1 bv.1 -> Id (Sigma A B) au bv

が重要。univQuotの方は、もっと面倒だが、頑張るとできる(説明がめんどい)。univQuotの二変数・N変数版は別途作る必要がある



例として、モノイドの項を割って、自由モノイドを作るみたいのを

に書いてみた。自由モノイドなので、リストでいいんだけど、例としては丁度いい


項の間の同値関係の定義として、一つはnormalizerを定義して、正規化したら、等しい項になるという形で定義できる。ただ、normalizerを正しく作ることは、一般には全然自明でないし、数学的な定義とも乖離してるし、存在するという保証もない。別の定義として

monoideq : (A:U) -> (x y:MonoidTerm A) -> U
monoideq A x y = (r:rel (MonoidTerm A)) -> (p1:equivalence (MonoidTerm A) r) -> 
  (p2:assocProp r) -> (p3:leftidProp r) -> (p4:rightidProp r) -> (p5:substProp r) -> (r x y)
    where
      assocProp : (r:rel (MonoidTerm A)) -> U
      assocProp r = (x y z:MonoidTerm A) -> (r (join x (join y z)) (join (join x y) z))
      leftidProp : (r:rel (MonoidTerm A)) -> U
      leftidProp r = (x:MonoidTerm A) -> (r (join empty x) x)
      rightidProp : (r:rel (MonoidTerm A)) -> U
      rightidProp r = (x:MonoidTerm A) -> (r (join x empty) x)
      substProp : (r:rel (MonoidTerm A)) -> U
      substProp r = (x1 x2 y1 y2:MonoidTerm A) -> (r x1 x2) -> (r y1 y2) -> (r (join x1 y1) (join x2 y2))

とかでもいける。この2つの定義が同値であることは証明できる(上のgistでは面倒になって途中で諦めているけど)


多分本当は

monoideq : (A:U) -> (x y:MonoidTerm A) -> U
monoideq A x y = (r:rel (MonoidTerm A)) -> (p0:propRel (MonoidTerm A) r) -> (p1:equivalence (MonoidTerm A) r) -> 
  (p2:assocProp r) -> (p3:leftidProp r) -> (p4:rightidProp r) -> (p5:substProp r) -> (r x y)
    where
      assocProp : (r:rel (MonoidTerm A)) -> U
      assocProp r = (x y z:MonoidTerm A) -> (r (join x (join y z)) (join (join x y) z))
      leftidProp : (r:rel (MonoidTerm A)) -> U
      leftidProp r = (x:MonoidTerm A) -> (r (join empty x) x)
      rightidProp : (r:rel (MonoidTerm A)) -> U
      rightidProp r = (x:MonoidTerm A) -> (r (join x empty) x)
      substProp : (r:rel (MonoidTerm A)) -> U
      substProp r = (x1 x2 y1 y2:MonoidTerm A) -> (r x1 x2) -> (r y1 y2) -> (r (join x1 y1) (join x2 y2))

としておかないと、monoideqがpropRelにならなくて困りそうな気がする


あまり説明になってないけど、実装見ればわかる気がする
quotient3.cub
https://gist.github.com/vertexoperator/c741f54b2d8a4dfa816f7a375205eae2

monoid.cub
https://gist.github.com/vertexoperator/a0ff3d1aefa6fddc63c0a06cf6b6efba


(追記)Sets in homotopy type theory
http://arxiv.org/abs/1305.3835
の2.4節Voevodsky's impredicative quotientsの構成と、本質的には同じと思う