List view

• Populate Types directory

  Fill out each of the following files in [/theories/types](https://github.com/HoTT/HoTT/tree/master/theories/types) Paths, Forall, Arrow, Sigma, Prod, Sum, Unit, Empty[Set], Bool, Universe, Record so that each follows the following outline (or some variation of it as appropriate): UMP; paths; transport; functoriality; equivalences; h-levels. as currently exemplified by Prod.v ([frozen permalink](https://github.com/HoTT/HoTT/blob/1190cd7b33dfd7b8f80e12907f02cbcf1f7aa047/theories/types/Prod.v), [live copy](https://github.com/HoTT/HoTT/blob/master/theories/types/Prod.v)).

  No due date

  •10/10 issues closed
  100% complete0 open10 closed

• Port content of old HoTT library

  Port over all the content from HoTT/HoTT as it stood before the Dec 2012 reset, i.e. roughly [this commit](https://github.com/HoTT/HoTT/blob/b0ba7974595857df4fc6b77c4e6e88e8ed7aa911/theories/FunextEquivalences.v).

  No due date

  •7/7 issues closed
  100% complete0 open7 closed

• Higher inductive types

  When Bruno Barras has a good enough version of Coq supporting higher inductive types, we should use them to define circles, h-set-reflection, quotients, etc.

  No due date
  0% complete0 open0 closed

• Incorporate polymorphic universes

  Once Matthieu Sozeau creates a stable enough version of Coq with universe polymorphism, the library will be ported to the newer version of Coq.

  No due date
  0% complete0 open0 closed

• Canonical structures

  The library shall be organized so that it uses the canonical structures mechanism to automatically infer properties of types and objects (contractible, h-set, equivalence). There are several steps that we need to accomplish each described as an issue under this milestone. We are doing this with an older version of Coq which does not yet support universe polymorphism. Once the universe polymorphism code is stable enough we will port the library to the newer version of Coq.

  No due date

  •2/2 issues closed
  100% complete0 open2 closed