Monthly Archives: August 2017

André Joyal : categorical #HoTT 2

L’exposé d’André Joyal est ici: http://www1.maths.leeds.ac.uk/~pmtng/joyal-mit.pdf Nous en avions déjà étudié la première partie ici: https://anthroposophiephilosophieetscience.wordpress.com/2017/08/23/joyal-categorical-hott-1/ et avions vu que les tribus (tribes; attention il existe le même terme en théorie de la mesure, mais cela n’a rien à voir) … Continue reading

Posted in ∞-catégories, ∞-topoi, homotopy type theory | Tagged

Cubical Higher Type Theory as a Programming Language

Originally posted on Existential Type:
I gave a presentation at the Workshop on Categorical Logic and Univalent Foundations held in Leeds, UK July 27-29th 2016.  My talk, entitled Computational Higher Type Theory, concerns a formulation of higher-dimensional type theory in which terms are interpreted directly as…

Posted in Philosophie

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 , , ,

#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 , , ,

Joyal : #HoTT and category theory

http://logica.dmi.unisa.it/tacl/wp-content/uploads/2014/08/Joyal-TACL2015.pdf

Posted in ∞-catégories, ∞-topoi, category theory, Higher category theory, homotopy type theory, Philosophie mathématique

Type systems in terms of contexts and judgments

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

Posted in homotopy type theory

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