From 4073d70189d5de12ab63612a91edb1d44c0b3269 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 16 May 2018 11:03:34 +0200 Subject: [PATCH] Add note about constructive intepretation of univalence --- doc/introduction.tex | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/introduction.tex b/doc/introduction.tex index 2441614..2c41469 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -33,7 +33,9 @@ The usual notion of propositional equality in \nomen{Intensional Type motivating examples will highlight this. There exist techniques to circumvent these problems, as we shall see. This thesis will explore an extension to Agda that redefines the notion of propositional -equality and as such is an alternative to these other techniques. +equality and as such is an alternative to these other techniques. What +makes this extension particularly interesting is that it gives a +\emph{constructive} interpretation of univalence. % \section{Motivating examples} %