Archives quotidiennes :

Alain Resnais : Hiroshima mon amour (1959)

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

https://m.ok.ru/video/87158557371

« Impossible de ne pas venir »

« HI-RO-SHI-MA ..Hiroshima c’est ton nom »

« C’est mon nom oui. ..et toi ton nom est NE-VERS Nevers-en-France »

Impossible d’oublier cette scène ..

Et dans la scène du début , est ce la poussière du temps qui se déverse sur l’enlacement des corps des amants ?

https://unedemeuresouterraineenformedecaverne.wordpress.com/la-troisieme-aile-de-lange/

View original post

Publicités

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

#HoTT une théorie « synthétique » des groupoides

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

Toujours dans l’article :

http://home.sandiego.edu/~shulman/papers/synhott.pdf

Michael Shulman Page 4 décrit les groupoides comme une généralisation des ensembles comme collections. Il y a deux sortes de collections, dont la seconde est Le collection des manières dont deux objets x et y sont « égaux  » : c’est un groupoide (ou un ∞-groupoide) considéré comme généralisation d’un ensemble (« Set »).
Au début du paragraphe 3 Page 5 Michael Shulman oppose la « théorie synthétique » des ∞-groupoide sur qu’est HoTT , en gros théorie axiomatique qui précise les règles et axiomes auxquelles doivent obéir ces entités nouvelles à la « théorie analytique » qui définit ce qu’est un ∞-groupoide en termes d’autres entités mathématiques.

Les entités basiques de HoTT se comportent comme des ∞-groupoide sur mais sont appelées « types » . Ces types ont des éléments dont il sont les « collections » . Section 4, les propositions de la logique sont des types à partir desquels on peut former d’autres…

View original post 260 mots de plus