Adams, Robin ;
Bezem, Marc ;
Coquand, Thierry
A Normalizing Computation Rule for Propositional Extensionality in HigherOrder Minimal Logic
Abstract
The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity  that every closed term computes to a canonical form. A computation becomes "stuck" when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed using a nominal extension of lambdacalculus, it may be interesting to explore alternative solutions, which do not require such an extension.
As a first step, we present here a system of propositional higherorder minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Omega. There are proofs which inhabit propositions, which are the terms of type Omega. The canonical propositions are those constructed from false by implication. Thirdly, there are paths which inhabit equations M =_A N, where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality  logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity.
We present a callbyname reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term headreduces to a canonical form. This work has been formalised in Agda.
BibTeX  Entry
@InProceedings{adams_et_al:LIPIcs:2018:9858,
author = {Robin Adams and Marc Bezem and Thierry Coquand},
title = {{A Normalizing Computation Rule for Propositional Extensionality in HigherOrder Minimal Logic}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {3:13:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770651},
ISSN = {18688969},
year = {2018},
volume = {97},
editor = {Silvia Ghilezan and Herman Geuvers and Jelena Ivetić},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9858},
URN = {urn:nbn:de:0030drops98581},
doi = {10.4230/LIPIcs.TYPES.2016.3},
annote = {Keywords: type theory, univalence, canonicity}
}
05.11.2018
Keywords: 

type theory, univalence, canonicity 
Seminar: 

22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Issue date: 

2018 
Date of publication: 

05.11.2018 