Type theory with explicit universe polymorphism

DOI10.4230/LIPICS.TYPES.2022.13MaRDI QIDQ6643043

Martín Escardo, Thierry Coquand, Marc Bezem, Peter Dybjer

Publication date: 26 November 2024

zbMATH Keywords

type theoryuniverse polymorphismconstraint-indexed productslevel-indexed productsuniverses in type theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Sharing proofs with predicative theories through universe-polymorphic elaboration

This page was built for publication: Type theory with explicit universe polymorphism

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