scientific article; zbMATH DE number 7003193
From MaRDI portal
DOI10.23638/LMCS-14(4:23)2018MaRDI QIDQ4611379
Publication date: 18 January 2019
Full work available at URL: https://arxiv.org/abs/1712.04864
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Categorical logic, topoi (03G30) Topoi (18B25) Topological categories, foundations of homotopy theory (55U40) Type theory (03B38)
Related Items
Cubical methods in homotopy type theory and univalent foundations, On Church’s thesis in cubical assemblies, A general framework for the semantics of type theory, Two-level type theory and applications, On the ∞$\infty$‐topos semantics of homotopy type theory, Towards a constructive simplicial model of Univalent Foundations, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Model structure on the universe of all types in interval type theory, Syntax and models of Cartesian cubical type theory, MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Isomorphism is equality
- The Frobenius condition, right properness, and uniform fibrations
- A Kripke model for simplicial sets
- Lokal präsentierbare Kategorien. (Locally presentable categories)
- Nominal Sets
- The Local Universes Model
- An algebraic weak factorisation system on 01-substitution sets: a constructive proof
- A homotopy-theoretic model of function extensionality in the effective topos
- Natural models of homotopy type theory
- Modular correspondence between dependent type theories and categories including pretopoi and topoi
- On a Topological Topos
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Internal type theory
- Guarded Cubical Type Theory: Path Equality for Guarded Recursion
- Homotopy Type Theory: Univalent Foundations of Mathematics
- FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
