% (find-angg "LATEX/2017vichy-abs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017vichy-abs.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017vichy-abs.pdf"))
% (defun e () (interactive) (find-LATEX "2017vichy-abs.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017vichy-abs"))
% (find-xpdfpage "~/LATEX/2017vichy-abs.pdf")
% (find-sh0 "cp -v  ~/LATEX/2017vichy-abs.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2017vichy-abs.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2017vichy-abs.pdf
%               file:///tmp/2017vichy-abs.pdf
%           file:///tmp/pen/2017vichy-abs.pdf
% http://angg.twu.net/LATEX/2017vichy-abs.pdf
%
% (find-sh0 "cp -v  ~/LATEX/2017vichy-abs.pdf /tmp/tutorial-cats.pdf")
% (find-sh0 "cp -v  ~/LATEX/2017vichy-abs.tex /tmp/tutorial-cats.tex")
% (find-sh "cd /tmp/ && lualatex tutorial-cats.tex")
% (find-xpdfpage "/tmp/tutorial-cats.pdf")
% (find-fline    "/tmp/tutorial-cats.tex")

%\documentclass[oneside]{book}
%\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
%\usepackage{amsmath}
%\usepackage{amsfonts}
%\usepackage{amssymb}
%\usepackage{pict2e}
%\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
%\usepackage{colorweb}             % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
%\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
%\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
%\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
%\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
%\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
%\begin{document}

% \catcode`\^^J=10
% \directlua{dednat6dir = "dednat6/"}
% \directlua{dofile(dednat6dir.."dednat6.lua")}
% \directlua{texfile(tex.jobname)}
% \directlua{verbose()}
% %\directlua{output(preamble1)}
% \def\expr#1{\directlua{output(tostring(#1))}}
% \def\eval#1{\directlua{#1}}
% \def\pu{\directlua{pu()}}
% 
% \directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
% \directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
% %L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end

\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref}
\begin{document}
\def\Set{\mathbf{Set}}
\catcode`×=13 \def×{\times}
\catcode`β=13 \defβ{\beta}
\catcode`λ=13 \defλ{\lambda}

{\bf An Introduction to Categorical Semantics (``For Children'')}

\medskip

One great way to make the expression ``for children'' precise in
mathematical titles is to {\sl define} ``children'' as ``people
without mathematical maturity'', in the sense that they are not able
to understand structures that are too abstract straight away --- they
need particular cases first.

% On children:
% (find-xpdfpage "~/LATEX/2015children.pdf")
% (ebsp 1 "title")

Consider these four basic theorems of Categorical Semantics: 1) the
categorical models for Intuitionistic Propositional Calculus are the
Heyting Algebras (HAs); 2) the categorical models for the simply-typed
$\lambda$-calculus with products are the Cartesian Closed Categories
(CCCs); 3) HAs are CCCs with one extra condition, namely that each
hom-set has at most one element; 4) $\Set$ is a CCC. Let's refer to
them as ``1--4''.

Theorems 1--4 involve lots of definitions and this makes them quite
hard to understand when they are proved in the usual way --- ``for
adults'' --- in which the most general case is done first.

The first part of this minicourse will be centered on proving 1--4
``for children''. We will see how to interpret on sets the
lambda-notation with types, and use that to formalize a common trick
in Category Theory that is seldom explained: the trick of the ``the''.
In an expression like ``We write $(A×)$ for {\sl the} functor that
takes each set $B$ to $A×B$'' the action of this functor on sets,
$(A×)_0$, is told explicitly, but the action of $(A×)$ on morphisms,
$(A×)_1$, is left for the reader to discover; we know that if $\beta:B
\to B'$ then $(A×)_1(\beta):A×B \to A×B'$ --- we know the {\sl type}
of the operation $(A×)_1$, and what we have to do is to find a
$\lambda$-term with that type and then check that it respects the
naturality conditions. Some of the techniques we will use, like
liftings and parallel diagrams, are sketched in [1].

% On corry-Howard:
% (ebsp 14 "the-big-picture")
% (laop 7 "C-H-diagram")
% (lao    "C-H-diagram")
% (find-angg ".emacs" "unilog-current")

% The trick of the "the":
% (find-idarctpage 3 "proof\nsearch")
% (find-idarcttext 3 "proof\nsearch")
% (lamp171 5 "types")
% (lam171    "types")
% (lamp171 15 "algebraic-structures")
% (lam171     "algebraic-structures")
% (laqe171)
% (laq171  9 "20170418" "ND: provando certas coisas vindas de diagramas; regras")
% (laq171 15 "20170502" "Categrias")

The second part of the minicourse will be on some less obvious HAs and
CCCs: the planar HAs of [2] and categories of the form $\Set^D$, where
$D$ is a directed graph.

% (laq171 11 "20170425" "Lógica em ZHAs")
% (ebsp 11 "non-tautologies")
% (ebs     "non-tautologies")

The third part will be on elementary toposes. An elementary topos is
formally just a CCC with pullbacks and a classifier object, but just
as we can interpret $\lambda$-calculus on a CCC we can interpret
``Local Set Theory'' (``LST'') in a topos. LST has lots of operations
and rules, and most of them can be understood easily if we look at
what they ``mean'' in $\Set$ and in categories of the form $\Set^D$,
and we choose the right particular cases.

The fourth and last part of the minicourse will be on tricks for
understanding both the type-theoretical language and the categorical
structures used in [3], again using specialization to particular cases
where everything is easy to draw explicitly.

% (find-books "__cats/__cats.el" "jacobs")
% (find-books "__cats/__cats.el" "jacobs" "4_  First order predicate logic")
% (find-books "__cats/__cats.el" "maclane")
% (find-books "__cats/__cats.el" "maclane" "IV. Adjoints")
% (find-books "__cats/__cats.el" "awodey")
% (find-books "__cats/__cats.el" "awodey" "6.5 lambda-calculus")



\bigskip

[1]: Ochs, Eduardo: {\sl Internal Diagrams and Archetypal Reasoning in
  Category Theory}. Logica Universalis, 2013.

[2]: Ochs, Eduardo: {\sl Intuitionistic Logic for Children, or: Planar
  Heyting Algebras for Children}. Preprint, 2017.

[3]: Jacobs, Bart: {\sl Categorical Logic and Type Theory}. North-Holland, 1999.



\medskip

Eduardo Ochs --- UFF

eduardoochs@gmail.com

Home page: \url{http://angg.twu.net/math-b.html}

\medskip

(Version: 2017fev21)

\end{document}

% (find-angg ".emacs" "idarct")
% (find-idarctpage 24 "17. Cartesian Closed Categories")


% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: