Some wellfounded trees in UniMath

Benedikt Ahrens*, Anders Mörtberg

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)


UniMath, short for "Univalent Mathematics", refers to both a language (a.k.a. a formal system) for mathematics, as well as to a computer-checked library of mathematics formalized in that system. The UniMath library, under active development, aims to coherently integrate machine-checked proofs of mathematical results from many different branches of mathematics. The UniMath language is a dependent type theory, augmented by the univalence axiom. One goal is to keep the language as small as possible, to ease verification of the theory. In particular, general inductive types are not part of the language. In this work, we partially remedy this lack by constructing some inductive (families of) sets. This involves a formalization of a standard category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the inductive sets thus obtained. The present work constitutes one part of a construction of a framework for specifying, via a signature, programming languages with binders as nested datatypes. To this end, we are going to combine our work with previous work by Ahrens and Matthes (itself based on work by Matthes and Uustalu) on an axiomatisation of substitution for languages with variable binding. The languages specified via the framework will automatically be equipped with the structure of a monad, where the monadic operations and axioms correspond to a well-behaved substitution operation.

Original languageEnglish
Title of host publicationMathematical Software - ICMS 2016
Subtitle of host publication5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings
EditorsGert-Martin Greuel, Thorsten Koch, Peter Paule, Andrew Sommese
PublisherSpringer Verlag
ISBN (Electronic)9783319424323
ISBN (Print)9783319424316
Publication statusPublished - 6 Jul 2016
Event5th International Conference on Mathematical Software, ICMS 2016 - Berlin, Germany
Duration: 11 Jul 201614 Jul 2016

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference5th International Conference on Mathematical Software, ICMS 2016


  • Inductive datatypes
  • Initial algebras
  • Proof assistant
  • UniMath
  • Univalent type theory

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Some wellfounded trees in UniMath'. Together they form a unique fingerprint.

Cite this