« En dehors de la présence de l’unité dans une conscience qui sait n’être radicalement extérieure à rien, il n’y a rien, non point parce qu’on a été incapable de rien trouver, mais parce qu’il n’y avait rien en effet à chercher «
(Léon Brunschvicg)_
« Entre le pénis et les mathématiques, il n’y a rien ! C’est le vide total! »
Louis Ferdinand Céline, Voyage au bout de la nuit (1932)
l’amour, c’est quelque chose qu’on n’a pas et qu’on donne à quelqu’un qui n’en veut pas
Entre tout et rien, il y a tout, et donc il n’y a rien. Tout, c’est tout ce qu’il y a. En tout cas ce n’est pas assez!
Dieu ne naîtra pas d’une intuition tournée vers l’extérieur comme celle qui nous met en présence d’une chose ou d’une personne. Dieu est précisément ce chez qui l’existence ne sera pas différente de l’essence ; et cette essence ne se manifestera que du dedans grâce à l’effort de réflexion qui découvre dans le progrès indéfini dont est c a pable notre pensée l’éternité de l’intelligence et l’universalité de l’amour. Nous ne doutons pas que Dieu existe puisque nous nous se n tons toujours, selon la parole de Malebranche, du mouvement pour aller plus loin jusqu’à cette sphère lumineuse qui apparaît au sommet de la dialectique platonicienne où, passant par dessus l’imagination de l’être, l’unité de l’Un se suffit et se répond à soi-même. Méditer l’Être nous en éloigne ; méditer l’unité y ramène.
Léon Brunschvicg : héritage de mots, héritage d’idées
Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids. Homotopy type theory offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. The present book is intended as a first systematic exposition of the basics of univalent foundations,