Archives pour la catégorie HoTT

Elementary (∞,1)-topoi

https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html

https://ncatlab.org/nlab/show/elementary+%28infinity%2C1%29-topos

Publicités

Kapulkin : locally cartesian closed quasicategories from type theory

http://www-home.math.uwo.ca/~kkapulki/papers/qcats-from-type-theory.pdf

Relation entre type theory, category theory et logique

https://news.ycombinator.com/item?id=986746

A noter, en commentaires de cet article de blog, une discussion entre Jacob Lurie, Mike Shulman et Urs Schreiber sur HoTT:

https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-224

Truncations and truncated higher inductive types

Homotopy Type Theory

Truncation is a homotopy-theoretic construction that given a space $latex A$ and an integer n returns an n-truncated space $latex tau_{le{}n}A$ together with a map $latex p:Atotau_{le{}n}A$ in an universal way. More precisely, if i is the inclusion of n-truncated spaces into spaces, then n-truncation is left adjoint to i. ($latex tau_{le{}n}A$ is the free n-truncated space built from $latex A$).

Moreover, the notion of truncated object is something already known in homotopy type theory: a type is n-truncated precisely if it is of h-level n+2.

Truncations are very useful in homotopy theory, and are also useful for foundations of mathematics, especially for n=-1,0:

  • The (-1)-truncation is also known as isinhab: given a type A it returns a proposition isinhab A which is true if and only if A is inhabited (by « proposition » and « set » I will always mean « h-proposition » and…

View original post 1 740 mots de plus