For Finitary Induction-Induction, Induction is Enough

DOI10.4230/lipics.types.2019.6OpenAlexW3088552701MaRDI QIDQ6079233

András Kovács, Ambrus Kaposi, Ambroise Lafont

Publication date: 27 October 2023

Full work available at URL: https://hal-imt-atlantique.archives-ouvertes.fr/hal-03594037

zbMATH Keywords

type theoryinductive typesinductive-inductive types

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Constructing a universe for the setoid model

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Generalized algebraic theories and contextual categories
• Quotient inductive-inductive types
• Constructing inductive-inductive types in cubical type theory
• From signatures to monads in \textsf{UniMath}
• Type Theory Should Eat Itself
• Type theory in type theory using quotient inductive types
• Positive Inductive-Recursive Definitions
• Inductive-Inductive Definitions
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• Internal type theory
• Impredicative Encodings of (Higher) Inductive Types
• Large and Infinitary Quotient Inductive-Inductive Types
• Indexed containers
• A relationally parametric model of dependent type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: For Finitary Induction-Induction, Induction is Enough