Аннотация
Morphoid type theory is a typed foundation for mathematics in which each type
is associated with an equality relation in correspondence with the standard
notions of isomorphism in mathematics. The main result is an abstraction
theorem stating that isomorphic objects are substitutable in well typed
contexts. A corollary is "Voldemort's theorem" stating that a non-canonical
object, like a point on a circle, or an isomorphism between a finite
dimensional vector space and its dual, cannot be named by a well typed
expression.
Morphoid type theory seems different from the recently developed homotopy
type theory (HOTT). Morphoid type theory is classical and extensional while
HOTT is constructive and intensional. Morphoid type theory does not involve
homotopy theory. Morphoids are technically quite different from the infinity
groupoids of HOTT.
Пользователи данного ресурса
Пожалуйста,
войдите в систему, чтобы принять участие в дискуссии (добавить собственные рецензию, или комментарий)