fredefox
/
cat
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Small changes

This commit is contained in:
Frederik Hanghøj Iversen 2018-05-16 11:36:26 +02:00
parent 4073d70189
commit 1c0b0d9db2
1 changed files with 9 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
doc/introduction.tex
View File

@ -22,20 +22,21 @@ propositional equality at play for a simple example.\TODO{How to
For propositional equality the decidability requirement is relaxed. It
is not in general possible to decide the correctness of logical
propositions (cf. Hilbert's \nomen{entscheidigungsproblem}).
propositions (cf.\ Hilbert's \emph{entscheidigungsproblem}).
Propositional equality are provided by the developer. When introducing
definitions this report will use the notation $\defeq$. Judgmental
equalities written $=$. For propositional equalities the notation
$\equiv$ is used.
The usual notion of propositional equality in \nomen{Intensional Type
Theory} (ITT) is quite restrictive. In the next section a few
The usual notion of propositional equality in \nomenindex{Intensional
Type Theory} (ITT) is quite restrictive. In the next section a few
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. What
makes this extension particularly interesting is that it gives a
\emph{constructive} interpretation of univalence.
\emph{constructive} interpretation of univalence. What this means will
be elaborated in the following sections.
%
\section{Motivating examples}
%
@ -176,9 +177,9 @@ implementations of category theory in Agda:
A formalization in Coq in the homotopic setting:
\url{https://github.com/HoTT/HoTT/tree/master/theories/Categories}
\item
A formalization in CubicalTT - a language designed for cubical type theory.
Formalizes many different things, but only a few concepts from category
theory:
A formalization in \emph{CubicalTT} -- a language designed for
cubical type theory. Formalizes many different things, but only a
few concepts from category theory:
\url{https://github.com/mortberg/cubicaltt}
\end{itemize}
%
@ -206,7 +207,7 @@ and an equivalence relation $\sim\ \tp X \to X \to \MCU$ on that type.
Under the setoid interpretation the equivalence relation serve as a
sort of ``local'' propositional equality. Since the developer gets to
pick this relation it is not guaranteed to be a congruence relation
apriori. So this must be verified manually by the developer.
a priori. So this must be verified manually by the developer.
Furthermore, functions between different setoids must be shown to be
setoid homomorphism, that is; they preserve the relation.