The Local Universes Model
From MaRDI portal
Publication:2957763
DOI10.1145/2754931zbMath1354.03101arXiv1411.1736OpenAlexW4293252599WikidataQ59757170 ScholiaQ59757170MaRDI QIDQ2957763
Michael A. Warren, Peter LeFanu Lumsdaine
Publication date: 30 January 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1411.1736
Categorical logic, topoi (03G30) Combinatory logic and lambda calculus (03B40) Topological categories, foundations of homotopy theory (55U40)
Related Items
Modalities in homotopy type theory ⋮ AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ An interpretation of dependent type theory in a model category of locally cartesian closed categories ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Unnamed Item ⋮ Identity types and weak factorization systems in Cauchy complete categories ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Homotopical inverse diagrams in categories with attributes ⋮ A type theory for synthetic $\infty$-categories ⋮ Displayed Categories ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ Univalence in locally Cartesian closed categories ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Semantics of higher inductive types ⋮ A cubical model of homotopy type theory ⋮ Model structures on categories of models of type theories ⋮ Modal dependent type theory and dependent right adjoints ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Models of Type Theory Based on Moore Paths ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Natural models of homotopy type theory ⋮ Categories with Families: Unityped, Simply Typed, and Dependently Typed ⋮ Univalence and completeness of Segal objects ⋮ MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The identity type weak factorisation system
- Generalized algebraic theories and contextual categories
- Comprehension categories and the semantics of type dependency
- Revisiting the categorical interpretation of dependent type theory
- Topological and Simplicial Models of Identity Types
- Homotopy-Theoretic Models of Type Theory
- Locally cartesian closed categories and type theory
- Homotopy theoretic models of identity types
- Strong stacks and classifying spaces
- Type Theory and Homotopy
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalence for inverse diagrams and homotopy canonicity
This page was built for publication: The Local Universes Model
