A general formulation of simultaneous inductive-recursive definitions in type theory

DOI10.2307/2586554zbMath0960.03048WikidataQ59540955 ScholiaQ59540955MaRDI QIDQ4508246

Peter Dybjer

Publication date: 3 October 2000

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

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

zbMATH Keywords

Frege structures; intuitionistic type theory; simultaneous inductive-recursive definition

Mathematics Subject Classification ID

03F35: Second- and higher-order arithmetic and fragments

03D70: Inductive definability

Related Items

Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, A Syntax for Higher Inductive-Inductive Types, Dependent Types at Work, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Variations on inductive-recursive definitions, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Normalization by Evaluation for Martin-Löf Type Theory with One Universe, Pure type systems with explicit substitutions, Well-founded recursion with copatterns and sized types, Partiality and recursion in interactive theorem provers – an overview, Containers, monads and induction recursion, From type theory to setoids and back, Rensets and renaming-based recursion for syntax with bindings extended version, An intuitionistic set-theoretical model of fully dependent CC, Map fusion for nested datatypes in intensional type theory, Viewing \({\lambda}\)-terms through maps, Partial and nested recursive function definitions in higher-order logic, Induction-recursion and initial algebras., Predicativity and constructive mathematics, Rensets and renaming-based recursion for syntax with bindings, Finitary higher inductive types in the groupoid model, Constructing a universe for the setoid model, Canonicity for cubical type theory, Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory, Regular universes and formal spaces, Indexed induction-recursion, From realizability to induction via dependent intersection, Another Look at Function Domains, A Brief Overview of Agda – A Functional Language with Dependent Types, Working with Mathematical Structures in Type Theory, Least and Greatest Fixpoints in Game Semantics, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance, An induction principle for nested datatypes in intensional type theory, Typed Applicative Structures and Normalization by Evaluation for System F ω

Cites Work

• Propositional functions and families of types
• Inaccessibility in constructive set theory and type theory
• Inductive families
• Intuitionistic model constructions and normalization proofs
• The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
• Normalization and the Yoneda embedding
• A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
• Unnamed Item