Type-theoretical features

Todo

heterogeneous Id types (used in e.g. cubicaltt)

Impredicative prop / propositional resizing

The principle that there is only one type \(\Omega\) of propositions, and it is a member of \(\mathcal{U}_0\): so all types of propositions \(\mathsf{Prop}_i\) are equal, and it is a type in the lowest universe.

Assuming this principle, the set of types of any universe is a topos.

Assuming this principle, some HITs become definable by impredicative encoding: e.g. truncation as \(\prod_{P:\Omega}(X\to P)\to P\).

UniMath uses propositional resizing.

Induction-{induction,recursion}

Induction-induction is different from induction-recursion.

See also Andrej Bauer on CS.StackExchange as well as [NFS12].

W-types

Todo

aka GADTs (?): every instance of a datatype declaration is really just a W-type. compare with unimath (which doesn’t assume to have them). (well, this is not quite true: should also consider the computation rules.)

Initial algebras

Coinduction

Todo

• pi-types
• altenkirch’s presentation?