From signatures to monads in UniMath

Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)
170 Downloads (Pure)


The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it—in particular, general inductive types are not part of the system. In this work, we partially remedy the lack of inductive types by constructing some set-level datatypes and their associated induction principles from other type constructors. This involves a formalization of a category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the datatypes obtained. We also connect this construction to a previous formalization of substitution for languages with variable binding. Altogether, we construct a framework that allows us to concisely specify, via a simple notion of binding signature, a language with variable binding. From such a specification we obtain the datatype of terms of that language, equipped with a certified monadic substitution operation and a suitable recursion scheme. Using this we formalize the untyped lambda calculus and the raw syntax of Martin-Löf type theory.
Original languageEnglish
Pages (from-to)285-318
Number of pages34
JournalJournal of Automated Reasoning
Issue number2
Early online date11 Jul 2018
Publication statusPublished - 15 Aug 2019
EventWorkshop on Homotopy Type Theory and Univalent Foundations of Mathematics - Ontario, Canada
Duration: 16 May 201620 Jun 2016


  • Univalent mathematics
  • Initial algebra semantics
  • Inductive types
  • Representation of substitution

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence
  • Computational Theory and Mathematics


Dive into the research topics of 'From signatures to monads in UniMath'. Together they form a unique fingerprint.

Cite this