Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor.

DOI10.4230/LIPICS.FSCD.2021.22MaRDI QIDQ6159938zbMATH OpenOpenAlexFDO

Authors Niccolò Veltri

Publication date 23 June 2023

Full work available at URL https://doi.org/10.4230/LIPIcs.FSCD.2021.22

zbMATH Keywords

cubical agdafinal coalgebrafinite powersettype theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX) Theory of computing (68Qxx)

Recommendations

• On the final sequence of a finitary set functor
• Logical construction of final coalgebras
• Realization of coinductive types
• A note on expressive coalgebraic logics for finitary set functors
• On final coalgebras of power-set functors and saturated trees

Cited in

(6)

• scientific article; zbMATH DE number 5080413 (Why is no real title available?)
• Quotients of bounded natural functors
• A concrete final coalgebra theorem for ZF set theory
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• The category of iterative sets in homotopy type theory and univalent foundations
• Terminal coalgebras and non-wellfounded sets in homotopy type theory

This page was built for publication: Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6159938)