Non-wellfounded trees in Homotopy Type Theory

DOI10.4230/LIPIcs.TLCA.2015.17zbMath1433.03027arXiv1504.02949MaRDI QIDQ5277827

Régis Spadotti, Benedikt Ahrens, Paolo Capriotti

Publication date: 12 July 2017

Full work available at URL: https://arxiv.org/abs/1504.02949

zbMATH Keywords

homotopy type theorycomputer theorem provingcoinductive types

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Related Items (6)

Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Unnamed Item ⋮ Some Wellfounded Trees in UniMath ⋮ From signatures to monads in \textsf{UniMath} ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Uses Software

• Agda

This page was built for publication: Non-wellfounded trees in Homotopy Type Theory