12/02/04 11:17:47.41
スレチですまんのだけど、Coqだと
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : eq A x x.
という風に等号を定義するだけで（ちなみに上記の意味は、「Type Aの変数xに対して
x=x（eq A x xのこと）の証明が存在することを仮定し、その証明をeq_reflと名づける」といった感じ。）
eq_rect : forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, eq A x y -> P y
というような等号公理が導かれてしまうけど、これってどういう原理なの？
わかりやすい説明とか文献あったら教えてくだされ。エラいひと！