We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Quotients, inductive types, and quotient inductive types

Abstract: This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2101.02994 [cs.LO]
  (or arXiv:2101.02994v1 [cs.LO] for this version)

Submission history

From: S. C. Steenkamp [view email]
[v1] Fri, 8 Jan 2021 13:00:52 GMT (181kb,D)

Link back to: arXiv, form interface, contact.