On the relationship between well-orderings in intuitionistic type theory and data types inductively defined

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.

Copyright Notice

The author of the article or book reviews submitted and approved for publication authorizes the editors to reproduce it and publish it in the journal O que nos faz pensar, with the terms “reproduction” and “publication” being understood in accordance with the definitions of the Creative Commons Attribution-NonCommercial 4.0 International license. The article or book reviews may be accessed both via the World Wide Web – Internet (WWW – Internet), and in printed form, its being permitted, free of charge, to consult and reproduce the text for the personal use of whoever consults it. This authorization of publication has no time limit, with the editors of the journal O que nos faz pensar being responsible for maintaining the identification of the author of the article.