Representing continuous functions between greatest fixed points of indexed containers

MaRDI QIDQ5155674zbMATH OpenFDO

Authors Pierre Hyvernat

Publication date 8 October 2021

Full work available at URL https://arxiv.org/abs/1902.10971, https://lmcs.episciences.org/7712

zbMATH Keywords

Agdacoinductive typescontinuous functionsdependent type theoryindexed containersinductive recursive definitions

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Continuous functions on final coalgebras
• Continuous functions on final coalgebras
• Representations of stream processors using nested fixed points
• General Recursion via Coinductive Types
• From Coinductive Proofs to Exact Real Arithmetic

Cites work

• A final coalgebra theorem
• A general formulation of simultaneous inductive-recursive definitions in type theory
• A linear category of polynomial diagrams
• A Linear Category of Polynomial Functors (extensional part)
• A predicative analysis of structural recursion
• A set constructor for inductive sets in Martin-Löf's type theory
• Coequalizers and free triples
• Continuous functions on final coalgebras
• Cubical type theory: a constructive interpretation of the univalence axiom
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 517090 (Why is no real title available?)
• scientific article; zbMATH DE number 7288622 (Why is no real title available?)
• Indexed containers
• Induction-recursion and initial algebras.
• Inductively generated formal topologies.
• Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
• Non-wellfounded trees in homotopy type theory
• Polynomial functors and polynomial monads
• Programming interfaces and basic topology
• Relating coalgebraic notions of bisimulation
• Representations of stream processors using nested fixed points
• Types for Proofs and Programs

Cited in

(2)

• Formal definitions and proofs for partial (co)recursive functions
• Continuous functions on final comodels of free algebraic theories

Describes a project that uses

Uses Software

• cubicaltt
• Cubical Agda

This page was built for publication: Representing continuous functions between greatest fixed points of indexed containers

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