Author Archives: mathesisuniversalis

A syntax for cubical type theory

https://akaposi.github.io/pres_oxford.pdf Advertisements

Posted in homotopy type theory | Leave a comment

Warming up to Homotopy Type Theory

Originally posted on pigworker in a space:
“Why do you hate homotopy type theory?” is question I am sometimes asked, but I never answer it, because the question has an inaccurate presupposition. I am not happy when people forget that…

Posted in Philosophie | Leave a comment

Just Kidding: Understanding Identity Elimination in Homotopy Type Theory

Originally posted on Homotopy Type Theory:
Several current proof assistants, such as Agda and Epigram, provide uniqueness of identity proofs (UIP): any two proofs of the same propositional equality are themselves propositionally equal. Homotopy type theory generalizes this picture to…

Posted in Philosophie | Leave a comment

L’amour

“L’amour c’est donner quelque chose qu’on n’a pas à quelqu’un qui n’en veut pas” ( Jacques Lacan)

Posted in Europe, FRANCE 2017, France-bordel, Merde in France | Leave a comment

Philosophie et calcul aujourd’hui : Deleuze et les triades de la substance chez Spinoza

https://hal.archives-ouvertes.fr/lirmm-00435704/document Dans “La raison systématique” Daniel Parrochia tente de formaliser, si je me souviens bien, une catégorie des systèmes philosophiques. Ce projet est voisin. Voir aussi la dianoématique de Martial Guéroult: https://www.cairn.info/revue-de-metaphysique-et-de-morale-2001-2-page-69.htm On peut distinguer cinq types de systèmes philosophiques: … Continue reading

Posted in category theory, Deleuze, Philosophie, Philosophie mathématique | Tagged , , | Leave a comment

Martin Scorsese : le loup de Wall Street (vf)

http://sokrostream.ws/films/le-loup-de-wall-street-78712.html (Choisir openload) Il faut écouter et prendre au sérieux les divagations de Mark Hannah au début : “J’emmerde le client… le but du jeu c’est de siphonner l’argent dans la poche du client et de le faire passer dans … Continue reading

Posted in Cinéma | Leave a comment

Logic, types and Spaces : dependent fonction types

http://siddhartha-gadgil.github.io/LogicTypesSpaces/blog/2015/01/22/dependent-function-types/

Posted in homotopy type theory | Leave a comment