Skip to content
Browse files

tiny modif

  • Loading branch information...
1 parent 3401d83 commit de09a74fa3e75efab2e24d2a56031cbe634f7fef Thomas Anberree committed Dec 13, 2011
Showing with 1 addition and 1 deletion.
  1. BIN defquotients.pdf
  2. +1 −1 defquotients.tex
View
BIN defquotients.pdf
Binary file not shown.
View
2 defquotients.tex
@@ -257,7 +257,7 @@ \subsection{Type theory basics}
declaration of implicitly quantified arguments, assuming that the
human reader, unlike a machine, can reconstruct those. Given elements $b : B\,a$ and $b' : B\,a'$ with a proof $p : a = a'$,
we write $b \simeq_{p} b'$ for the \emph{heterogeneous equality} $\subst\,B\,p\,b \equiv b'$. Most of
-our examples do not require functional extensionality, but if we do assume that it is present in form of an \amend[uninterpreted]{\todo{postulated}} constant $\Ext : (\forall(x : A) \to f\,x = g\,x) \to f = g$,
+our examples do not require functional extensionality, but if we do assume that it is present in form of \amend[an uninterpreted]{a postulated} constant $\Ext : (\forall(x : A) \to f\,x = g\,x) \to f = g$,
which is justified by Hofmann's observation that extensional type
theory is a conservative extension of the theory considered in the present paper~\cite{hofmann1995thesis}. Alternatively, we can eliminate $\Ext$ as suggested in
\cite{alti:lics99}.

0 comments on commit de09a74

Please sign in to comment.
Something went wrong with that request. Please try again.