scientific article; zbMATH DE number 7407785

MaRDI QIDQ5155674

Pierre Hyvernat

Publication date: 8 October 2021

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

continuous functionsAgdadependent type theorycoinductive typesindexed containersinductive recursive definitions

Mathematics Subject Classification ID

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

Uses Software

• cubicaltt
• Cubical agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Induction-recursion and initial algebras.
• Inductively generated formal topologies.
• Coequalizers and free triples
• Programming interfaces and basic topology
• A predicative analysis of structural recursion
• Continuous Functions on Final Coalgebras
• Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)
• Relating coalgebraic notions of bisimulation
• Representations of Stream Processors Using Nested Fixed Points
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Polynomial functors and polynomial monads
• A set constructor for inductive sets in Martin-Löf's type theory
• A final coalgebra theorem
• Non-wellfounded trees in Homotopy Type Theory
• Indexed containers
• A Linear Category of Polynomial Functors (extensional part)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Types for Proofs and Programs
• A linear category of polynomial diagrams