Daily Archives: September 27, 2017

Homotopy Theory in Homotopy Type Theory: Introduction

Originally posted on Homotopy Type Theory:
Many of us working on homotopy type theory believe that it will be a better framework for doing math, and in particular computer-checked math, than set theory or classical higher-order logic or non-univalent type…

Posted in Philosophie

Stanley Kubrick : Lolita (vf) 1962

L’infinie misère humaine est dans le livre de Nabokov, adapté par Kubrick avec James Mason: https://m.ok.ru/dk?st.cmd=movieLayer&st.discId=207800961659&st.retLoc=default&st.discType=MOVIE&st.mvId=207800961659&st.stpos=rec_13&_prevCmd=movieLayer&tkn=899

Posted in Cinéma

Internal category in #HoTT

https://ncatlab.org/nlab/show/internal+category+in+homotopy+type+theory https://ncatlab.org/nlab/show/category+object+in+an+%28infinity%2C1%29-category

Posted in ∞-catégories, category theory, Higher category theory, homotopy type theory

Segal-type models of higher categories

Click to access 1707.01868.pdf

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

“Dismissive attitude of #HoTT” among homotopy theorists and higher category theorists


Posted in ∞-catégories, Homotopy, homotopy type theory

David Corfield : #HoTT and the vertical unity of concepts in mathematics

Click to access vertical.pdf

Posted in homotopy type theory, Philosophie

An Interval Type Implies Function Extensionality

Originally posted on Homotopy Type Theory:
One of the most important spaces in homotopy theory is the interval (be it the topological interval or the simplicial interval ). Thus, it is natural to ask whether there is, or can be,…

Posted in homotopy type theory

Computational higher type theory

Click to access harper.pdf http://math.andrej.com/category/homotopy-type-theory/ https://ncatlab.org/nlab/show/computational+type+theory Click to access lh12wg2.8.pdf

Posted in homotopy type theory

A hands-on introduction to cubicaltt

Originally posted on Homotopy Type Theory:
Some months ago I gave a series of hands-on lectures on cubicaltt at Inria Sophia Antipolis that can be found at: https://github.com/mortberg/cubicaltt/tree/master/lectures The lectures cover the main features of the system and don’t assume…

Posted in homotopy type theory

#HoTT The Book : product types, dependent pair types ou Σ-types

The HoTT Book http://planetmath.org/typetheory Étant donné deux types A , B on définit leur produit cartésien comme pour les ensembles. Un élément de A × B est une paire ordonnée (a,b) avec a : A et b:B https://en.m.wikipedia.org/wiki/Product_type Le produit … Continue reading

Posted in homotopy type theory