propositional equality

gistfile1.scala

import scalaz._
import Scalaz._

trait REQUAL[A, B] {
  def apply[C[_, _]](
    x: Forall[({type X[D]=C[D, D]})#X]
  ): C[A, B]
}

CoqはIntensional Type Theory。Setoidが必要なのはこのため？
OTTについて: http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf
http://strictlypositive.org/ott.pdf

It separates definitional equality, decidable as in ITT, and a substitutive propositional equality, capturing extensional equality of functions, as in ETT. Moreover, canonicity holds: any closed term is definitionally reducible to a canonical value.
それはITTにおけるようにdecidableなdefinitional equalityとETTにおけるように関数のextensional equalityを捕まえるsubstitutive propositional equalityへ分離する。その上canonicityを持っている。任意の閉じた項はcanonical valueへとdefinitonallyにreducibleである。

Setはdatatypeのsort
Propはpropositional typeのsort
propsitioinal equationが使われるときにITTとOTTが分かれる？
ITTは明示的なLeibniz ruleの適用操作が必要。
ETTだとdefinitional equality (as used in typechecking)とpropositional equality (expressed as a type and used for reasoning)を同一視する。typecheckingがundecidable。
ITTはdefinitional equalityでtype checkingがdecidable。しかしpropositional equalityを扱うのが面倒？
OTTはこれらのいいとこ取りっぽい？
breaucratic:お役所的な