Homotopy Type Theory desired articles > history (Rev #23)

This page collects desired articles in the style of a TODO list. Feel free to edit and add your own wishes.

More on encode-decode

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 $\pi_1(S^1)$ and van kampen.

Group theory

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.

Probability theory

Along the lines of Alex Simpson’s synthetic probability theory define the type of probability measures $\mathcal{M}_1(A)$ over a decidable type? $A$ and the set of random variable?s $RV(A)$ over $A$ in homotopy type theory.

Solèr’s theorem and the category of Hilbert spaces

Define the terms used to define and prove Solèr's theorem? in a constructive and predicative manner, and the terms used in the article HilbR to define the category of Hilbert spaces over the real numbers in a constructive and predicative manner.

Order theory and real numbers

(0,1)-sites (i.e. posites), (0,1)-presheaves (antitonic predicates), copresheaves (monotonic predicates), (0,1)-sheaves (ideals), (0,1)-cosheaves (filters), et cetera.

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.

There is also the interval coalgebraic definition of the unit interval and the real numbers by Peter Freyd.

Show that the two-sided Dedekind real numbers defined using Prop is the same as the Cauchy net real numbers, and Freyd’s coalgebraic real numbers.

Show that the predicative Dedekind cut structure real numbers is the same as the Cauchy real numbers.

There is also the HoTT real numbers, and the Escardo-Simpson real numbers defined using interval objects. Show that those two types of real numbers are the same.

• real numbers (disambiguation page for different types of real numbers)

• real unit interval? (disambiguation page for different types of unit intervals in the different types of real numbers)

  • Euclidean unit interval or Escardo-Simpson unit interval
  • coalgebraic unit interval or Freyd unit interval