%0 Generic %1 mcallester2014morphoid %A McAllester, David %D 2014 %K morphoid type %T Morphoid Type Theory %U http://arxiv.org/abs/1407.7274 %X 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.

@misc{mcallester2014morphoid, abstract = {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.}, added-at = {2015-01-31T04:17:16.000+0100}, author = {McAllester, David}, biburl = {https://www.bibsonomy.org/bibtex/2be9bf3a2dcb7f6c7f76b5480808bbd08/t.uemura}, description = {[1407.7274] Morphoid Type Theory}, interhash = {8ad278de121b3805d7a24330d80eee99}, intrahash = {be9bf3a2dcb7f6c7f76b5480808bbd08}, keywords = {morphoid type}, note = {cite \href{http://arxiv.org/abs/1407.7274}{arxiv:1407.7274}}, timestamp = {2015-01-31T04:17:16.000+0100}, title = {Morphoid Type Theory}, url = {http://arxiv.org/abs/1407.7274}, year = 2014 }