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

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.

Recent changes

• 2023-05-16. Fredrik Bakke. Swap from md to text code blocks (#622).
• 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
• 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
• 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).
• 2023-02-13. Jonathan Prieto-Cubides. Nueva era (#445).