A syntax for higher inductive-inductive types

DOI10.4230/LIPICS.FSCD.2018.20MaRDI QIDQ4993350zbMATH OpenOpenAlexFDO

Authors 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

higher inductive typeshomotopy type theoryinductive-inductive typeslogical relationsquotient inductive types

Mathematics Subject Classification ID

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

Recommendations

• Quotient inductive-inductive types
• Semantics of higher inductive types
• Inductive-inductive definitions
• A categorical semantics for inductive-inductive definitions
• Type theory in type theory using quotient inductive types

Cites work

• A general formulation of simultaneous inductive-recursive definitions in type theory
• A relationally parametric model of dependent type theory
• Canonicity of weak -groupoid laws using parametricity theory
• Constructions with non-recursive higher inductive types
• Containers: Constructing strictly positive types
• Finitary higher inductive types in the groupoid model
• Higher inductive types as homotopy-initial algebras
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 1342277 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• Inductive families
• Parametricity and dependent types
• Proofs for free. Parametricity for dependent types
• Quotient inductive-inductive types
• Type theory based on dependent inductive and coinductive types
• Type theory in type theory using quotient inductive types

Cited in

(17)

• Quotient inductive-inductive types
• Finitary higher inductive types in the groupoid model
• The construction of set-truncated higher inductive types
• Constructing a universe for the setoid model
• Type-theoretic approaches to ordinals
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• Constructing higher inductive types as groupoid quotients
• Quotients, inductive types, and quotient inductive types
• Large and infinitary quotient inductive-inductive types
• Signatures and induction principles for higher inductive-inductive types
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• For Finitary Induction-Induction, Induction is Enough
• scientific article; zbMATH DE number 7756115 (Why is no real title available?)
• A syntax for mutual inductive families
• Second-order generalised algebraic theories: signatures and first-order semantics
• Initial algebras of domains via quotient inductive-inductive types
• Type inference with recursive types: Syntax and semantics

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: A syntax for higher inductive-inductive types

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