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.
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.