Cover Image

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bezem, Marc, Coquand, Thierry, Dybjer, Peter, Escardó, Martín
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Type Theory with Explicit Universe Polymorphism (revised and extended version)
by: Bezem, Marc, et al.
Published: (2022)

Reduction Free Normalisation for a proof irrelevant type of propositions
by: Coquand, Thierry
Published: (2021)

Non-Derivability Results in Polymorphic Dependent Type Theory
by: Geuvers, Herman
Published: (2026)

On Small Types in Univalent Foundations
by: de Jong, Tom, et al.
Published: (2021)

Constructive higher sheaf models with applications to synthetic mathematics
by: Coquand, Thierry, et al.
Published: (2026)

Two Remarks about Game Semantics of Classical Logic
by: Coquand, Thierry
Published: (2026)

Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
by: Coquand, Thierry
Published: (2026)

An Analysis of Tennenbaum's Theorem in Constructive Type Theory
by: Hermes, Marc, et al.
Published: (2023)

Rings and Boolean Algebras as Algebraic Theories
by: De Faveri, Arturo
Published: (2025)

Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
by: Takahashi, Yuta
Published: (2024)

The equivariant model structure on cartesian cubical sets
by: Awodey, Steve, et al.
Published: (2024)

(Pointed) Univalence in Universe Category Models of Type Theory
by: Kapulkin, Chris, et al.
Published: (2025)

Primitive Recursive Dependent Type Theory
by: Buchholtz, Ulrik, et al.
Published: (2024)

A Naive Encoding of Russell's Paradox in Type Theory
by: Qu, Zhuoyuan
Published: (2025)

Controlling unfolding in type theory
by: Gratzer, Daniel, et al.
Published: (2022)

GATlab: Modeling and Programming with Generalized Algebraic Theories
by: Lynch, Owen, et al.
Published: (2024)

A topological reading of inductive and coinductive definitions in Dependent Type Theory
by: Sabelli, Pietro
Published: (2024)

Case Study: Saturations as Explicit Models in Equational Theories
by: Janota, Mikoláš, et al.
Published: (2026)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
by: Gratzer, Daniel, et al.
Published: (2024)

Groupoidal Realizability for Intensional Type Theory
by: Speight, Sam
Published: (2024)

Coslice Colimits in Homotopy Type Theory
by: Hart, Perry, et al.
Published: (2024)

Universal Proof Theory, TACL 2022 Lecture Notes
by: Iemhoff, Rosalie, et al.
Published: (2023)

Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
by: Mannucci, Mirco A., et al.
Published: (2026)

Open Horn Type Theory
by: Poernomo, Iman
Published: (2025)

Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation
by: Tabatabai, Amirhossein Akbar, et al.
Published: (2018)

Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
by: Tabatabai, Amirhossein Akbar, et al.
Published: (2018)

A Judgmental Construction of Directed Type Theory
by: Neumann, Jacob
Published: (2025)

Are Dependent Types in Set Theory Feasible?
by: Yang, Yunsong, et al.
Published: (2026)

Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
by: Mannucci, Mirco A., et al.
Published: (2025)

Chatelet's Theorem in Synthetic Algebraic Geometry
by: Coquand, Thierry, et al.
Published: (2025)

The Unification Type of an Equational Theory May Depend on the Instantiation Preorder: From Results for Single Theories to Results for Classes of Theories
by: Baader, Franz, et al.
Published: (2026)

The Regular Element Property in Constructive Mathematics
by: Coquand, Thierry
Published: (2024)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Automating Boundary Filling in Cubical Type Theories
by: Doré, Maximilian, et al.
Published: (2024)

Nominal Type Theory by Nullary Internal Parametricity
by: Van Muylder, Antoine, et al.
Published: (2025)

The Groupoid-Syntax of Type Theory is a Set
by: Altenkirch, Thorsten, et al.
Published: (2025)

Polynomial Universes in Homotopy Type Theory
by: Aberlé, C. B., et al.
Published: (2024)

Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts
by: Marković, Đorđe, et al.
Published: (2025)

A Foundation for Differentiable Logics using Dependent Type Theory
by: Affeldt, Reynald, et al.
Published: (2026)

Type Theory With Erasure
by: Theocharis, Constantine, et al.
Published: (2026)