scientific article; zbMATH DE number 2079044
From MaRDI portal
Publication:4474857
Recommendations
- The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
- Locally cartesian closed categories and type theory
- An interpretation of dependent type theory in a model category of locally cartesian closed categories
- Locally Cartesian closed quasi-categories from type theory
- A cartesian closed category in Martin-Löf's intuitionistic type theory
- scientific article; zbMATH DE number 4010480
- Revisiting the categorical interpretation of dependent type theory
- Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
- scientific article; zbMATH DE number 4103048
- The maximality of the typed lambda calculus and of cartesian closed categories
Cited in
(57)- A minimalist two-level foundation for constructive mathematics
- Comprehension categories and the semantics of type dependency
- Wellfounded trees in categories
- A cartesian closed category in Martin-Löf's intuitionistic type theory
- The simplicial model of univalent foundations (after Voevodsky)
- Axiomatic reals and certified efficient exact real computation
- Revisiting the categorical interpretation of dependent type theory
- Combinatorial structure of type dependency
- Containers: Constructing strictly positive types
- Modeling Martin-Löf type theory in categories
- Dependent types and fibred computational effects
- Joyal's arithmetic universes via type theory
- Towards formalizing categorical models of type theory in type theory
- A constructive manifestation of the Kleene-Kreisel continuous functionals
- Homotopy type theory and Voevodsky's univalent foundations
- Products of families of types and (Pi,lambda)-structures on C-systems
- The local universes model: an overlooked coherence construction for dependent type theories
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- Natural models of homotopy type theory
- Locally Cartesian closed quasi-categories from type theory
- scientific article; zbMATH DE number 445156 (Why is no real title available?)
- Locally cartesian closed categories and type theory
- Two-dimensional models of type theory
- Kripke Semantics for Martin-Löf’s Extensional Type Theory
- scientific article; zbMATH DE number 4010480 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
- Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
- Internal type theory
- Functional completeness of the free locally Cartesian closed category and interpretations of Martin-Löf's theory of dependent types
- Propositions as [Types]
- Dependent inductive and coinductive types are fibrational dialgebras
- Categories with families: unityped, simply typed, and dependently typed
- 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
- On generalized algebraic theories and categories with families
- Denotational semantics for guarded dependent type theory
- Exact completion and constructive theories of sets
- Modal dependent type theory and dependent right adjoints
- Type theory and homotopy
- The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
- Locally cartesian closed categories without chosen constructions
- A generalization of the Takeuti-Gandy interpretation
- MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
- A general framework for the semantics of type theory
- Towards a constructive simplicial model of Univalent Foundations
- Kripke-Joyal forcing for type theory and uniform fibrations
- Semantics of multimodal adjoint type theory
- A categorical approach to DIBI models
- -type theories
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- Extracting efficient exact real number computation from proofs in constructive type theory
- A 2-categorical approach to the semantics of dependent type theory with computation axioms
- Formalising inductive and coinductive containers
- Non-well-founded trees in categories
- The identity type weak factorisation system
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4474857)
