Showing changes from revision #5 to #6:
Added | Removed | Changed
This page collects desired articles in the style of a TODO list. Feel free to edit and add your own wishes.
This method is used fruitfully in HoTT however can be a bit difficult to understand for beginners. Add some more articles detailing its use and generalisations. Specifically the proof of and van kampen.
Write out results of Higher Groups in Homotopy Type Theory. In particular outline how it can be linked with Localization in Homotopy Type Theory. Then we can finally start talking about localised cohomology.
Write out a definition of a poset, preorder a directed poset, a net, and a Cauchy poset. net, and give a definition of the real numbers in terms of Cauchy nets in a universe, which would inevitably in the next universe. Also give a definition of an inductive system in a precategory and a directed colimit of such an inductive system.
Write out a definition of (0,1)-categorical limits, colimits, functors, opposite preorders, sites, presheaves, copresheaves, sheaves, cosheaves, et cetera.
Write out a definition of a directed poset, a net, and a Cauchy net, and give a definition of the Cauchy net real numbers in terms of Cauchy nets in a universe, which would inevitably in the next universe. Also give a definition of an inductive system in a precategory and a directed colimit of such an inductive system.
Write out a definition of a countably complete directed poset. Define partial function classifiers as a higher inductive-inductive type, as the free countably complete directed poset, and Sierpinski space as the partial function classifier on the unit type.
Write out a definition of a dense linear order, as well as Dedekind cuts and Dedekind cut structure on the dense linear order, using Sierpinski space and using the type of propositions. Define the real numbers in terms of Dedekind cuts and Dedekind cut structure on the dense linear order of some Archimedean integral domain extension of the integers.
There is also the interval coalgebraic definition of the unit interval and the real numbers by Peter Freyd.
Show that the Dedekind real numbers using Prop is the same as the Cauchy net real numbers, and Freyd’s coalgebraic real numbers.
Show that the Dedekind structure real numbers is the same as the Cauchy sequence real numbers.
There is also the HoTT real numbers as the free Cauchy complete metric space on the rationals given in the HoTT book, and the Escardo-Simpson real numbers defined using interval objects. Show that those two types of real numbers are the same.
Define the other terms used in the article HilbR.
Define the terms needed to express Soler’s theorem. Certain terms, such as division star-ring, may need to be modified to make sense constructively (i.e. inequality spaces instead of mere sets). Show that Soler’s theorem is valid constructively and predicatively, or modify Soler’s theorem to be valid constructively and predicatively, and show that the endomorphism object is equivalent to the real numbers using Soler’s theorem. Also determine what type of real numbers is derived from Soler’s theorem in predicative constructive mathematics.