Cover Image

Extensional concepts in intensional type theory, revisited

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Kapulkin, Chris, Li, Yufeng
Format:	Preprint
Published:	2023
Subjects:	Logic Logic in Computer Science Category Theory 03B38, 18N45
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Logical Structure on Inverse Functor Categories
by: Fiore, Marcelo, et al.
Published: (2024)

A type-theoretic definition of lax $(\infty,\infty)$-limits
by: Mikhail, Thomas Jan
Published: (2024)

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

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

Generalized Chevalley criteria in simplicial homotopy type theory
by: Weinberger, Jonathan
Published: (2024)

Yet another cubical type theory, but via a semantic approach
by: Kapulkin, Chris, et al.
Published: (2025)

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

Synthetic perspectives on spaces and categories
by: Riehl, Emily
Published: (2025)

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

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)

The Sup Connective in IMALL: A Categorical Semantics
by: Díaz-Caro, Alejandro, et al.
Published: (2022)

Beyond Eckmann-Hilton: Commutativity in Higher Categories
by: Benjamin, Thibaut, et al.
Published: (2025)

Two-sided cartesian fibrations of synthetic $(\infty,1)$-categories
by: Weinberger, Jonathan
Published: (2022)

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

Smooth and Proper Maps
by: Anel, Mathieu, et al.
Published: (2024)

The Yoneda embedding in simplicial type theory
by: Gratzer, Daniel, et al.
Published: (2025)

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

Directed univalence in simplicial homotopy type theory
by: Gratzer, Daniel, et al.
Published: (2024)

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

A Toolkit for Structured Lifts
by: Kapulkin, Chris, et al.
Published: (2025)

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

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

Projective Presentations of Lex Modalities
by: Williams, Mark Damuni
Published: (2025)

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

Algebraic Type Theory, Part 1: Martin-Löf algebras
by: Awodey, Steve
Published: (2025)

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

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

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

Domains and Classifying Topoi
by: Sterling, Jonathan, et al.
Published: (2025)

The free bifibration on a functor
by: Clarke, Bryce, et al.
Published: (2025)

Cubical coherent confluence, $ω$-groupoids and the cube equation
by: Malbos, Philippe, et al.
Published: (2025)

A Completeness Theorem for Topological Doctrines
by: Ghilardi, Silvio, et al.
Published: (2025)

Model theory in compactly generated (tensor-)triangulated categories
by: Prest, Mike, et al.
Published: (2023)

Substructural fixed-point theorems and the diagonal argument: theme and variations
by: Roberts, David Michael
Published: (2021)

Ext groups in Homotopy Type Theory
by: Christensen, J. Daniel, et al.
Published: (2023)

Monoidal bicategories, differential linear logic, and analytic functors
by: Fiore, M., et al.
Published: (2024)

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

Logic and Concepts in the 2-category of Topoi
by: Di Liberti, Ivan, et al.
Published: (2025)