Monthly Archives: September 2019

#HoTT #HTTUF Homotopy type theory =#HigherToposTheory ?

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

  1.  https://homotopytypetheory.org

»Homotopy Type Theory refers to a new field of study relating Martin-Löf’s system of intensional, constructive type theory with abstract homotopy theory. … As the natural logic of homotopy, constructive type theory is also related to higher category theoryas it is used e.g. in the notion of a higher topos. »

Page 24 sur 31 :

Homotopy type theory = Higher topos theory ( en encadré)

page 3 sur 21

« it is suspected  that HoTT can be modeled in higher toposes , more precisely (∞,1)-toposes »

https://ncatlab.org/nlab/show/(infinity,1)-topos#ToposTheory

« Working in the (∞,1)-category ∞Grpd of (∞,0)-categories amounts to doing homotopy theory. The point of (∞,1)-sheaves is to pass to parameterized (∞,0)-categories, namely (∞,1)-presheaf categories. Although these (∞,1) (∞,1) ∞Grpd, their objects are generalized spaces 

View original post 445 more words