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

% http://www.logica-universalis.org/wld3-rio-de-janeiro
% https://www.mariamartinezordaz.com/uploads/1/2/4/3/124357943/[cveng]maor2020.pdf

% «.defs»		(to "defs")
% «.title-page»		(to "title-page")
% «.discrete-bmos»	(to "discrete-bmos")
% «.non-tautologies-1»	(to "non-tautologies-1")
% «.non-tautologies-2»	(to "non-tautologies-2")
% «.non-tautologies-3»	(to "non-tautologies-3")
% «.calculating»	(to "calculating")
% «.set-comprehensions»	(to "set-comprehensions")
% «.links-to-fav»	(to "links-to-fav")
% «.links-about-core»	(to "links-about-core")

\documentclass[oneside]{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")
\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
\usepackage[backend=biber,
   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
            %total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            %a4paper,
            top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
           ]{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

% «defs»  (to ".defs")
% (find-LATEX "edrx15.sty" "colors-2019")
\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}

\def\True {\mathbf{T}}
\def\V    {\mathbf{T}}
\def\False{\mathbf{F}}
\def\F    {\mathbf{F}}

\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uC#1{\und{#1}{context}}

\def\picturedotsa(#1,#2)(#3,#4)#5{%
  \vcenter{\hbox{%
  \beginpicture(#1,#2)(#3,#4)%
  \pictaxes%
  \pictdots{#5}%
  \end{picture}%
  }}%
}

\noedrxfooter % (find-LATEX "edrxheadfoot.tex")

\setlength{\parindent}{0em}

%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page»  (to ".title-page")
% (lod21p 1 "title-page")
% (lod21    "title-page")
% (excp 1 "title-page")
% (exc     "title-page")
% (ecop 1 "title-page")
% (eco    "title-page")

\thispagestyle{empty} % (find-es "tex" "thispagestyle")

\begin{center}

\begin{tabular}{c}
{\Large {\bf The Logic for Children Project}} \\[1pt]
{\Large {\bf (is trying to translate its}} \\[1pt]
{\Large {\bf categorical diagrams}} \\[1pt]
{\Large {\bf to Type Theory)}} \\[1pt]
\ColorGray{(talk @ Logic Day 2021)}
\end{tabular}

\bsk

\begin{tabular}[c]{r}
  By: \\
  Eduardo Ochs $→$ \\
  \ColorGray{(original author)} \\
  \\
  Selana Ochs $→$ \\
  \ColorGray{(recent contributor)} \\
\end{tabular}
  \!\!\!\!\!\!\!
\begin{tabular}[c]{c}
  % $\includegraphics[height=85pt]{2019emacsconf-eu-e-selana.jpg}$
  $\includegraphics[height=85pt]{2021logicday-selana2.jpg}$
\end{tabular}

% \msk
% \url{http://angg.twu.net/\#eev}

\end{center}

\newpage

Note: this presentation is a kind of

mini-rehearsal for a longer presentation titled

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

that I submitted to the

``Encontro Brasileiro em Teoria das Categorias''.

For more information on it, see:

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





\newpage


{\bf Logic for Children / Categories for Children}

\ssk

Here I will refer a lot to:

\begin{enumerate}

\item \cite{PH1}: ``Planar Heyting Algebras for Children'' (E. Ochs,
  SAJL, 2019). From its abstract:

  \begin{quote}

    In a wider context these ZHAs are interesting because toposes of
    the form $\Set^{(P,A)}$ are one of the basic tools for doing
    ``Topos Theory for Children'', in the following sense. We can {\sl
      define} ``children'' as people who think mathematically in a
    certain way --- as {\sl people who prefer to start from particular
      cases and finite examples that can be drawn explicitly,
      \ColorRed{and only then generalize}} --- and we can define a
    method for working on a particular case (less abstract, ``for
    children'') and on a general case (``for adults'') in parallel,
    using \ColorRed{parallel diagrams with similar shapes; we have
      some ways of transfering knowledge from the general case to the
      particular case, {\sl and back}. This method is sketched in the
      introduction.}

  \end{quote}

\item \cite{FavC}: ``On my favorite conventions for drawing the
  missing diagrams in Category Theory''. Published on Arxiv in 2020...
  \ColorRed{unpublishable?} From its abstract:

  \begin{quote}

    People in CT usually only share their ways of visualizing things
    when their diagrams cross some threshold of mathematical
    relevance --- and this usually happens when they \ColorRed{prove
      new theorems} with their diagrams, or when they can show that
    their diagrams can translate calculations that used to be huge
    into things that are much easier to visualize. \ColorRed{The
      diagrammatic language that I present here lies below that
      threshold --- and so it is a ``private'' diagrammatic language,
      that I am making public as an attempt to establish a dialogue
      with other people who have also created their own private
      diagrammatic languages.}

  \end{quote}

\newpage

\item \cite{CWM2}: Mac Lane's ``Categories for the Working
  Mathematician''. \ColorRed{The} standard text on CT. Very hard to
  read --- should have 100 times more diagrams that it has, but they
  are left to the reader. ``Normal'' people start from a state in
  which CWM is impossible, then they switch to a state in which CWM is
  \ColorRed{obvious}. I got stuck studying it in many. many, many
  times. One of the main themes of \cite{FavC} is formalizing
  ``notions of obviousness'', and it ends with:

  \begin{quote}

    I am especially interested in how people write when they turn
    their level-of-detail knob to a very high position.

  \end{quote}


\newpage

\item Proof assistants based of Type Theory. From the introduction of
  \cite{HOTT}:

  \begin{quote}

    Type theory (...) Although it is not generally regarded as the
    foundation for classical mathematics, set theory being more
    customary, type theory still has numerous applications, especially
    in computer science and the theory of programming languages (...)
    This is the basis of the system that we consider here; it was
    originally intended as a rigorous framework for the formalization
    of constructive mathematics.

  \end{quote}

\newpage

\item Haskell. From its Wikipedia page:

  \begin{quote}

    At the conference on Functional Programming Languages and Computer
    Architecture (FPCA '87) in Portland, Oregon, there was a strong
    consensus that a committee be formed to define an open standard
    for such languages. The committee's purpose was to consolidate
    existing functional languages into a common one to serve as a
    basis for future research in functional-language design.

  \end{quote}

  Haskell is based on a Type Theory that is simpler than the one in
  HOTT, and many universities in Europe teach Haskell to first-year
  students... so there is a lot of very readable material on it.


\item Idris: essentially Haskell plus \ColorRed{dependent types} and
  other bells and whistles. Its type system is close enough to the one
  in HOTT (from my beginner's point of view). Idris can be used as a
  proof assistant, and the authors of \cite{IdrisCT2019} have
  formalized some CT in Idris.


\item Discrete Mathematics. I taught DM for years, and a good part of
  my students entered the university without knowing how to use
  variables, and without knowing what is a theorem.

  Their difficulties with learning new levels of abstraction were very
  similar to my difficulties trying to learn Category Theory and Type
  Theory.

  I also gave some seminar courses whose pre-requisites were only
  Discrete Mathematics (or not even that). I only found the right
  approach for writing \cite{PH1} after these seminars --- they were
  on $λ$-calculus, Heyting Algebras, S4, and Intuitionistic Logic
  ``for children'', using finite examples everywhere...

% «non-tautologies-1»  (to ".non-tautologies-1")

%L kite  = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L W     = "1.2.3|.4.5."
%L guill = ".1.2|3.4.|.5.6"
%L hex   = ".1.2.|3.4.5|.6.7."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagKite",  meta="t", scale="4pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagW",     meta="s", scale="4pt"}, z):zfunction(W):output()
%L mp = MixedPicture.new({def="dagGuill", meta="s", scale="4pt"}, z):zfunction(guill):output()
%L mp = MixedPicture.new({def="dagHex",   meta="s", scale="4pt"}, z):zfunction(hex):output()
\pu

% (ph1p 10 "prop-calc")
% (ph1     "prop-calc")
% (ph1p 11 "prop-calc" "{\\sl not} a tautology")
% (ph1     "prop-calc" "{\\sl not} a tautology")

\def\und#1#2{\underbrace{#1}_{#2}}

$(P∨Q)→(P∧Q)$ is not a tautology:
%
$$\und{\und{\und{P}0 ∨ \und{Q}1}{1} → \und{\und{P}0 ∧\und{Q}1}{0}}{0}$$



\newpage

% «non-tautologies-2»  (to ".non-tautologies-2")

% (ph1p 11 "prop-calc-ZHA")
% (ph1     "prop-calc-ZHA")
% (ph1p 12 "prop-calc-ZHA" "not tautologies in this ZHA")
% (ph1     "prop-calc-ZHA" "not tautologies in this ZHA")

%R local znotnotP =
%R 1/ T   \
%R  |  .  |
%R  | . c |
%R  |b . a|
%R  | P . |
%R  \  F  /
%R local T = {F="⊥", T="⊤", a="P'", b="P''", c="→"}
%R znotnotP:tozmp({def="znotnotP", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R local zdemorgan =
%R 1/ T   \
%R  |  o  |
%R  | . . |
%R  |q . p|
%R  | P Q |
%R  \  a  /
%R local T = {F="⊥", T="⊤", p="P'", q="Q'", a="∧", o="∨"}
%R zdemorgan:tozmp({def="zdemorgan", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R zdemorgan:tozmp({def="ohouse",    scale="12pt", meta=nil}):addlrs():output()
%
%UB (¬ ¬ P) → P
%UB     --   --
%UB     10   10
%UB    ---
%UB    02
%UB  -----
%UB   20
%UB ----------- 
%UB       12
%L
%L defub "notnotP"
%
%UB ¬(P ∧ Q) → (¬ P ∨ ¬ Q)
%UB   -- --      --    --
%UB   10 01      10    01
%UB   -----     ---   ---
%UB     00      02    20
%UB -------     ---------
%UB    32          22
%UB ----------------------
%UB          22
%L
%L defub "demorgan"
%

Two classical tautologies that are not

intuitionistic tautologies:

$\pu
 \hspace{-0.5cm}
 \scalebox{0.75}{$
  \begin{array}{ccccl}
  \ohouse && \znotnotP  && \mat{\ub{notnotP}} \\ \\
          && \zdemorgan && \mat{\ub{demorgan}} \\
  \end{array}
 $}
$


\newpage

% «non-tautologies-3»  (to ".non-tautologies-3")

The connection with S4 and (order) topologies

% (ph1p 32 "topologies-as-HAs")
% (ph1     "topologies-as-HAs")
% (ph1p 33 "topologies-as-HAs" "``topological'' way")
% (ph1     "topologies-as-HAs" "``topological'' way")

\msk

%UB (¬ ¬ P) → P
%UB     --   --
%UB     10   10
%UB    ---
%UB    02
%UB  -----
%UB   20
%UB ----------- 
%UB       12
%L
%L defub "ntntP -> P"
%
%UB (¬ ¬    P  ) →    P
%UB     -------    -------
%UB     \h00010    \h00010
%UB    --------
%UB    \h00101
%UB  ---------
%UB   \h01010
%UB ----------------------
%UB      \h00111
%L
%L defub "ntntP -> P : houses"
%L
$\pu
  \ub{ntntP -> P}
  \qquad
  \qquad
  \def\h{\dagHouse}
      \ub{ntntP -> P : houses}
$


\end{enumerate}






% (favp 2 "missing-diagrams")
% (fav    "missing-diagrams")




\newpage

% «discrete-bmos»  (to ".discrete-bmos")
% (lod21p 12 "discrete-bmos")
% (lod21     "discrete-bmos")

{\bf A trick for teaching Discrete Mathematics}

\ssk

$\bbA$ is our set of \ColorRed{atoms:}

the integers plus $\True$ and $\False$ (and later also ascii strings)

\msk

$\bbB$ is our set of basic mathematical objects:

$\bbB$ contains $\bbA$, and is closed by

forming \ColorRed{finite} sets and by forming \ColorRed{finite} lists

(a \ColorRed{finite} number of times)

\msk

In the first part of the course all objects that we \ColorRed{build}

are elements of $\bbB$. We use $\N$, $\Z$, $\Q$ and $\R$ sometimes,

but expressions like $\N×\N$ and $a∈\N.a^2≥a$ only appear

in the second part of the course.

\msk

\ColorRed{Why?}

\newpage



% «calculating»  (to ".calculating")
% (lod21p 13 "calculating")
% (lod21     "calculating")

% (lodp 4 "dm-layers" "Calculating")
% (lod    "dm-layers" "Calculating")
% (lodp 5 "dm-layer-1" "Calculating")
% (lod    "dm-layer-1" "Calculating")

{\bf Layer 1: Calculating things}

...in a system with numbers, truth-values, sets and lists

where everything can be calculated in a \ColorRed{finite} number

of steps with almost no creativity required.

Example:

$%\antitabular
 \begin{array}{rcl}
  (∀a∈\{2,3,5\}.a^2<10) &=& (a^2<10)[a:=2] \;∧ \\&&
                            (a^2<10)[a:=3] \;∧ \\&&
                            (a^2<10)[a:=5] \\
                        &=& (2^2<10) ∧
                            (3^2<10) ∧
                            (4^2<10) \\
                        &=& (4<10) ∧
                            (9<10) ∧
                            (16<10) \\
                        &=& \V ∧ \V ∧ \F \\
                        &=& \F \\
  \end{array}
$

Note the substituion operator:

$(a^2<10)[a:=3] = (3^2<10)$.

\newpage

%   ____                               _                    _                 
%  / ___|___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __  ___ 
% | |   / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \/ __|
% | |__| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | \__ \
%  \____\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|___/
%                      |_|                                                    
%
% «set-comprehensions»  (to ".set-comprehensions")
% (lod21p 14 "set-comprehensions")
% (lod21     "set-comprehensions")
% (lodp 6 "set-comprehensions")
% (lod    "set-comprehensions")

{\bf Layer 1: Set Comprehensions}

I wrote a lengthy explanation of set comprehensions,

using ``generators'', ``filters'' and a ``result expression''.

The students started by learning how to calculate things

like these (note the `;' instead of a `$|$'; these `$\{\ldots;\ldots\}$'s

are calculated from left to right!):

\unitlength=5pt \def\closeddot{\circle*{0.4}}
\unitlength=5pt \def\closeddot{\circle*{0.2}}

$$\begin{array}{lll}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\{\ug{a∈\{1,2\}},
  \ug{b∈\{2,3\}},
  \uf{a≠b}; \ue{(a,b)}\} \\[10pt]
 = \;\; \{(1,2),(1,3),(2,3)\} \\[5pt]
 = \;\; \picturedotsa(0,0)(3,4){ 1,2 1,3 2,3 } \\
\end{array}
$$

...then $\setofst{a∈\{2,3,4\}}{a^2<10}$

and $\setofst{10a+b}{a∈\{1,2\},b∈\{3,4\}}$.



\newpage

In the rest of the talk I will use diagrams from...

\msk

\cite{IDARCT}:

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

\url{http://angg.twu.net/LATEX/idarct-preprint.pdf}

\msk

\cite{PH1}:

\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}

\url{http://angg.twu.net/LATEX/2017planar-has-1.pdf}

\msk

\cite{FavC}:

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

\url{http://angg.twu.net/LATEX/2020favorite-conventions.pdf}



\newpage


% «links-to-fav»  (to ".links-to-fav")
% (favp  2 "toc")
% (fav     "toc")
% (favp  8 "the-conventions")
% (fav     "the-conventions")
% (favp 11 "to-deserve-a-name")
% (fav     "to-deserve-a-name")
% (favp 11 "to-deserve-a-name" "term inference")
% (fav     "to-deserve-a-name" "term inference")
% (favp 14 "freyd")
% (fav     "freyd")
% (favp 16 "freyd-with-functors")
% (fav     "freyd-with-functors")
% (favp 16 "freyd-with-functors" "universalness")
% (fav     "freyd-with-functors" "universalness")
% (favp 19 "internal-views")
% (fav     "internal-views")
% (favp 19 "reductions")
% (fav     "reductions")
% (favp 24 "internal-view-adjunction")
% (fav     "internal-view-adjunction")
% (favp 29 "basic-example-as-skel")
% (fav     "basic-example-as-skel")
% (favp 29 "basic-example-full")
% (fav     "basic-example-full")


% «links-about-core»  (to ".links-about-core")
% (find-books "__comp/__comp.el" "marlow-peyton-jones")
% (find-books "__logic/__logic.el" "altenkirch-dtwos" "sugar")
% (find-bradytddpage (+ 26 83) "3.4.2   Bound and unbound implicits")
% (find-bradytddtext (+ 26 83) "3.4.2   Bound and unbound implicits")

% https://dl.acm.org/doi/10.1145/1190315.1190324
% (find-pdf-page "~/books/System_F_with_type_equality_coercions.pdf")
% (find-pdf-text "~/books/System_F_with_type_equality_coercions.pdf")

% Rings
% 
% Abuses of language




\cite{HOTT}
\cite{HaskellCore}
\cite{Kamareddine}
\cite{Sommaruga}

% (find-books "__logic/__logic.el" "hott")

\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=2021logicday veryclean
make -f 2019.mk STEM=2021logicday pdf

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