A Logical Relation for Setoid Type Theory in Agda
Creators: name: Pujet Loïc
name: Tabareau Nicolas
Publisher: name: Zenodo
Year: 2021

description: # A Logical Relation for Setoid Type Theory in Agda # This is a formalized proof of the decidability of conversion for an<br> extension of Martin Löf type theory with an equality satisfying UIP,<br> function extensionality, and propositional extensionality. The source code can be browsed in HTML [here](https://htmlpreview.github.io/?https://github.com/CoqHott/logrel-mltt/blob/setoid-universes-hierarchy/html/README.html). The companion paper can be found [here](https://hal.inria.fr/hal-03367052) ### Setoid Type Theory ### The type theory under scrutiny is a simplified version of TT&lt;sup&gt;obs&lt;/sup&gt;, as described in the companion<br> paper.<br> It features:<br> - A hierarchy of universes for proof-relevant types, and one for proof-irrelevant types,<br> - dependent products, with domain and codomain in any universe,<br> - dependent pairs with proof-irrelevant domain and codomain ("existential types"),<br> - proof-irrelevant identity types and type casting along equalities in the universes,<br> - natural numbers and a proof-irrelevant empty type.<br> However, it is subject to the following restrictions:<br> - The universe hierarchies are restricted to two levels,<br> - no general inductive types,<br> - no equality types à la Swan,<br> - no quotient types. The interested reader is invited to consult either the companion paper or the formalized definitions<br> for a more detailed account of TT&lt;sup&gt;obs&lt;/sup&gt;. ### Structure of the proof ### The raw, untyped syntax is defined inductively, followed by an inductive definition of the typing<br> derivations of TT&lt;sup&gt;obs&lt;/sup&gt;. The proof then relies on Agda's implementation of induction-recursion to define a logical relation<br> that characterizes the computational behaviour of the typing judgments. Some basic properties of<br> this logical relation are then established, in order to prove the *fundamental lemma*, which states<br> that any derivable judgement satisfies the logical relation. Once the fundamental lemma has been proven, it entails several fundamental properties of the type<br> theory, such as the termination of the weak-head reduction strategy, the canonicity of the integers,<br> typing inversion results, etc. This first part lays the foundation necessary to the definition of an algorithmic equality relation<br> on types and terms. We can prove that this algorithmic equality is decidable, and, using the<br> fundamental lemma, that it coincides with the judgmental equality. It follows that the judgmental<br> equality of terms and types is decidable. A more detailed, but still high-level overview of the proof is provided in the companion paper. ### Files ### A more detailed description of the role of each file can be found in README.agda ### Dependencies ### This project is written in Agda. It has been tested to be working with Agda version 2.6.3. ### Warning ### The reader who wishes to type-check the entire proof should be warned that the files<br> Defintion/LogicalRelations/Substitution/Introductions/Cast.agda and Conversion/Decidable.agda may<br> be quite resource-intensive (Type-checking the latter seems to take at least 10 min on a<br> higher-end laptop).<br>