Daily Archives: October 23, 2017

Type-theoretic model category

https://ncatlab.org/nlab/show/type-theoretic+model+category Page citée sur celle ci : https://ncatlab.org/nlab/show/identity+type Advertisements

Posted in category theory, Higher category theory, homotopy type theory | Tagged

Premier contact (2016) : les humains, comme les toxicomanes chez Ernst Junger portent La Croix du temps!

Originally posted on Henosophia Léon BRUNSCHVICG et la philosophie Μαθεσις Universalis:
le film peut être vu ici en vf : https://m.ok.ru/video/216015440503 Cet article de l’an dernier à son sujet: https://anthroposophiephilosophieetscience.wordpress.com/2016/12/16/premier-contact-arrival-2016-excellent-et-important/ ? En fait ce que les extraterrestres apportent à l’humanité…

Posted in Cinéma, Cochet-Brunschvicg, Léon Brunschvicg, Ouvert : dualité plan vital-plan spirituel, Philosophie, Physique, Science, mathesis, Science-internelle

Impredicative Encodings of Inductive Types in HoTT

Originally posted on Homotopy Type Theory:
I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the…

Posted in Philosophie

#HoTT The Book : 1.11 propositions as types

The HoTT Book https://hott.github.io/book/nightly/hott-online-1075-g3c53219.pdf Je passe sur ce qui n’est pas essentiel pour aller plus vite car il faut accélérer pour en arriver aux choses sérieuses qui commencent au chapitre 2. Passons donc Page 41 au 1.11: Les termes ou … Continue reading

Posted in homotopy type theory

Thèse : towards an (∞,2)-category of coherent monads in an ∞-cosmos

https://infoscience.epfl.ch/record/231037/files/EPFL_TH7748.pdf

Posted in ∞-catégories, ∞-cosmoi, ∞-topoi | Tagged , ,

Fibration categories and Type theory

http://www.lorentzcenter.nl/lc/web/2011/467/presentations/Presentation%20C%20Kapulkin.pdf

Posted in Homotopy, homotopy type theory