Finite presentations of types

module univalent-combinatorics.finite-presentations where
Imports

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.