An intuitionistic set-theoretical model of fully dependent CC

DOI10.1017/S0960129523000087arXiv2010.12504MaRDI QIDQ6174091FDOQ6174091

Authors: Masahiro Sato, Jacques Garrigue 

Publication date: 13 July 2023

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Abstract: Werner's set-theoretical model is one of the simplest models of CIC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle holds. Following our previous work, we interpret Prop into a topological space (a special case of Heyting algebra) to make the model more intuitionistic without sacrificing simplicity. We improve on that work by providing a full interpretation of dependent product types, using Alexandroff spaces. We also extend our approach to inductive types by adding support for lists.

Full work available at URL: https://arxiv.org/abs/2010.12504

zbMATH Keywords

modelintuitionistic logictype theory

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Sheaves in geometry and logic: a first introduction to topos theory
• Categorical logic and type theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Homotopy type theory. Univalent foundations of mathematics
• Sets in Coq, Coq in Sets
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Title not available (Why is that?)
• The calculus of constructions
• Proof-irrelevant model of CC with predicative induction and judgmental equality
• Title not available (Why is that?)
• Title not available (Why is that?)
• A general formulation of simultaneous inductive-recursive definitions in type theory
• On the strength of proof-irrelevant type theories
• Introduction to generalized type systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• A higher-order calculus and theory abstraction
• Title not available (Why is that?)
• Title not available (Why is that?)
• A simple model construction for the calculus of constructions

This page was built for publication: An intuitionistic set-theoretical model of fully dependent CC

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174091)