\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{propositions as types}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{constructivism_realizability_computability}{}\paragraph*{{Constructivism, Realizability, Computability}}\label{constructivism_realizability_computability}

[[!include constructivism - contents]]

\hypertarget{category_theory}{}\paragraph*{{$(0,1)$-Category theory}}\label{category_theory}

[[!include (0,1)-category theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{general_idea}{General idea}\dotfill \pageref*{general_idea} \linebreak
\noindent\hyperlink{PropositionsAsSomeTypes}{Propositions as some types}\dotfill \pageref*{PropositionsAsSomeTypes} \linebreak
\noindent\hyperlink{in_homotopy_type_theory}{In homotopy type theory}\dotfill \pageref*{in_homotopy_type_theory} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{ReferencesHistory}{History}\dotfill \pageref*{ReferencesHistory} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\hypertarget{general_idea}{}\subsubsection*{{General idea}}\label{general_idea}

In [[type theory]], the paradigm of \textbf{propositions as types} says that [[propositions]] and [[types]] are essentially the same. A proposition is identified with the type (collection) of all its [[proofs]], and a type is identified with the proposition that it has a [[term]] (so that each of its terms is in turn a proof of the corresponding proposition).

\begin{quote}%
\ldots{} to show that a proposition is true in type theory corresponds to exhibiting an element $[$ [[term]] $]$ of the type corresponding to that proposition. We regard the elements of this type as \emph{evidence} or \emph{witnesses} that the proposition is true. (They are sometimes even called \emph{proofs}\ldots{} (from [[Homotopy Type Theory -- Univalent Foundations of Mathematics]], section 1.11)


\end{quote}
Not all type theories follow this paradigm; among those that do, [[Martin-Löf type theories]] are the most famous. In its variant as [[homotopy type theory]] the paradigm is also central, but receives some refinements, see at \emph{\hyperlink{PropositionsAsSomeTypes}{Propositions as some types}}

Even when the paradigm is not adopted, however, there is still a close relationship between logical and type-theoretic operations, called the \textbf{Curry--Howard isomorphism} or (if it is not clear in which category this [[isomorphism]] is supposed to exist) the \textbf{Curry--Howard correspondence}. Or maybe better (\hyperlink{Harper}{Harper}) the \textbf{[[Brouwer-Heyting-Kolmogorov interpretation]]}. This correspondence is most precise and well-developed for [[intuitionistic logic]].

Accordingly, [[logic|logical]] operations on propositions have immediate analogs on [[types]]. For instance logical \emph{[[and]]} corresponds to forming the [[product type]] $A \times B$ (a [[proof]] of $A$ and a proof of $B$), the [[universal quantifier]] corresponds to [[dependent product]], the [[existential quantifier]] to [[dependent sum]].

\hypertarget{PropositionsAsSomeTypes}{}\subsubsection*{{Propositions as some types}}\label{PropositionsAsSomeTypes}

A related paradigm may be called \textbf{propositions as some types}, in which propositions are identified with particular types, but not all types are regarded as propositions. Generally, the propositions are the ``types with at most one [[term]]''. This is the paradigm usually used in the [[internal logic]] of [[categories]] such as [[toposes]], as well as in [[homotopy type theory]]. In this case, the type-theoretic operations on types either restrict to the propositions to give logical operations (for [[conjunction]], [[implication]], and the [[universal quantifier]]), or have to be ``reflected'' therein (for [[disjunction]] and the [[existential quantifier]]). The reflector operation is called a [[bracket type]].

\hypertarget{in_homotopy_type_theory}{}\subsubsection*{{In homotopy type theory}}\label{in_homotopy_type_theory}

We consider aspects of the interpretation of \emph{propositions as types} in [[homotopy type theory]], see (\hyperlink{HoTTBook}{HoTT book, section 1.11}).

In [[homotopy type theory]] where types may be thought of as [[homotopy types]] ([[∞-groupoids]]) (or rather [[geometric homotopy types]] ([[∞-stacks]],[[(∞,1)-sheaves]]), more generally), we may think for $A$ any type of

\begin{itemize}%
\item the [[objects]] of $A$ are [[proofs]] of some proposition;


\item the [[morphisms]] of $A$ are equivalences between these proofs;


\item the [[2-morphisms]] of $A$ are equivalences between these equivalences, and so on.



\end{itemize}
So in terms of the notion of [[n-connected object of an (infinity,1)-topos|n-connected]] and [[truncated|n-truncated objects in an (∞,1)-category]] we have

\begin{itemize}%
\item if $A$ is [[(-1)-connected]] then the corresponding proposition is [[true]];


\item if $A$ is [[(-2)-truncated]] (a [[(-2)-groupoid]]) then the corresponding proposition is true by a unique proof which is uniquely equivalent to itself, etc.;


\item if $A$ is [[(-1)-truncated]] (a [[(-1)-groupoid]]) then the corresponding proposition may be true or [[false]], but if it is true it is to by a unique proof as above;


\item if $A$ is [[0-truncated]] then there may be more than one proof, but none equivalent to itself in an interesting way;


\item if $A$ is [[1-truncated]] then there may be proofs of the corresponding proposition that are equivalent to themselves in interesting ways.



\end{itemize}
We would not say homotopy type theory has propositions as types in the same way that Martin--L\"o{}f type theory has; only the $(-1)$-truncated types are propositions as such. That is, in HoTT we have propositions as \emph{some} types. In this case the [[bracket types]] can be identified with a particular [[higher inductive type]] called $isInhab$.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[proof relevance]]


\item [[computational trinitarianism]]


\item [[theory]]


\item [[proposition]]/[[type]] (\textbf{propositions as types})


\item [[definition]]/[[proof]]/[[program]] ([[proofs as programs]])


\item [[theorem]], [[axiom]]


\item [[propositions as projections]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\hypertarget{general}{}\subsubsection*{{General}}\label{general}

A standard account for [[intuitionistic type theory]] is

\begin{itemize}%
\item [[Per Martin-Löf]], \emph{Intuitionistic Type Theory}, Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Napoli, 1984.

\end{itemize}
Discussion in [[homotopy type theory]] is in section 1.11 of

\begin{itemize}%
\item [[UF-IAS-2012|Univalent Foundations Project]], \emph{[[Homotopy Type Theory -- Univalent Foundations of Mathematics]]} (\textbf{\href{http://homotopytypetheory.org/book/}{web}}, \textbf{\href{http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf}{pdf}}, \textbf{[[Planet Math|PM]] \href{http://planetmath.org/node/87534}{wiki version}})

\end{itemize}
Exposition is in

\begin{itemize}%
\item [[Robert Harper]], \emph{Extensionality, Intensionality, and Brouwer's Dictum} (\href{http://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/}{blog})

\end{itemize}
\hypertarget{ReferencesHistory}{}\subsubsection*{{History}}\label{ReferencesHistory}

An influential original article was

\begin{itemize}%
\item [[William Howard]], \emph{The formulae-as-types notion of construction}. In J. Roger Seldin, Jonathan P.; Hindley, (ed.s), \emph{To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, pages 479--490. Academic Press, 1980. original paper manuscript from 1969. (Cited on pages 53, 54, 100, and 430.) (\href{http://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}{pdf})

\end{itemize}
The origins of this manuscript and its publication are recounted in a 2014 email from Howard to Philip Wadler:

\begin{itemize}%
\item [[William Howard]], \href{http://wadler.blogspot.fr/2014/08/howard-on-curry-howard.html}{email}.

\end{itemize}
This influential note brought [[Dana Scott]] to write ``Constructive Validity'' (a precursor of type theory) and also strongly influenced [[Per Martin-Löf]]. Independently and at about the same time, the idea was also found by [[N.G. de Bruijn]] for the [[Automath]] system.

[[Dana Scott]], [[William Howard]], [[Per Martin-Löf]], and [[William Tait]] were all involved in the late 60s and early 70s, mainly in Chicago.

\begin{itemize}%
\item [[William Tait]], \emph{The completeness of intuitionistic first-order logic}. Unpublished manuscript.

\end{itemize}
Also [[William Lawvere]] was there, lecturing on [[hyperdoctrines]]. Lawvere told [[Steve Awodey]] that the basic example of a morphism of hyperdoctrines from the proof-relevant one to the proof-irrelevant one was influenced by Kreisel, not Howard, who attended Lawvere's Chicago lectures in the 60s. See pages 2 and 3 of

\begin{itemize}%
\item [[William Lawvere]] interviewed by Felice Cardone, \emph{The role of Cartesian closed categories in foundations}, March 2000 (\href{https://dl.dropboxusercontent.com/u/92056191/Archive/temporary_new_material/lawvere-cardone-2000/lawvere-cardone-2000.pdf}{link})

\end{itemize}
But the story started earlier with what has been called the [[Brouwer-Heyting-Kolmogorov interpretation]] of [[intuitionistic logic]], highlighted for instance in (\hyperlink{Troelstra91}{Troelstra 91}), which identifies a proposition with the collection of its proofs. This view goes back to an observation of Kolmogorov that the formalisation of Brouwer's ideas by Heyting in 1930 can be semantically interpreted as a calculus of `Aufgaben' - problems (and solutions), reported in

\begin{itemize}%
\item [[Andrey Kolmogorov]], \emph{Zur Deutung der intuitionistischen Logik}, Math. Z. \textbf{35} (1932) pp.58-65. (\href{http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=GDZPPN002373467}{gdz})

\end{itemize}
A historical account is in the section on types in

\begin{itemize}%
\item Hindley J. Roger; Cardone Felice, \emph{History of Lambda-calculus and Combinatory Logic}. Handbook of the History of Logic. Volume 5. Logic from Russell to Church (edited by D. Gabbay and J. Woods), Elsevier, 2009, pp. 723-817 (\href{http://www.di.unito.it/~felice/pdf/lambdacomb.pdf}{pdf}, \href{http://www.di.unito.it/~felice/pdf/erratalist.pdf}{errata})

\end{itemize}
and in section 5 of

\begin{itemize}%
\item [[Anne Sjerp Troelstra]], \emph{History of Constructivism in the 20th Century}, 1991 (\href{https://www.illc.uva.nl/Research/Publications/Reports/ML-1991-05.text.pdf}{preprint})

\end{itemize}
Philip Wadler is currently in the process of writing another history \href{http://homepages.inf.ed.ac.uk/wadler/topics/history.html#propositions-as-types}{here}.

[[!redirects propositions as types]] [[!redirects propositions-as-types]] [[!redirects propositions as types in type theory]]

[[!redirects Curry-Howard correspondence]] [[!redirects Curry?Howard correspondence]] [[!redirects Curry--Howard correspondence]] [[!redirects Curry-Howard isomorphism]] [[!redirects Curry?Howard isomorphism]] [[!redirects Curry--Howard isomorphism]]



\end{document}