Cover Image

Algebraic Type Theory, Part 1: Martin-Löf algebras

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Awodey, Steve
Format:	Preprint
Published:	2025
Subjects:	Category Theory Logic 18C40, 18C50, 03B38
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Non-Standard Models of Homotopy Type Theory
by: Rasekh, Nima
Published: (2025)

Type Theory for the Working Mathematical Music Theorist
by: Flieder, Drew
Published: (2025)

Simplicial Homotopy Type Theory is not just Simplicial: What are $\infty$-Categories?
by: Rasekh, Nima
Published: (2025)

On logical parameterizations and functional representability in local set theories
by: Hernández, Enrique Ruiz, et al.
Published: (2021)

The biequivalence of path categories and axiomatic Martin-Löf type theories
by: Otten, Daniël, et al.
Published: (2025)

The algebraic internal groupoid model of Martin-Löf type theory
by: Hughes, Calum
Published: (2025)

Kripke-Joyal forcing for type theory and uniform fibrations
by: Awodey, S., et al.
Published: (2021)

A Topos-Theoretic Semantics of Intuitionistic Modal Logic with an Application to the Logic of Branching Spacetime
by: Lambert, Michael J.
Published: (2024)

An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction
by: Maietti, Maria Emilia, et al.
Published: (2025)

A 2-categorical approach to the semantics of dependent type theory with computation axioms
by: Spadetto, Matteo
Published: (2025)

The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems
by: van Woerkom, Wijnand, et al.
Published: (2024)

Duality for Clans: an Extension of Gabriel-Ulmer Duality
by: Frey, Jonas
Published: (2023)

On the theories classified by an étendue
by: Wrigley, Joshua
Published: (2025)

Topoi with enough points
by: Di Liberti, Ivan, et al.
Published: (2024)

Categorical Framework for Typed Extensional and Intensional Models in Formal Semantics
by: Quigley, Daniel
Published: (2024)

Games as recursive coalgebras: A categorical view on the Nim-sum
by: Hora, Ryuya
Published: (2025)

Biased elementary doctrines and quotient completions
by: Cioffo, Cipriano Junior
Published: (2023)

Arrow algebras
by: Berg, Benno van den, et al.
Published: (2023)

Toward the effective 2-topos
by: Awodey, Steve, et al.
Published: (2025)

A 2-categorical analysis of context comprehension
by: Coraglia, Greta, et al.
Published: (2024)

Solution to Lawvere's first problem: a Grothendieck topos that has proper class many quotient topoi
by: Kamio, Yuhi, et al.
Published: (2024)

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

Extensional concepts in intensional type theory, revisited
by: Kapulkin, Chris, et al.
Published: (2023)

Craig Interpolation for Subgeometric Logics
by: Di Liberti, Ivan, et al.
Published: (2026)

$(\infty,1)$-Categorical Comprehension Schemes
by: Stenzel, Raffael
Published: (2020)

A 2-categorical proof of Frobenius for fibrations defined from a generic point
by: Hazratpour, Sina, et al.
Published: (2022)

Hilbert spaces admit no finitary discrete imaginaries
by: Chen, Ruiyuan, et al.
Published: (2025)

On the $\infty$-topos semantics of homotopy type theory
by: Riehl, Emily
Published: (2022)

On duality and model theory for polyadic spaces
by: van Gool, Sam, et al.
Published: (2022)

Free Doubly-Infinitary Distributive Categories are Cartesian Closed
by: Nunes, Fernando Lucatelli, et al.
Published: (2024)

The List Object Endofunctor is Polynomial
by: Desrochers, Samuel
Published: (2025)

Sketches and Classifying Logoi
by: Di Liberti, Ivan, et al.
Published: (2024)

A topos for extended Weihrauch degrees
by: Maschio, Samuele, et al.
Published: (2025)

Connectedness through decidable quotients
by: Hernández, Enrique Ruiz, et al.
Published: (2023)

Internal sums for synthetic fibered $(\infty,1)$-categories
by: Weinberger, Jonathan
Published: (2022)

2-Segal sets and pseudomonoids in the bicategory of spans
by: Marx, Sophia E, et al.
Published: (2025)

Dose-Escalation Trial Protocols that Extend Naturally to Admit Titration
by: Norris, David C.
Published: (2025)

The elementary theory of the 2-category of small categories
by: Hughes, Calum, et al.
Published: (2024)

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

Cofibrant generation of pure monomorphisms in presheaf categories
by: Cox, Sean, et al.
Published: (2025)