A new class of models for the univalence axiom

Homotopy Type Theory

First of all, in case anyone missed it, Chris Kapulkin recently wrote a guest post at the n-category cafe summarizing the current state of the art regarding “homotopy type theory as the internal language of higher categories”.

I’ve just posted a preprint which improves that state a bit, providing a version of “Lang(C)” containing univalent strict universes for a wider class of (?,1)-toposes C:

View original post 976 more words

Advertisements
Posted in Philosophie | Leave a comment

#HoTT The Book : 2.3 les fibrations comme familles de types

The HoTT Book

Page 72 paragraphe 2.3

Le lemme 2.2.1 Page 71 peut être généralisé aux fonctions types dépendants (« dependently typed functions  »)

Soit P une famille de types sur A et p : x=Ay

Alors il existe une fonction p* : P(x) → P(y)

André Joyal parle aussi des fibrations en tant que flèches particulières dans des catégories particulières appelées clans ou tribus, qui sont la version catégorique de la théorie des types dépendants (« dependent type theory ») :

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/20/hott-le-cours-dandre-joyal-en-cinq-parties-sur-les-tribus/

Voir notamment le deuxième cours:

https://synapse.math.univ-toulouse.fr/s/QWrxKeXn31mN3gz/download?path=%2F&files=Joyal_Theory%20of%20tribes%202.pdf

Page 5 sur 37 : une fibration est un morphisme appartenant à la classe F de morphismes définie selon les conditions explicitées Page 5 et permettant de définir un clan :

– tout isomorphisme (flèche inversible ) est dans F

– F est fermée pour la composition de flèches et le changement de base

– soit 1 l’objet terminal ( qui existe dans tout clan d’apres la définition) alors par définition de l’objet terminal:

https://meditationesdeprimaphilosophia.wordpress.com/2012/05/09/objet-initial-objet-terminal-et-objet-nul-premiere-application-de-la-toposophie-au-coran/

Pour tout objet X du clan il existe une flèche unique de X à 1:

X → 1

cette flèche appartient alors à la classe F des fibrations

André Joyal emploie une notation spéciale pour ces flèches spéciales que sont les fibrations , une flèche à deux pointes :

http://www.fileformat.info/info/unicode/char/21a0/index.htm

Notation dont le code html est donné par la page ci dessus ( & suivi de # et 8608;)

p : A ↠ B

Ces fibrations sont des familles d’objets ( voir Page 7 sur 37)

Au total, comme les objets d’un clan sont les types dans HoTT, on arrive donc bien à une famille de types indexée par un élément variable x d’un autre type :

{E(x), x:B}

famille dite interne (« internal ») au clan.
Un clan ( appelé tribu dans d’autres notes de Joyal ) est donc une catégorie spéciale, qui est une collection de familles internes, fermée pour certaines opérations.

Posted in ∞-catégories, category theory, Higher category theory, homotopy type theory | Leave a comment

Homotopy type theory : univalent foundations of mathematics

Posted in Philosophie | Leave a comment

#ScienceInternelle deux interprétations possibles(?) du théorème de Louis Ferdinand Céline

Le théorème est défini ici d’après Les dialogues entre Parapine (nom évocateur!) et son « chef » Baryton dans le «  Voyaage au bout de la nuit »:

https://anthroposophiephilosophieetscience.wordpress.com/2017/05/04/un-nouveau-theoreme-de-la-scienceinternelle-dit-theoreme-de-louis-ferdinand-celine/

« 

Entre le pénis et les mathématiques, Monsieur Baryton, il n’existe rien… Rien! C’est le vide!

 »

Le pénis représente ici le plan vital de la génération ( et de la mort) , les féministes modernes pourraient y trouver à redire et accuser ce pauvre Céline de phallocentrisme, mais cela serait bien le cadet de ses soucis, lui l’écrivain antisémite vilipendé (et adoré par certains ) et les mathématiques le plan internel

« Brunschvicg «  est le seul nom de juif réel cité dans le récit le plus antisémite de Céline « Bagatelles pour un massacre » dont un extrait significatif est donné ici :

https://anthroposophiephilosophieetscience.wordpress.com/2017/04/13/un-fameux-passage-des-bagatelles-de-louis-ferdinand-celine/

Passons maintenant au théorème : « entre le pénis et les mathématiques il n’y a rien «  peut se comprendre comme identité du plan vital et du plan internel , c’est à dire comme monisme athée : il n’y a que le monde des corps (mortels) , l’esprit est pure illusion s’il est envisagé autrement que comme production des corps matériels , superstructure de la matière.
Le non-dualisme (advaita) n’est pas du tout la même chose que le monisme, l’équivalence que l’identité.
On peut aussi lire «  entre le pénis et les mathématiques il y a RIEN », c’est à dire TOUT , la multiplicité totale des étants, de tout ce qui EST : tout, c’est rien (théorème zéro) :

https://anthroposophiephilosophieetscience.wordpress.com/2017/11/14/rien-est-en-plus-du-mal-de-le-savoir/

Notez bien que Parapine ne dit pas « entre le pénis et la tête il n’y a rien » car là l’erreur serait patente, il oppose « le pénis » notion corporelle et « les mathématiques » notion spirituelle , et ce n’est pas pour rien .. en somme Parapine ( et Louis Ferdinand Céline ) est un kabbaliste ou un talmudiste qui s’ignore , bref un juif « coupeur de cheveux en quatre »

Le théorème peut donc être compris selon la lecture suivante…est ce une lecture littérale, allégorique , homilétique ou mystique ?

https://fr.m.wikipedia.org/wiki/PaRDeS

Entre le pénis, le monde et les mathématiques, la Mathesis, l’hénologie , l’Un , il y a RIEN c’est à dire TOUT, toute la multiplicité des choses et des êtres. LA mathématique n’est rien d’autre que l’activité humaine qui crée l’UN , le plan internel
RIEN EST, mais l’UN n’EST PAS ( Platon expliqué par Badiou qui ne cite pas sa source : Brunschvicg)

Posted in Alain Badiou, Europe, Léon Brunschvicg, Littérature-Poésie, Philosophie, Platon, Science-internelle | Leave a comment

Jacques Audiard : regarde les hommes tomber (1993,vf)

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

https://fr.m.wikipedia.org/wiki/Regarde_les_hommes_tomber

Je dois admettre que Matthieu Kassovitz a un jeu extraordinaire..il y a aussi Christine Pascal quelques années avant son suicide..

Posted in Cinéma | Leave a comment

Soleil vert (1973,vf)

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

New York en 2022.. dans 5 ans maintenant

Posted in Cinéma | Leave a comment

Fais comme l’oiseau

Posted in Musique | Leave a comment