Some Wellfounded Trees in UniMath

DOI10.1007/978-3-319-42432-3_2zbMath1434.03023OpenAlexW2475593741MaRDI QIDQ2819193

Anders Mörtberg, Benedikt Ahrens

Publication date: 28 September 2016

Published in: Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-42432-3_2

zbMATH Keywords

proof assistantinitial algebrasinductive datatypesunivalent type theoryUniMath

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items (1)

Heterogeneous Substitution Systems Revisited

Uses Software

• Coq
• Coq/SSReflect
• UniMath
• cubicaltt

Cites Work

• Substitution in non-wellfounded syntax with variable binding
• Inductive Types in Homotopy Type Theory
• de Bruijn notation as a nested datatype
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Non-wellfounded trees in Homotopy Type Theory
• Univalent categories and the Rezk completion
• An experimental library of formalized Mathematics based on the univalent foundations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Some Wellfounded Trees in UniMath