Modular correspondence between dependent type theories and categories including pretopoi and topoi
From MaRDI portal
Publication:3371526
DOI10.1017/S0960129505004962zbMath1093.03042OpenAlexW2120677003MaRDI QIDQ3371526
Publication date: 21 February 2006
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129505004962
Categorical logic, topoi (03G30) Topoi (18B25) Metamathematics of constructive systems (03F50) Axiom of choice and related propositions (03E25)
Related Items (25)
From type theory to setoids and back ⋮ On Church’s thesis in cubical assemblies ⋮ A Minimalist Foundation at Work ⋮ Dialectica logical principles ⋮ Quotient completion for the foundation of constructive mathematics ⋮ The linear-non-linear substitution 2-monad ⋮ A class of higher inductive types in Zermelo‐Fraenkel set theory ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ A constructive picture of Noetherian conditions and well quasi-orders ⋮ A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets ⋮ An induction principle for consequence in arithmetic universes ⋮ On Choice Rules in Dependent Type Theory ⋮ The identity type weak factorisation system ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ Setoids and universes ⋮ The existential completion ⋮ A minimalist two-level foundation for constructive mathematics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Models of Type Theory Based on Moore Paths ⋮ LIFSCHITZ REALIZABILITY AS A TOPOLOGICAL CONSTRUCTION ⋮ Maximal ideals in countable rings, constructively
Uses Software
This page was built for publication: Modular correspondence between dependent type theories and categories including pretopoi and topoi
