Cover Image

Type Theory with Explicit Universe Polymorphism (revised and extended version)

Fuente: arXiv

Saved in:

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

Similar Items

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
by: Bezem, Marc, et al.
Published: (2026)

Internal Effectful Forcing in System T
by: Escardo, Martin H., et al.
Published: (2025)

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
by: Gylterud, Håkon Robbestad, et al.
Published: (2020)

Univalent Material Set Theory
by: Gylterud, Håkon Robbestad, et al.
Published: (2023)

Continuous and algebraic domains in univalent foundations
by: de Jong, Tom, et al.
Published: (2024)

A Coherence Construction for the Propositional Universe
by: Huang, Xu
Published: (2024)

On symmetries of spheres in univalent foundations
by: Cagne, Pierre, et al.
Published: (2024)

Complexity of some modal logics of density (extended version)
by: Balbiani, Philippe, et al.
Published: (2025)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
by: Farmer, William M., et al.
Published: (2023)

How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)
by: Cerda, Rémy, et al.
Published: (2023)

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)

Continuations and Completeness in Proof-theoretic Semantics
by: Gu, Tao, et al.
Published: (2026)

DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift
by: Poernomo, Iman
Published: (2025)

Formal P-Category Theory and Normalization by Evaluation in Rocq
by: Berry, David G., et al.
Published: (2025)

Meaning as Use, Application, Employment, Purpose, Usefulness
by: de Queiroz, Ruy J. G. B.
Published: (2025)

From the Notebooks to the Investigations and Beyond
by: de Queiroz, Ruy J. G. B.
Published: (2025)

A vector logic for extensional formal semantics
by: Quigley, Daniel
Published: (2024)

Universal Algebra in UniMath
by: Amato, Gianluca, et al.
Published: (2021)

Y is a least fixed point combinator
by: Helfer, Joseph
Published: (2025)

Examples and counterexamples of injective types
by: de Jong, Tom, et al.
Published: (2026)

2-Coherent Internal Models of Homotopical Type Theory
by: Chen, Joshua
Published: (2025)

A New Overture to Classical Simple Type Theory, Ketonen-type Gentzen and Tableau Systems
by: Miwa, Tadayoshi, et al.
Published: (2026)

On the computational properties of ambivalent sets and functions
by: Normann, Dag, et al.
Published: (2026)

Dismantling the Surprise Test "Paradox"
by: Dietzfelbinger, Martin
Published: (2026)

Glivenko's theorems from an ecumenical perspective
by: Pereira, Luiz Carlos, et al.
Published: (2026)

First-Order Fischer Servi Logic
by: Christensen, Ahmee
Published: (2024)

Normal forms in cubical type theory
by: Huang, Xu
Published: (2026)

Finite Hilbert systems for Weak Kleene logics
by: Greati, Vitor, et al.
Published: (2024)

Knowability as continuity: a topological account of informational dependence
by: Baltag, Alexandru, et al.
Published: (2024)

Axiomatizing the Logic of Ordinary Discourse
by: Greati, Vitor, et al.
Published: (2024)

Generating proof systems for three-valued propositional logics
by: Greati, Vitor, et al.
Published: (2024)

Belief in Simplicial Complexes
by: Sink, Philip, et al.
Published: (2025)

Reasoning Around Paradox with Grounded Deduction
by: Ford, Bryan
Published: (2024)

A Note on Proper Relational Structures
by: Bjorndahl, Adam, et al.
Published: (2025)

Bennett's Conjecture in Lean 4: Counter-Models for the PSR-Reducibility of Spinoza's Propositions V and XIV
by: Nakamura, Yuki
Published: (2026)

The Compatibility of the Minimalist Foundation with Homotopy Type Theory
by: Contente, Michele, et al.
Published: (2022)

Bounded First-Class Universe Levels in Dependent Type Theory
by: Chan, Jonathan, et al.
Published: (2025)

Hennessy-Milner Type Theorems for Fuzzy Multimodal Logics Over Heyting Algebras
by: Stanković, Marko, et al.
Published: (2025)

Undecidability in Relevant Logic
by: Knudstorp, Søren Brinck
Published: (2026)