Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |

% (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: