Kripke-Joyal forcing for type theory and uniform fibrations
type: Item
instance of: scholarly article
title: Kripke-Joyal forcing for type theory and uniform fibrations
author: Steve Awodey
author: Nicola Gambino
author: Sina Hazratpour
published in: Selecta Mathematica. New Series
publication date: 2024-08-13T00:00:00Z
Mathematics Subject Classification ID: 03C25
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18B25
Mathematics Subject Classification ID: 18C50
Mathematics Subject Classification ID: 55P05
zbMATH DE Number: 7896247
MaRDI profile type: Publication
cites work: Syntax and models of Cartesian cubical type theory
cites work: A cubical model of homotopy type theory
cites work: Natural models of homotopy type theory
cites work: Propositions as [Types]
cites work: Kripke Semantics for Martin-L\"of's Extensional Type Theory
cites work: Homotopy theoretic models of identity types
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Q2968413
cites work: La logique des topos
cites work: Algebraic weak factorisation systems. I: Accessible AWFS.
cites work: Algebraic weak factorisation systems. II: Categories of weak maps.
cites work: Varieties of Cubical Sets
cites work: Q3424496
cites work: Cubical Type Theory: a constructive interpretation of the univalence axiom
cites work: The identity type weak factorisation system
cites work: Towards a constructive simplicial model of Univalent Foundations
cites work: Polynomial functors and polynomial monads
cites work: MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
cites work: The Frobenius condition, right properness, and uniform fibrations
cites work: Understanding the small object argument
cites work: Q3539846
cites work: Q4474857
cites work: Q4225149
cites work: Q4783274
cites work: Q4853985
cites work: Q4993352
cites work: Modular correspondence between dependent type theories and categories including pretopoi and topoi
cites work: Dependently Typed Programming in Agda
cites work: Q4611379
cites work: Q4117992
cites work: Categorical homotopy theory
cites work: Locally cartesian closed categories and type theory
cites work: An algebraic weak factorisation system on 01-substitution sets: a constructive proof
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Homotopy Type Theory: Univalent Foundations of Mathematics
cites work: An experimental library of formalized Mathematics based on the univalent foundations
cites work: Topological and Simplicial Models of Identity Types
DOI: 10.1007/S00029-024-00962-2
description: scientific article; zbMATH DE number 7896247