2度目のCubical

HoTT

Thierry Coquandが、cubical interpreterでHigher Inductive Typeが使えるようになったとアナウンスしていた。理論的な面で進歩があったわけではないようだけど、cubical interpreterの実装が少し進歩したらしい。
https://github.com/mortberg/cubicaltt


基本的には、以前の実装を踏襲しているけど、primitive扱いだったreflとかmapOnPathが

refl (A : U) (a : A) : Id A a a = <i> a

みたいな形で定義できるようになっている。前も、内部的には、こういう形で扱われていた(実装上はTermとValueの区別が、あんまりなくなった?)のだけど、明示的に書けるようになったので、cubical type theoryを理解するのに便利になった。この変更のおかげで、実装も以前より、すっきりしたように見える。


<i> aは直感的には、i=0とi=1にaを対応させるintervalのことと思う(一次元"cube")。
Variation on Cubical sets
http://www.cse.chalmers.se/~coquand/comp.pdf
の13節に、operational semanticsとかがある。一般に、p : Id A x yは、i=0にx、i=1にyを対応させる"関数のようなもの"と解釈されて、新しいcubical interpreterでは、p@0とp@1で、それぞれx,yを取り出せる。直感的には、iは区間[0,1]のことであるが、p@0.5とかはできない


Syntaxとかも少し変更されているようなので、
はじめてのCubical
http://d.hatena.ne.jp/m-a-o/20131227#p1
の後半の例を書き直してみた(Syntaxは、また変わるかもしれないが)

module firsttest where

-- definitions from examples/prelude.ctt
-- -- "IdP P a b" is a built-in notion where P : Id U A B, a : A and b : B
-- "<a>" abstracts the name/color/dimension a.
Id (A : U) (a0 a1 : A) : U = IdP (<a> A) a0 a1

refl (A : U) (a : A) : Id A a a = <i> a

mapOnPath (A B : U) (f : A -> B) (x y : A)
          (p : Id A x y) : Id B (f x) (f y) = <a> f (p @ a)

funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
       (p : (x : A) -> Id (B x) (f x) (g x)) :
       Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i

subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
  transport (mapOnPath A U P a b p) e


-- end of quote


ext (A B:U) (f g:A->B) (p : (x:A) -> Id B (f x) (g x)) : Id (A->B) f g = funExt A (\(a:A) -> B) f g p

data Nat = zero | succ (n:Nat)

add : Nat -> Nat -> Nat = split
  zero -> \(y:Nat) -> y
  succ n -> \(y:Nat) -> succ (add n y)

add0 : Nat -> Nat = \(n:Nat) -> add zero n

id (A:U) (a:A) : A = a

add0 : Nat -> Nat = \(n:Nat) -> add zero n

add0_eq_id : Id (Nat->Nat) add0 (id Nat) = 
   ext Nat Nat add0 (id Nat) p
      where
         p (n:Nat) : (Id Nat (add0 n) (id Nat n)) = refl Nat n

test : Nat = subst (Nat->Nat) f add0 (id Nat) add0_eq_id  zero
  where
    f (x:Nat -> Nat) : U = Nat

前半部分は、prelude.cttから取ってきたので、import preludeで済む(transportとIdPはprimitive)。ファイルをloadして、testを評価すると、これが、ちゃんとzeroであることが分かる


以前は、内部的に扱われていたKan compositionも明示的に書けるようになった(Variation on Cubical setsの4節に説明がある)。例えば

module kantest where

Id (A : U) (a0 a1 : A) : U = IdP (<a> A) a0 a1
kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
                          (r : Id A b d) : Id A c d =
  <i> comp A (p @ i) [ (i = 0) -> q , (i = 1) -> r ]

これは
A model of type theory in cubical sets
http://www.cse.chalmers.se/~coquand/mod1.pdf
の操作$X^{+}$に対応している。<i> comp A (p @ i) [ (i = 0) -> q , (i = 1) -> r ]は、i=0の時
(<i> comp A (p @ i) [ (i = 0) -> q , (i = 1) -> r ])@0 = comp A a [(i=0)->q]
で、qの型はq : Id A a cであるけど、compは点a=q@0をq : Id A a cをc=q@1に"繋ぐ"ような働きをして、
(<i> comp A (p @ i) [ (i = 0) -> q , (i = 1) -> r ])@0 = c
となる。同様に、i=1の時は
(<i> comp A (p @ i) [ (i = 0) -> q , (i = 1) -> r ])@1 = d
で、<i> comp A (p @ i) [ (i = 0) -> q , (i = 1) -> r ]自体の型は、Id A c dとなる。これを使えば、Idの推移律を示すことができる。対称律も、本来は、Kan filling/Kan compositionを使って作るのだけど、もっと単純に

