Finite presentations of types

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2021-12-30.
Last modified on 2023-05-16.

module univalent-combinatorics.finite-presentations where


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.

Recent changes