The Construction of Set-Truncated Higher Inductive Types | Zendy

Niels van der Weide | Zendy; Herman Geuvers | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

The Construction of Set-Truncated Higher Inductive Types

Author(s) -

Niels van der Weide,

Herman Geuvers

Publication year - 2019

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2019.09.014

Subject(s) - finitary , adjunction , quotient , mathematics , schema (genetic algorithms) , algebra over a field , set (abstract data type) , interpretation (philosophy) , type theory , lift (data mining) , type (biology) , pure mathematics , discrete mathematics , computer science , programming language , ecology , machine learning , data mining , biology

We construct finitary set-truncated higher inductive types (HITs) from quotients and the propositional truncation. For that, we first define signatures as a modification of the schema by Basold et al., and we show they give rise to univalent categories of algebras in both sets and setoids. To interpret HITs, we use the well-known method of initial algebra semantics. The desired algebra is obtained by lifting the quotient adjunction to the level of algebras and adapting Dybjeru0027s and Moeneclaeyu0027s interpretation of HITs in setoids. From this construction, we conclude that the equality types of HITs are freely generated and that HITs are unique. The results are formalized in the UniMath library.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research