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

final coalgebratype theoryfinite powersetcubical agda

Mathematics Subject Classification ID

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

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

(4)

• scientific article; zbMATH DE number 5080413 (Why is no real title available?)
• A concrete final coalgebra theorem for ZF set theory
• scientific article; zbMATH DE number 7471712 (Why is no real title available?)
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks

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)