Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2)

Name: Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2)
Published: 2022-03-30T11:58:58Z
License: https://creativecommons.org/licenses/by/4.0/
Keywords: dependent type theory, higher inductive types, quotient types, topos theory, weakly initial set of covers,, well-founded relation

Pitts, Andrew; Fiore, Marcelo; Steenkamp, SC

Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2)

Type

Dataset

Authors

Pitts, Andrew

https://orcid.org/0000-0001-7775-3471

Fiore, Marcelo

https://orcid.org/0000-0001-8558-3492

Steenkamp, SC

Description

Formal proofs for the results in the paper "Quotients, Inductive Types and Quotient Inductive Types" constructed with the Agda theorem proving system.

Version 2 of the dataset updates some links to agree with the published version of the accompanying journal paper and uses Agda version 2.6.2.1 to check the code.