A Syntax for Higher Inductive-Inductive Types

DOI10.4230/LIPIcs.FSCD.2018.20zbMath1462.68022OpenAlexW2885792094MaRDI QIDQ4993350

Ambrus Kaposi, András Kovács

Publication date: 15 June 2021

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2018/9190/pdf/LIPIcs-FSCD-2018-20.pdf/

zbMATH Keywords

homotopy type theorylogical relationshigher inductive typesinductive-inductive typesquotient inductive types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Related Items (7)

The construction of set-truncated higher inductive types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Type-theoretic approaches to ordinals ⋮ Constructing a universe for the setoid model ⋮ Unnamed Item

Uses Software

• Haskell

Cites Work

• Unnamed Item
• Unnamed Item
• Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
• Inductive families
• Quotient inductive-inductive types
• Finitary higher inductive types in the groupoid model
• Containers: Constructing strictly positive types
• Higher Inductive Types as Homotopy-Initial Algebras
• Type theory in type theory using quotient inductive types
• Proofs for free
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Type Theory based on Dependent Inductive and Coinductive Types
• Constructions with Non-Recursive Higher Inductive Types
• Parametricity and dependent types
• A relationally parametric model of dependent type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: A Syntax for Higher Inductive-Inductive Types