% (find-LATEX "2021excuse-abs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021excuse-abs.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2021excuse-abs.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2021excuse-abs.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021excuse-abs.pdf"))
% (defun e () (interactive) (find-LATEX "2021excuse-abs.tex"))
% (defun u () (interactive) (find-latex-upload-links "2021excuse-abs"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (find-pdf-page   "~/LATEX/2021excuse-abs.pdf")
% (find-sh0 "cp -v  ~/LATEX/2021excuse-abs.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2021excuse-abs.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2021excuse-abs.pdf
%               file:///tmp/2021excuse-abs.pdf
%           file:///tmp/pen/2021excuse-abs.pdf
% http://angg.twu.net/LATEX/2021excuse-abs.pdf
% (find-LATEX "2019.mk")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb}                 % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
%\usepackage{proof}   % For derivation trees ("%:" lines)
%\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
%\usepackage[backend=biber,
%   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu


{
\setlength{\parindent}{0em}

\footnotesize

This is the abstract for the talk

``Category Theory as An Excuse to Learn Type Theory''

that I ($←$ Eduardo Ochs) will present at the

``Encontro Brasileiro em Teoria das Categorias'' in 2021jan29.

For more info, see:

\url{https://encontrocategorico.mat.br/}

\url{https://encontrocategorico.mat.br/programacao/}

\url{http://angg.twu.net/math-b.html\#2021-excuse-tt}

}

\bsk
\bsk



Several years ago I tried to study Topos Theory ``seriously'' for the
first time... and I got stuck. The books explained everything in a way
that was too abstract for me, mentioning concrete examples either very
briefly or not at all, drawing only tiny a fraction of the diagrams
that seemed to be implicit in the text, and leaving all the details as
exercises for the readers. My slogan became: ``I need a version for
children of all this!''

A few years after that I found a first {\it definition} of ``for
children'' that was good enough. ``Adults'' prefer to start by
theorems that are as general as possible, and then specialize them;
``children'' prefer to start by playing with finite objects, then
develop (visual) intuitions about how they behave, and then understand
the theorems -- both in the finite cases, that are easy to visualize,
and in the general, most abstract cases. The nice thing is that we can
work in the general case, ``for adults'', and in a particular case,
``for children'', in parallel, using diagrams that have exactly the
same shape, and that can be draw side by side -- and we can transfer
knowledge from the general case, ``for adults'', to the particular
case ``for children'', {\it and back}. The paper ``Planar Heyting
Algebras for Children'' is about this; this transference of knowledge
is not totally formalized yet -- we only have a few examples now, and
we need many more to understand the patterns.

Let's consider another situation. Suppose that we want to learn
Category Theory from a book -- from Mac Lane's ``Categories for The
Working Mathematician'', for example. Before taking one of its
constructions and working on it using two parallel diagrams with the
same shape, one for the general abstract case and one for a particular
case that is more concrete, we need to be able to draw the diagram for
the construction as it appears in the book, using the same notation as
in the book if possible. The techniques for doing that will form the
core of this presentation -- we will see how to translate the language
in CWM to diagrams that can be read in a precise way, and how to
translate these diagrams to a language that is close enough to the
language that is used by proofs assistants based on type theories with
dependent types. We will also see a ``Type Theory for Children'', in
which the basic concepts of Type Theory are presented ``for adults''
and ``for children'' in parallel, using diagram with the same shapes;
and we will see how to translate a part of the notation to Haskell and
Idris, and to their type systems.

Most of the material in the previous paragraph comes from the
\hbox{(non?-)} paper ``On my favorite conventions for drawing the
missing diagrams in Category Theory'', available from:

\msk

\centerline{\url{http://angg.twu.net/math-b.html\#favorite-conventions}}

\msk

The presentation will be in Portuguese, but with slides in English.



%\printbibliography

\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021excuse-abs veryclean
make -f 2019.mk STEM=2021excuse-abs pdf

% Local Variables:
% coding: utf-8-unix
% ee-tla: "exca"
% End: