Internal strict propositions using point-free equations

Donkó, István and Kaposi, Ambrus (2022) Internal strict propositions using point-free equations. Leibniz International Proceedings in Informatics (LIPIcs), 2nd International Symposium on Computational Geometry (SoCG 2016), 239. 6:1-6:21. ISSN 1868-8969

Preview

Text LIPIcs-TYPES-2021-6.pdf - Accepted Version Available under License Creative Commons Attribution. Download (787kB) | Preview

Abstract

The setoid model of Martin-Löf’s type theory bootstraps extensional features of type theory from intensional type theory equipped with a universe of definitionally proof irrelevant (strict) propositions. Extensional features include a Prop-valued identity type with a strong transport rule and function extensionality. We show that a setoid model supporting these features can be defined in intensional type theory without any of these features. The key component is a point-free notion of propositions. Our construction suggests that strict algebraic structures can be defined along the same lines in intensional type theory.

Actions (login required)

Edit Item