Constructing infinitary quotient-inductive types

DOI10.1007/978-3-030-45231-5_14MaRDI QIDQ2200826zbMATH OpenOpenAlexFDO

Authors Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp

Publication date 23 September 2020

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

category theorydependent type theoryhigher inductive typesinductive-inductive definitionsquotient typessized types

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Recommendations

• Quotients, inductive types, and quotient inductive types
• Large and infinitary quotient inductive-inductive types
• Type theory in type theory using quotient inductive types
• Quotient inductive-inductive types
• Constructing higher inductive types as groupoid quotients

Cites work

• A feature constraint system for logic programming with entailment
• A formally verified interpreter for a shell-like programming language
• Deciding the first-order theory of an algebra of feature trees with updates
• Feature-constraint logics for unification grammars
• Local Reasoning for the POSIX File System
• Records for logic programming

Cited in

(8)

• Infinite products of recursive equivalence types
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Constructing initial algebras using inflationary iteration
• Quotients, inductive types, and quotient inductive types
• Quotients over Minimal Type Theory
• Type theory in type theory using quotient inductive types
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• Capturing constrained constructor patterns in matching logic

Describes a project that uses

Uses Software

• Agda

This page was built for publication: Constructing infinitary quotient-inductive types

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