Archives pour la catégorie Higher category theory

Emily Riehl, Mike Shulman : a type theory for synthetic ∞-categories

Un article crucial, écrit par deux des plus grands chercheurs dans le domaine de HoTT et des ∞-catégories, sur l’étroite association des deux domaines:

La présentation de cet article par Emily Riehl sur n-category-cafe :

Sous forme de notes de conférences, plus facile à lire:

Cliquer pour accéder à riehl_e.pdf

Il y a aussi les travaux d’André Joyal sur les tribus et clans, à propos du lien entre théorie des catégories et HoTT :

Étant donné que nous partons de la théorie des catégories et ∞-catégories comme cadre mathématique pour le plan internel et la pensée hénologique, pensée-selon- l’Un et que nous n’enfourchons HoTT que parce qu’il s’agit du cheval le plus dynamique en maths depuis une dizaine d’années, c’est par excellence le sujet adéquat à nos préoccupations

Categories, What’s the Point?

Math ∩ Programming

Perhaps primarily due to the prominence of monads in the Haskell programming language, programmers are often curious about category theory. Proponents of Haskell and other functional languages can put category-theoretic concepts on a pedestal or in a mexican restaurant, and their benefits can seem as mysterious as they are magical. For instance, the most common use of a monad in Haskell is to simulate the mutation of immutable data. Others include suspending and backtracking computations, and even untying tangled rope.

Category theory is often mocked (or praised) as the be-all and end-all of mathematical abstraction, and as such (and for other reasons I’ve explored on this blog) many have found it difficult to digest and impossible to master. However, in truth category theory arose from a need for organizing mathematical ideas based on their shared structure. In this post, I want to give a brief overview of what purpose…

Voir l’article original 1 609 mots de plus

Relation entre type theory, category theory et logique

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

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…

Voir l’article original 1 740 mots de plus