この門をくぐる者 一切の幾何学的イメージを捨てよ

(追記)結局、ここに書いたことは嘘でした(

homotopy type theoryで、circleの定義は、higher inductive typeを使って

(* this is invalid in Coq *)
Inductive circle : Type :=
  | base : circle
  | loop : paths base base.

と書ける(ということになっている)。何となく、点baseがあって、baseとbaseを結ぶ(自明でない)曲線があるのだから、まあ円周だよね、という風に理解してたのだけど、最近は「objectがbaseで"生成"され、Hom(base,base)がloopで生成されるような∞-groupoidの中で普遍的なもの」と読むのが正しい気がしている。"∞-groupoidの中で普遍的"ということの厳密な定義は、多分今のところないけど、「以下の生成元と関係式で定義される代数/群」とか数学者が言うのと、発想としては同じ。

普通のinductive typeは、morphismがどうなっているかについて、何も言及してないので、全てのmorphismは自明となると考えるのが自然。上のcircleの場合は、Hom(base,base)が群となることは証明できるので、(もし更にextraな構造がないなら)単一の生成元loopで生成される群=Zと考えるのが自然。これは、univalence axiomを仮定してSchulmanが証明したことでもある

HoTT業界のfolkloreによると、球面は

(* this is invalid in Coq *)
Inductive sphere : Type :=
  | base2 : sphere
  | loop2 : paths (refl base2) (refl base2)

と定義できることになっている

参考:http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html

これは「objectがbase2で生成され、base2からbase2の恒等射refl間の2-morphismがloop2で生成されるような∞-groupoidで普遍的なもの」と読むと、3次以上のホモトピー群は消えると思うのが自然なはず。homotopy hypothesisによれば、homotopy type(このtypeは型理論の"型"じゃなくて、いわゆる"ホモトピー型"の型)と∞-groupoidは1:1に対応するはずで、これを球面と読むのは、間違ってることになる。直感的には、1次のホモトピー群は自明な群{refl}、2次のホモトピー群はZになるはずで、これはEilenberg-MacLane空間K(Z,2)と思うべきだと思う。

参考:Homotopy hypothesis
http://ncatlab.org/nlab/show/homotopy+hypothesis

これを確認する方法は、実際に、上のHigher Inductive Typeの3次のホモトピー群がZになるか、0になるか証明すればいい。けど、今のところ、どっちもできてない。わたしの3倍くらい賢い人が、球面だと言ってるので、やっぱ球面なんだろうかとも思うけど、わたしが間違ってたらこの文章は黒歴史になり、正しかったらドヤ顔すればいい