A construction of non-well-founded sets within Martin-Löf's type theory

DOI10.2307/2275015zbMath0669.03028OpenAlexW1972002041MaRDI QIDQ3822156

Ingrid Lindström

Publication date: 1989

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275015

zbMATH Keywords

Martin-Löf's type theoryconstructive interpretation of non-well-founded setsHallnäs' limit definition

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

Related Items (7)

Inaccessible set axioms may have little consistency strength ⋮ A computable expression of closure to efficient causation ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Constructive sets in computable sets ⋮ Indexed containers ⋮ W-types in homotopy type theory ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory

This page was built for publication: A construction of non-well-founded sets within Martin-Löf's type theory