Monthly Archives: August 2017

André Joyal : categorical #HoTT 2

L’exposé d’André Joyal est ici: Click to access joyal-mit.pdf Nous en avions déjà étudié la première partie ici: Joyal : categorical #HoTT 1 et avions vu que les tribus (tribes; attention il existe le même terme en théorie de la mesure, … Continue reading

Posted in ∞-catégories, ∞-topoi, homotopy type theory | Tagged | Comments Off on André Joyal : categorical #HoTT 2

Cubical Higher Type Theory as a Programming Language

Posted in Philosophie | Comments Off on Cubical Higher Type Theory as a Programming Language

Fichte : l’être et l’esprit; la perception est un jugement. #HoTT

La présentation par Max Marcuzzi de la philosophie de Fichte en tête des “Introductions berlinoises à la philosophie” est précieuse pour quelqu’un qui, comme c’est mon cas, connaît mal cette pensée: https://books.google.fr/books?id=v38WAwAAQBAJ&printsec=frontcover&hl=fr#v=onepage&q&f=false On peut lire pages 38-39 et suivantes ces … Continue reading

Posted in Anthroposophie, ∞-catégories, ∞-topoi, Cochet-Brunschvicg, Fichte, homotopy type theory, Léon Brunschvicg, Philosophie, Science-internelle | Tagged , , , | Comments Off on Fichte : l’être et l’esprit; la perception est un jugement. #HoTT

#HoTT : théorie homotopique des types une révolution des mathématiques ?

Lorsque j’ai créé ce blog, il n’y a pas si longtemps de cela, je ne connaissais même pas ce nom : HoTT = homotopy type theory = théorie homotopique des types, encore moins en quoi consistait cette “nouvelle fondation” des … Continue reading

Posted in Alain Badiou, ∞-catégories, ∞-cosmoi, ∞-topoi, category theory, Grothendieck, Higher category theory, Higher topos theory, Homotopy, homotopy type theory, Léon Brunschvicg, Philosophie, Philosophie mathématique, Science, mathesis, Science-internelle | Tagged , , , | Comments Off on #HoTT : théorie homotopique des types une révolution des mathématiques ?

Joyal : #HoTT and category theory

Click to access Joyal-TACL2015.pdf

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, homotopy type theory, Philosophie mathématique | Comments Off on Joyal : #HoTT and category theory

Type systems in terms of contexts and judgments

https://groups.google.com/forum/m/#!msg/homotopytypetheory/ZG64YSPYUSE/zuuSKueFZVYJ

Posted in homotopy type theory | Comments Off on Type systems in terms of contexts and judgments

A bit of type theory: Negation is a proposition

Originally posted on infinite cardinals:
(This was originally posted to reddit, but since the response to it spawned this blog, I figured I’d repost it here. It could use some editing, but c’est la vie…)   So, I’ve wanted to…

Posted in Philosophie | Comments Off on A bit of type theory: Negation is a proposition

Constructive Validity

Originally posted on Homotopy Type Theory:
(This is intended to complement Mike Shulman’s nCat Cafe posting?HoTT, II.) The Propositions-as-Types conception of Martin-Löf type theory leads to a system of logic that is different from both classical and intuitionistic logic with…

Posted in Philosophie | Comments Off on Constructive Validity

Ce blog est “universaliste et laïque ” mais pas “de gauche” ni féministe

La gauche collaborationniste, comme il y a 80 ans avec le nazisme, par làcheté “pacifiste”, apporte son soutien au Mal Absolu, symbolisé par le port du voile: http://www.liberation.fr/debats/2017/08/23/stop-au-cyberharcelement-islamophobe-contre-l-association-lallab_1591443 ” En plus de reposer sur une compréhension erronée de la loi … Continue reading

Posted in Europe, nazisme, Ouvert : dualité plan vital-plan spirituel, Philosophie, Plan vital-plan spirituel, Religions, Science-internelle | Comments Off on Ce blog est “universaliste et laïque ” mais pas “de gauche” ni féministe

#HoTT la Page d’Erik Palmgren

http://staff.math.su.se/palmgren/

Posted in homotopy type theory | Comments Off on #HoTT la Page d’Erik Palmgren