eqsym (A:U) (x y:A) (p:Id A x y) : Id A y x= <i> p @ -i

と書ける。-iは、0を1に、1を0にする



compはintervalだけじゃなく、squareとか、任意のn-cubeも作れる。

module sqtest where
Id (A:U) (x y:A) : U = IdP (<i> A) x y
prop (A : U) : U = (a b : A) -> IdP (<i> A) a b
--         u
--    a0 -----> a1
--    |         |
-- r0 |         | r1
--    |         |
--    V         V
--    b0 -----> b1
--         v

Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
               (b0 b1 : A) (v : Id A b0 b1)
               (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
  = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1

propSquare  (A:U) (H:prop A) (a a0 a1 b0 b1:A) (r0 : Id A a0 b0) (r1 : Id A a1 b1) (u : Id A a0 a1) (v : Id A b0 b1) 
  : Square A a0 a1 u b0 b1 v r0 r1
  = <i j> comp A a [(i=0)-> H a (r0@j) ,(i=1) -> H a (r1@j) , (j=0) -> H a (u@i) , (j=1) -> H a (v@i)]

とか。<i j> comp A a [(i=0)-> H a (r0@j) ,(i=1) -> H a (r1@j) , (j=0) -> H a (u@i) , (j=1) -> H a (v@i)]は、頂点(i,j)=(0,0)に於いては、
comp A a [(i=0) -> H a (r0@0)]
と同じで、これはa0である。または
comp A a [(j=0) -> H a (u@0)]
でもあり、やっぱり、a0である。これは、当然ながら、ちゃんとcompatibleでないといけない。[]の中は空でもよくて(0-cube相当?)、comp A a [ ]は、aになる。


glueingもあるけど略


Higher Inductive Typeの作り方は,circle.cttとかsusp.cttとかinterval.cttとかにある

data S1 = base
        | loop_ @ base ~ base

loop : Id S1 base base = <i> loop_{S1} @ i

みたいにやる。なんでだかよく分からないけど、コンストラクタloop_の型は、Id S1 base baseでなく、上のような形で作る必要がある。それ以外は、普通



Quotients of sets
http://ncatlab.org/nlab/show/higher+inductive+type#QuotientsOfSets
を真似て、HITを使ってquotient typeを作ろうと思ったのだけど、書いてある定義は出来ない気がする

module quotient where
import prelude

rel (A:U) : U = A -> A -> U

prop (A:U) : U = (x y:A) -> Id A x y

propRel (A:U) (R:rel A) : U = (x y : A) -> prop (R x y)

{-
data quotient (A:U) (R:rel A) (p:propRel A R) 
  = proj (x:A) 
  | relate (x y:A) (r:R x y) @ proj x ~ proj y
  | contr1 (x y:quotient A R p) (u v : Id (quotient A R p) x y) @ u ~ v
-}

data quotient (A:U) (R:rel A) 
  = proj (x:A) 
  | relate (x y:A) @ proj x ~ proj y

よく考えてみると、contr1は、商をhSetにするために必要なのだと思うけど、そもそも、AがhSetでない場合、商もhSetであるとは限らないで、contr1が定義出来てしまうと、矛盾してしまう気がするけど、どうなんだろう。
quotient type in cubical type theory
http://d.hatena.ne.jp/m-a-o/20140825#p1
で定義したquotと同等な定義は上の形でいいんじゃないかという気がする。推測では、これだけで、(RがpropRelかつequivalenceの時)、商の普遍性が言え("inductive"なんだから普遍性は満たすだろうと思うけど)て、HITを使わないquotient typeと等しいことが言えると思う(けど、証明は書いていない。そのうち書く)


あと、こういう↓感じで、assocを定義しようとすると無理っぽい。2回addが出てきているので、だめっぽい

module testdat where

-- type constructor "assoc" is invalid
data TestAlg (A:U)
  = empty
  | lift (x:A)
  | add (x:TestAlg A) (y:TestAlg A)
  | comm (x y:TestAlg A) @ add x y ~ add y x
--  | assoc (x y z:TestAlg A) @ add (add x y) z ~ add x (add y z)


homotopy groups of spheres
http://ncatlab.org/homotopytypetheory/show/homotopy+groups+of+spheres
に

Guillaume has proved that there exists an $n$ such that $\pi_4(S^3)$ is $\mathbb{Z}_n$. Given a computational interpretation, we could run this proof and check that $n$ is 2.

という一文があるのだけど、cubical interpreterは、univalence axiomのcomputational interpretationを与えていると(予想)され、かつHITを使えるようになった(Suspensionがあるので、S^3は定義できる)ので、試金石として試すことができるはず