This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Finite presentations of types

module univalent-combinatorics.finite-presentations where

Idea

Finitely presented types are types A equipped with a map f : Fin k → A such that the composite

  Fin k → A → type-trunc-Set A

is an equivalence.