% (find-angg "LATEX/2019ebl-five-appls.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019ebl-five-appls.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019ebl-five-appls.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019ebl-five-appls.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019ebl-five-appls; makeindex 2019ebl-five-appls"))
% (defun e () (interactive) (find-LATEX "2019ebl-five-appls.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019ebl-five-appls"))
% (find-xpdfpage "~/LATEX/2019ebl-five-appls.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019ebl-five-appls.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019ebl-five-appls.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019ebl-five-appls.pdf
%               file:///tmp/2019ebl-five-appls.pdf
%           file:///tmp/pen/2019ebl-five-appls.pdf
% http://angg.twu.net/LATEX/2019ebl-five-appls.pdf
%
% Upload to:

% «.colors»			(to "colors")
% «.defs»			(to "defs")
% «.title-page»			(to "title-page")
% «.category-theory»		(to "category-theory")
% «.children»			(to "children")
% «.five-applications»		(to "five-applications")
% «.finite-topologies»		(to "finite-topologies")
% «.finite-topologies-2»	(to "finite-topologies-2")
% «.finite-topologies-3»	(to "finite-topologies-3")
% «.finite-topologies-4»	(to "finite-topologies-4")
% «.famous-J-operator»		(to "famous-J-operator")
% «.strange-J-operator»		(to "strange-J-operator")
% «.logic-in-a-ZHA»		(to "logic-in-a-ZHA")
% «.logic-in-a-ZHA-2»		(to "logic-in-a-ZHA-2")
% «.logic-in-a-ZHA-3»		(to "logic-in-a-ZHA-3")
% «.J-operators»		(to "J-operators")
% «.famous-J-operator-2»	(to "famous-J-operator-2")
% «.strange-J-operator-2»	(to "strange-J-operator-2")
% «.question-marks»		(to "question-marks")
% «.question-marks-2»		(to "question-marks-2")
% «.geometric-morphisms»	(to "geometric-morphisms")
% «.geometric-morphisms-2»	(to "geometric-morphisms-2")
% «.geometric-morphisms-3»	(to "geometric-morphisms-3")
% «.a-factorization»		(to "a-factorization")
% «.a-factorization-2»		(to "a-factorization-2")
% «.a-factorization-3»		(to "a-factorization-3")
% «.a-factorization-4»		(to "a-factorization-4")
% «.shape-and-movement»		(to "shape-and-movement")

\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor}  % (find-es "tex" "xcolor")
%\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
%\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")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-LATEXfile "2016-2-GA-VR.tex" "{geometry}")
% (find-latexgeomtext "total={6.5in,8.75in},")
\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")

\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")



% «colors» (to ".colors")
% (find-angg ".emacs.papers" "xcolor")
\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorBrown #1{{\color{Brown}#1}}
\long\def\ColorBrown #1{{\color{brown}#1}}
\long\def\ColorBook  #1{{\color{brown}#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}}


% «defs» (to ".defs")
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
\def\smile{\ensuremath{{=})}}
\def\frown{\ensuremath{{=}(}}
\def\smirk{\ensuremath{{=}/}}
\def\BPM{𝐬{BPM}}
\def\bbG{{\mathbb{G}}}
\def\sh{{\mathbf{sh}}}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\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\uCH#1{\und{#1}{context / hypotheses}}
\def\uvt#1{\und{#1}{v:T}}
\def\uterm#1{\und{#1}{term}}
\def\utype#1{\und{#1}{type}}
\def\uconc#1{\und{#1}{conclusion}}

\def\Sets{\mathsf{Sets}}
\def\TALA{\mathsf{TA}_λ^→}
\def\app {\mathsf{app}}
\def\pair{\mathsf{pair}}

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

\def\myvcenter#1{\begin{matrix}#1\end{matrix}}

\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}

\setlength{\parindent}{0em}

\def\O{\mathcal{O}}
\def\T{\mathbf{T}}
\def\F{\mathbf{F}}



%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page» (to ".title-page")
% (ntyp 1 "title-page")
% (nty    "title-page")
% (find-es "tex" "huge")
% (find-LATEXfile "2019ebl-abs.tex" "Five applications")

\begin{center}

\Large 

{\bf

Five applications of the

``Logic for Children''

project to Category Theory

\large

\ssk

% \ColorGray{and to the ``Logic for Children'' project}

}

%\bsk
%
\normalsize
%
%(a part of the ``Logic for Children'' project)

\msk

Eduardo Ochs (UFF, Brazil)

\footnotesize

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

\end{center}


\newpage

\noedrxfooter


%   ____ _____ 
%  / ___|_   _|
% | |     | |  
% | |___  | |  
%  \____| |_|  
%              
% «category-theory»  (to ".category-theory")

{\bf Category Theory...}

...\ColorRed{seems} to be a very elegant area with ``the right
abstractions'' and lots of diagrams, but the diagrams are usually
omitted from the texts as if they were ``obvious exercises'', and the
motivating examples are mentioned briefly, if at all --- so the
comparisons between these ``abstractions'' and the examples are also
left as exercises.

\msk

Topos Theory is a very important sub-area of CT.

When I tried to read Johnstone's ``Topos Theory'' (1977)

I understood very little, even though I tried \ColorRed{very} hard.

\ColorRed{``I need a version for children of this!!!''}

(I.e., with the \ColorRed{missing} diagrams and the examples.)





\newpage

%   ____ _     _ _     _                
%  / ___| |__ (_) | __| |_ __ ___ _ __  
% | |   | '_ \| | |/ _` | '__/ _ \ '_ \ 
% | |___| | | | | | (_| | | |  __/ | | |
%  \____|_| |_|_|_|\__,_|_|  \___|_| |_|
%                                       
% «children»  (to ".children")

{\bf My current favorite definition of ``children'':}

They prefer to start from particular cases

and then generalize ---

They like diagrams and finite objects

drawn very explicitly ---

They become familiar with mathematical ideas

by calculating / checking several cases

(rather than by proving theorems)

\msk

% http://puzzler.sourceforge.net/docs/pentominoes.html
% http://puzzler.sourceforge.net/docs/images/ominoes/pentominoes-8x8.png

$\hskip-5.5pt
 %
 \begin{tabular}[b]{l}
   Example: pentominos. \\
   Let ``children'' \ColorRed{play} \\
   with pentominos for a while \\
   \ColorRed{before} showing to them \\
   theorems and game trees! \\
  \end{tabular}
  %
  \qquad
  \quad
  %
  \includegraphics[height=52pt]{pentominoes-8x8.png}
$

\newpage


%  _____ _                               _     
% |  ___(_)_   _____    __ _ _ __  _ __ | |___ 
% | |_  | \ \ / / _ \  / _` | '_ \| '_ \| / __|
% |  _| | |\ V /  __/ | (_| | |_) | |_) | \__ \
% |_|   |_| \_/ \___|  \__,_| .__/| .__/|_|___/
%                           |_|   |_|          
%
% «five-applications»  (to ".five-applications")

{\bf Five applications}

{%\footnotesize

\begin{enumerate}

\item A way to develop visual intuition about Intuitionistic
  Propositional Logic. Models for IPL are Heyting Algebras; topologies
  are HAs. Look for finite topologies! Use order topologies. Bonus:
  use \ColorRed{planar} topologies (``\ColorRed{ZHA}s'').

\item A way to build a topos with a given logic (when that logic is a
  ZHA). Solution: $\Set^{(P,A)}$.

\item Sheaves are related to J-operators ($←$ old terminology) on HAs.
  So: a way to visualize J-operators on ZHAs (``slashings'').

\end{enumerate}

\newpage

\begin{enumerate}

\item The sheaf associated to a J-operator. Solution:
  \ColorRed{question marks}; erasing followed by reconstruction yields
  the sheafification functor.

\item A version ``for children'' for parts of The Elephant --- in
  which the ``missing diagrams'' are no longer missing and we can
  remember theorems and constructions by \ColorRed{shape} and
  \ColorRed{movement}. Also: motivating examples ``for children'', in
  which everything is finite and can be drawn explicitly. ``Children''
  develop familiarity with mathematical structures by
  \ColorRed{calculating} rather than by \ColorRed{proving theorems}.

\end{enumerate}

}



\newpage


%  _____ _       _ _         _                  
% |  ___(_)_ __ (_) |_ ___  | |_ ___  _ __  ___ 
% | |_  | | '_ \| | __/ _ \ | __/ _ \| '_ \/ __|
% |  _| | | | | | | ||  __/ | || (_) | |_) \__ \
% |_|   |_|_| |_|_|\__\___|  \__\___/| .__/|___/
%                                    |_|        
%
% «finite-topologies»  (to ".finite-topologies")
% (eb5p 6 "finite-topologies")
% (eb5    "finite-topologies")
% (ph1p 24 "topologies-as-partial-orders")
% (ph1     "topologies-as-partial-orders")

{\bf Finite topologies}

%R local house, ohouse = 2/  #1  \, 7/       !h11111                     \
%R                        |#2  #3|   |              !h01111              |
%R                        \#4  #5/   |       !h01011       !h00111       |
%R                                   |!h01010       !h00011       !h00101|
%R                                   |       !h00010       !h00001       |
%R                                   \              !h00000              /
%R  house:tomp({def="zfHouse#1#2#3#4#5", scale="5pt",   meta="s"}):addcells():output()
%R  house:tomp({def="zdagHouseMicro", scale="6.8pt", meta="t"}):addbullets():addarrows():output()
%R  house:tomp({def="zdagHouse",      scale="20pt",  meta=nil}):addbullets():addarrows():output()
%R ohouse:tomp({def="zdagOHouse",     scale="28pt",  meta=nil}):addcells():addarrows("w"):output()
%R ohouse:tozmp({def="zdagohouse",    scale="12pt",  meta="s"}):addlrs():addarrows("w"):output()
%
%R local guill, oguill = 2/  #1  #2\, 8/                !g111111                \
%R                        |#3  #4  |   |        !g101111        !g011111        |
%R                        \  #5  #6/   |                !g001111        !g010111|
%R                                     |        !g001011        !g000111        |
%R                                     |!g001010        !g000011                |
%R                                     |        !g000010        !g000001        |
%R                                     \                !g000000                /
%R  guill:tomp({def="zfGuill#1#2#3#4#5#6", scale="3.5pt", meta="s"}):addcells():output()
%R  guill:tomp({def="zdagGuill",    scale="7pt", meta="t"}):addbullets():addarrows():output()
%R  guill:tomp({def="zdagGuill",    scale="20pt",  meta=nil}):addbullets():addarrows():output()
%R oguill:tomp({def="zdagOGuill",   scale="28pt",  meta=nil}):addcells():addarrows("w"):output()
%R oguill:tozmp({def="zdagoguill",  scale="12pt",  meta="s"}):addlrs():addarrows():output()
%
%R local w, womit, W =
%R 2/#1  #2  #3\, 2/    a     \, 7/              !w11111              \
%R  \  #4  #5  /   |  b c d   |   |       !w11011!w10111!w01111       |
%R                 |  e f g   |   |       !w10011!w01011!w00111       |
%R                 |h   i   j |   |!w10010       !w00011       !w00101|
%R                 |  k   l   |   |       !w00010       !w00001       |
%R                 \    m     /   \              !w00000              /
%R w:tomp({def="zfW#1#2#3#4#5", scale="3.5pt", meta="s"}):addcells():output()
%R w:tomp({def="zfWbig#1#2#3#4#5", scale="25pt", meta=nil}):addcells():addarrows("w"):output()
%R w:tomp({def="zdagW",  scale="20pt", meta=nil}):addbullets():addarrows() :output()
%R W:tomp({def="zdagOW", scale="28pt", meta=nil}):addcells():addarrowsexcept("w", "(2,4)0"):output()
%

\pu
$\resizebox{!}{80pt}{$
  (\Opens\left(\zdagHouse\right), ⊂_1)
  =
  \def\h{\zfHouse}\zdagOHouse
  $}
$

\newpage

% «finite-topologies-2»  (to ".finite-topologies-2")
% (eb5p 7 "finite-topologies-2")
% (eb5    "finite-topologies-2")

{\bf Finite topologies (2)}

$\resizebox{!}{80pt}{$
  (\Opens\left(\zdagGuill\right), ⊂_1)
  =
  \def\g{\zfGuill}\zdagOGuill
  $}
$

\newpage

% «finite-topologies-3»  (to ".finite-topologies-3")
% (eb5p 8 "finite-topologies-3")
% (eb5    "finite-topologies-3")

{\bf Finite topologies (3)}

$\resizebox{!}{70pt}{$
  (\Opens\left(\zdagW\right), ⊂_1)
  =
  \def\w{\zfW}\zdagOW
  $}
$

Non-planar! Why?

Answer: because the W has \ColorRed{three independent points!}



\newpage

% «finite-topologies-4»  (to ".finite-topologies-4")
% (eb5p 9 "finite-topologies-4")
% (eb5    "finite-topologies-4")

{\bf Finite topologies (4): 2CGs and ZHAs}

A \ColorRed{2-column graph} never has three independent points.

Trick: $\pile(25) = \{2▁,1▁,\;\;▁1,▁2,▁3,▁4,▁5\}$.

% (oxap 8 "fig:2CGs-ZHA")
% (oxa    "fig:2CGs-ZHA")
%
\linethickness{0.3pt}
% 
%L tdims = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7}   -- with v arrows
%L tspec_PA  = TCGSpec.new("46; 11 22 34 45, 25")
%L tspec_PAQ = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
%L tspec_PA :mp  ({zdef="O_A(P)"})  :addlrs():print()            :output()
%L tspec_PAQ:mp  ({zdef="O_A(P),J"}):addlrs():print()            :output()
%L tspec_PA :tcgq({tdef="(P,A)",   meta="1pt p"}, "lr q h v ap") :output()
%L tspec_PAQ:tcgq({tdef="(P,A),Q", meta="1pt p"}, "lr q h v ap") :output()
%L
%L tspec_PAC = TCGSpec.new("46; 11 22 34 45, 25", "?...", "???...")
%L tspec_PAC:mp  ({zdef="closed-op"}) :addlrs():print()            :output()
%L tspec_PAC:tcgq({tdef="closed-op", meta="1pt p"}, "lr q h v ap") :output()
%L 
\pu

\bsk

$\resizebox{!}{60pt}{$
  (\Opens\tcg{(P,A)}, ⊂_1)
  \;\;=\;\;
  \zha{O_A(P)}
  $}
$

\newpage

% «famous-J-operator»  (to ".famous-J-operator")
% (eb5p 10 "famous-J-operator")
% (eb5     "famous-J-operator")

{\bf A famous J-operator: $(13∨)$}

\bsk

$\resizebox{!}{60pt}{$
   \tcg{closed-op} \squigbij \zha{closed-op} \\
  $}
$

\newpage

% «strange-J-operator»  (to ".strange-J-operator")
% (eb5p 11 "strange-J-operator")
% (eb5     "strange-J-operator")

{\bf A strange J-operator}

\bsk

$\resizebox{!}{60pt}{$
   \tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
  $}
$



\newpage

%  _                _        _                 ______   _    _    
% | |    ___   __ _(_) ___  (_)_ __     __ _  |__  / | | |  / \   
% | |   / _ \ / _` | |/ __| | | '_ \   / _` |   / /| |_| | / _ \  
% | |__| (_) | (_| | | (__  | | | | | | (_| |  / /_|  _  |/ ___ \ 
% |_____\___/ \__, |_|\___| |_|_| |_|  \__,_| /____|_| |_/_/   \_\
%             |___/                                               
%
% «logic-in-a-ZHA»  (to ".logic-in-a-ZHA")
% (eb5p 12 "logic-in-a-ZHA")
% (eb5     "logic-in-a-ZHA")
% (lodp 27 "ipl-on-a-topology-2")
% (lod     "ipl-on-a-topology-2")

{\bf Logic in a ZHA (visually!!!)}

Notation: a 2-column graph is \ColorRed{$(P,A)$} --- (points, arrows) ---

its order topology is \ColorRed{$\Opens_A(P)$},

and a Planar Heyting Algebra (a ZHA) is $\ColorRed{H}⊂\Z^2$.

The correspondence is written as \ColorRed{$(P,A) \squigbij H$}

and formally it means $\Opens_A(P) ≅ H$.

There are two ways to define $⊤,⊥∈H$ and $∧,∨,→∈⊤$...

\msk

1) Via topology, in $\Opens_A(P)$:

$⊤:=P$,

$⊥:=∅$,

$Q∧R:=Q∩R$,

$Q∨R:=Q∪R$,

$R→S := \ColorRed{𝐬{Int}}((T∖R)∪S)$

\newpage

% «logic-in-a-ZHA-2»  (to ".logic-in-a-ZHA-2")
% (eb5p 13 "logic-in-a-ZHA-2")
% (eb5     "logic-in-a-ZHA-2")

{\bf Logic in a ZHA (visually!!!) (2)}

2) Via order. For example:

$\begin{array}{rcl}
 (Q→(R→S)) &↔& ((Q∧R)→S) \\
 (Q≤(R→S)) &↔& ((Q∧R)≤S) \\
 \setofst{Q∈H}{Q≤(R→S)} &=& \setofst{Q∈H}{(Q∧R)≤S} \\
 (R→S) &=& \sup \; \setofst{Q∈H}{(Q∧R)≤S} \\
       &=& ⋃ \; \setofst{Q∈H}{(Q∧R)≤S} \\
 \end{array}
$

\newpage

% «logic-in-a-ZHA-3»  (to ".logic-in-a-ZHA-3")
% (eb5p 14 "logic-in-a-ZHA-3")
% (eb5     "logic-in-a-ZHA-3")

{\bf Logic in a ZHA (visually!!!) (3)}

\bsk
\bsk

% (ph1p 11 "HAs")
% (ph1     "HAs")

%R local QoRai, PoQai, PnnP =
%R     1/    T    \, 1/    T    \, 1/ T   \
%R      |   . .   |   |   . .   |   |  .  | 
%R      |  . . .  |   |  . . .  |   | . . | 
%R      | . o . i |   | . o . . |   |d . n| 
%R      |. Q . . .|   |. P . . .|   | P . | 
%R      | . . R . |   | . . Q . |   \  F  / 
%R      |  . a .  |   |  . . .  |           
%R      |   . .   |   |   . .   |           
%R      \    F    /   \    F    /           
%R local T = {a="(∧)", o="(∨)", i="(\\!→\\!)", n="(¬)", d="(\\!\\!¬¬\\!)",
%R            T="·", F="·", T="⊤", F="⊥", }
%R PoQai:tozmp({def="PoQai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R QoRai:tozmp({def="QoRai", scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R PnnP :tozmp({def="PnnP" , scale="12pt", meta=nil}):addcells(T):addcontour():output()
%R
%R PoQai:tozmp({def="lozfive", scale="12pt", meta=nil}):addlrs():addcontour():output()
\pu
$$% \lozfive \qquad
  \QoRai
  %\qquad \PoQai
$$


\newpage

% «J-operators»  (to ".J-operators")
% (eb5p 15 "J-operators")
% (eb5     "J-operators")

{\bf J-operators}

A J-operator on a Heyting Algebra $H$ is an operation

$J:H→H$, abbreviated as `$·^*$', obeying $P≤P^*=P^{**}$

and $(P∧Q)^*=P^*∧Q^*$.

Some famous J-operators: $(¬¬)$, $(A∨)$, $(A→)$ (for $A∈H$).

\msk

A J-operator induces an equivalence relation:

$P ∼_J Q$ iff $P^*=Q^*$.

For many years I didn't have \ColorRed{ANY} visual intuition on

what J-operators were, or could be.

When we play with J-operators on ZHAs we discover that:

Each equivalence class $[P]^J$ has a top element, a bottom

element, and all element in between; and $P^*$ is always the

top element of $[P]^J$...

So we only need to \ColorRed{draw} the equivalence classes!


\newpage

% «famous-J-operator-2»  (to ".famous-J-operator-2")
% (eb5p 16 "famous-J-operator-2")
% (eb5     "famous-J-operator-2")

{\bf A famous J-operator: $(13∨)$}

\bsk

$\resizebox{!}{60pt}{$
   \tcg{closed-op} \squigbij \zha{closed-op} \\
  $}
$

\newpage

% «strange-J-operator-2»  (to ".strange-J-operator-2")
% (eb5p 17 "strange-J-operator-2")
% (eb5     "strange-J-operator-2")

{\bf A strange J-operator}

\bsk

$\resizebox{!}{60pt}{$
   \tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
  $}
$


\newpage

% «question-marks»  (to ".question-marks")
% (eb5p 18 "question-marks")
% (eb5     "question-marks")

{\bf Question marks}

Every set of question marks $Q⊆P$ in $(P,A)$ induces an equivalence
relation on $H≅\Opens_A(P)$. Two subsets $S,S'⊆P$ are
𝐢{$Q$-equivalent} when $S$ and $S'$ only differ in points of $Q$,
i.e.: $S∖Q = S'∖Q$. Here $Q=\{4▁,3▁,2▁,$ \; $▁1,▁2,▁3,▁5,\}$, and:

$\pile(22) ∼_Q \pile(23) \not∼_Q \pile(24)$,

$12^* = 23$, \;\; $22 ∼_J \pile23 \not∼_J 24$.

$\resizebox{!}{45pt}{$
   \tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
  $}
$

\newpage

% «question-marks-2»  (to ".question-marks-2")
% (eb5p 19 "question-marks-2")
% (eb5     "question-marks-2")

$\pile(22) ∼_Q \pile(23) \not∼_Q \pile(24)$,

$12^* = 23$, \;\; $22 ∼_J \pile23 \not∼_J 24$.

$\resizebox{!}{70pt}{$
   \tcg{(P,A),Q} \squigbij \zha{O_A(P),J}
  $}
$

\newpage

% «geometric-morphisms»  (to ".geometric-morphisms")
% (eb5p 20 "geometric-morphisms")
% (eb5     "geometric-morphisms")

{\bf Toposes, geometric morphisms, internal diagrams}

Internal diagrams are a tool to \ColorRed{lower the lever of abstraction}.

This is a \ColorRed{geometric morphism} between toposes.

%D diagram internal-gm
%D 2Dx     100 +20    +30 +20
%D 2D  100 A1  B1 <-| B2  C1
%D 2D      |   |       |   |
%D 2D      |   |  <->  |   |
%D 2D      v   v       v   v
%D 2D  +30 A2  B3 |-> B4  C2
%D 2D
%D 2D  +20     D1 <=> D2
%D 2D
%D 2D  +20     E1 --> E2
%D 2D
%D 2D  +20     F1     F2
%D 2D
%D ren A1 A2 ==> f^*f_*D D
%D ren B1 B2 B3 B4 ==> f^*C C D f_*D
%D ren C1 C2 ==> C f_*f^*C
%D ren B3 B4 ==> D f_*D
%D ren D1 D2 ==> \calE \calF
%D ren E1 E2 ==> \calE \calF
%D ren F1 F2 ==> \phantom{\catA} \phantom{\catB}
%D
%D (( A1 A2 -> .plabel= l εD
%D    C1 C2 -> .plabel= r ηC
%D
%D    B1 B2 <-|
%D    B1 B3 -> B2 B4 ->
%D    B3 B4 |->
%D    B1 B4 harrownodes nil 20 nil <->
%D
%D    D1 D2 <- sl^ .plabel= a f^*
%D    D1 D2 -> sl_ .plabel= b f_*
%D    E1 E2 -> .plabel= a f
%D    
%D    F1 place F2 place
%D ))
%D enddiagram
%D
%D diagram internal-zgm
%D 2Dx     100 +20    +30 +20
%D 2D  100 A1  B1 <-| B2  C1
%D 2D      |   |       |   |
%D 2D      |   |  <->  |   |
%D 2D      v   v       v   v
%D 2D  +30 A2  B3 |-> B4  C2
%D 2D
%D 2D  +20     D1 <=> D2
%D 2D
%D 2D  +20     E1 --> E2
%D 2D
%D 2D  +20     F1     F2
%D 2D
%D ren A1 A2 ==> f^*f_*D D
%D ren B1 B2 B3 B4 ==> f^*C C D f_*D
%D ren C1 C2 ==> C f_*f^*C
%D ren B3 B4 ==> D f_*D
%D ren D1 D2 ==> \Set^\catA \Set^\catB
%D ren E1 E2 ==> \Set^\catA \Set^\catB
%D ren F1 F2 ==> \catA \catB
%D
%D (( A1 A2 -> .plabel= l εD
%D    C1 C2 -> .plabel= r ηC
%D
%D    B1 B2 <-|
%D    B1 B3 -> B2 B4 ->
%D    B3 B4 |->
%D    B1 B4 harrownodes nil 20 nil <->
%D
%D    D1 D2 <- sl^ .plabel= a f^*
%D    D1 D2 -> sl_ .plabel= b f_*
%D    E1 E2 -> .plabel= a f
%D    
%D    F1 F2 -> .plabel= a f
%D ))
%D enddiagram
%D
\pu

\msk

$\resizebox{!}{70pt}{$
   \diag{internal-gm}
  $}
$

\newpage

% «geometric-morphisms-2»  (to ".geometric-morphisms-2")
% (eb5p 21 "geometric-morphisms-2")
% (eb5     "geometric-morphisms-2")

{\bf Toposes, geometric morphisms, internal diagrams (2)}

Let $\catA$ and $\catB$ be 2CGs regarded as categories.

Then a functor $f:\catA→\catB$ induces a geometric morphism...

\msk

$\resizebox{!}{60pt}{$
   \diag{internal-zgm}
  $}
$

\msk

And if we draw the internal views of $\catA$, $\catB$, $C$, $D$...

\newpage

% «geometric-morphisms-3»  (to ".geometric-morphisms-3")
% (eb5p 22 "geometric-morphisms-3")
% (eb5     "geometric-morphisms-3")


%R sesw = {[" w"]="↙",  [" e"]="↘"}
%R
%R local zcB, zpBC, zpBRD
%R  = 3/       1             \, 3/      C_1            \, 3/      !Dt            \
%R     |    w     e          |   |    w     e          |   |    w     e          |
%R     | 2           3       |   |C_2         C_3      |   |D_2         D_3      |
%R     |    e     w     e    |   |    e     w     e    |   |    e     w     e    |
%R     |       4           5 |   |      C_4         C_5|   |      D_4         D_5|
%R     |          e     w    |   |          e     w    |   |          e     w    |
%R     \             6       /   \            C_6      /   \             1       /
%R
%R local zpBRLC
%R  =                           3/      !Ct            \
%R                               |    w     e          |
%R                               |C_2         C_3      |
%R                               |    e     w     e    |
%R                               |      C_4         C_5|
%R                               |          e     w    |
%R                               \             1       /
%R
%R local zcA, zpALC, zpAD
%R  = 3/ 2           3       \, 3/C_2         C_3      \, 3/D_2         D_3      \
%R     |    e     w     e    |   |    e     w     e    |   |    e     w     e    |
%R     \       4           5 /   \      C_4         C_5/   \      D_4         D_5/
%R                
%R zcB   :tozmp({def="zcB",    scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBC  :tozmp({def="zpBC",   scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBRD :tozmp({def="zpBRD" , scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBRLC:tozmp({def="zpBRLC", scale="7pt", meta="s p"}):addcells(sesw):output()
%R zcA   :tozmp({def="zcA",    scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpALC :tozmp({def="zpALC",  scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpAD  :tozmp({def="zpAD",   scale="7pt", meta="s p"}):addcells(sesw):output()

%D diagram internal-zgm-particular-case
%D 2Dx     100 +50    +55 +50
%D 2D  100 A1  B1 <-| B2  C1
%D 2D      |   |       |   |
%D 2D      |   |  <->  |   |
%D 2D      v   v       v   v
%D 2D  +50 A2  B3 |-> B4  C2
%D 2D
%D 2D  +30     D1 <=> D2
%D 2D
%D 2D  +20     E1 --> E2
%D 2D
%D 2D  +30     F1     F2
%D 2D
%D ren A1 B1 B2 C1 ==> \zpALC  \zpALC \zpBC   \zpBC
%D ren A2 B3 B4 C2 ==> \zpAD   \zpAD  \zpBRD  \zpBRLC
%D ren D1 D2 ==> \Set^\catA \Set^\catB
%D ren E1 E2 ==> \Set^\catA \Set^\catB
%D ren F1 F2 ==> \catA \catB
%D ren F1 F2 ==> \zcA \zcB
%D
%D (( A1 A2 -> .plabel= l εD
%D    C1 C2 -> .plabel= r ηC
%D
%D    B1 B2 <-|
%D    B1 B3 -> B2 B4 ->
%D    B3 B4 |->
%D    B1 B4 harrownodes nil 20 nil <->
%D
%D    D1 D2 <- sl^ .plabel= a f^*
%D    D1 D2 -> sl_ .plabel= b f_*
%D    E1 E2 -> .plabel= a f
%D    
%D    F1 F2 -> .plabel= a f
%D ))
%D enddiagram
%D

\def\Ct{C_2 {×_{C_4}} C_3}
\def\Dt{D_2 {×_{D_4}} D_3}

\pu

$\resizebox{!}{100pt}{$
   \diag{internal-zgm-particular-case}
  $}
$

\newpage

% «a-factorization»  (to ".a-factorization")
% (eb5p 23 "a-factorization")
% (eb5     "a-factorization")

{\bf A factorization}

The Elephant presents in its sections A4.2 and A4.5 two factorizations
of geometric morphisms that can be combined in a single diagram (next
slide). An arbitrary geometry morphism $g:\calA→\calD$ can be factored
in an essentially unique way as a surjection followed by an inclusion
([EA4.2.10]), and an inclusion $i:\calB→\calD$ can be factored in an
essentially unique way as a dense g.m.\ followed by a closed
g.m.\ ([EA4.5.20]). A canonical way to build these factorizations is
by taking $\calB := \calA_\bbG$, where $\bbG$ is a certain comonad on
$\calA$ ([EA4.2.8]), and taking $\calC := \sh_j(\calD)$, where $j$ is
a certain local operator on $\calD$.

\newpage

% «a-factorization-2»  (to ".a-factorization-2")
% (eb5p 24 "a-factorization-2")
% (eb5     "a-factorization-2")

{\bf A factorization (2)}

\bsk

%D diagram factorization-1
%D 2Dx     100 +50 +40 +40
%D 2D  100 A0          A3
%D 2D
%D 2D  +12 B0  B1      B3
%D 2D
%D 2D  +12     C1  C2  C3
%D 2D
%D 2D  +12     D1  D2
%D 2D
%D ren A0       A3 ==> \calA             \calD
%D ren B0 B1    B3 ==> \calA \calB       \calD
%D ren    C1 C2 C3 ==>       \calB \calC \calD
%D ren    D1 D2    ==> \calA_\bbG \sh_j(\calD)
%D
%D (( A0 A3 -> .plabel= a \vtext{g}{\anygm}
%D    B0 B1 -> .plabel= a \vtext{s}{surjection}
%D    B1 B3 -> .plabel= a \vtext{i}{inclusion}
%D    C1 C2 -> .plabel= a \vtext{d}{dense}
%D    C2 C3 -> .plabel= a \vtext{c}{closed}
%D    D1 place
%D    D2 place
%D ))
%D enddiagram
%D
%D diagram factorization-2
%D 2Dx     100 +55 +45 +45
%D 2D  100 A0          A3
%D 2D
%D 2D  +12 B0  B1      B3
%D 2D
%D 2D  +12     C1  C2  C3
%D 2D
%D 2D  +12     D1  D2
%D 2D
%D 2D  +20 a0          a3
%D 2D
%D 2D  +12 b0  b1      b3
%D 2D
%D 2D  +12     c1  c2  c3
%D 2D
%D ren A0       A3 ==> \Set^\catA                       \Set^\catD
%D ren B0 B1    B3 ==> \Set^\catA \Set^\catB            \Set^\catD
%D ren    C1 C2 C3 ==>            \Set^\catB \Set^\catC \Set^\catD
%D ren    D1 D2    ==>     (\Set^\catA)_\bbG \sh_j(\Set^\catD)
%D
%D ren a0       a3 ==>       \catA                           \catD
%D ren b0 b1    b3 ==>       \catA     \catB                 \catD
%D ren    c1 c2 c3 ==>                 \catB      \catC      \catD
%D
%D (( A0 A3 -> .plabel= a \vtext{g}{\anygm}
%D    B0 B1 -> .plabel= a \vtext{s}{surjection}
%D    B1 B3 -> .plabel= a \vtext{i}{inclusion}
%D    C1 C2 -> .plabel= a \vtext{d}{dense}
%D    C2 C3 -> .plabel= a \vtext{c}{closed}
%D    D1 place
%D    D2 place
%D    a0 a3 -> .plabel= a g
%D    b0 b1 -> .plabel= a s
%D    b1 b3 -> .plabel= a i
%D    c1 c2 -> .plabel= a d
%D    c2 c3 -> .plabel= a c
%D ))
%D enddiagram
%D
%D diagram fact-characterization
%D 2Dx     100 +20 +30 +20 +45 +20 +30 +20 +35 +20 +30 +20 +20 +20 +30 +20
%D 2D  100 A0  A1  A2  A3  B0  B1                  B2  B3  
%D 2D                                                      
%D 2D  +20 A4  A5  A6  A7  B4  B5                  B6  B7  
%D 2D                                                      
%D 2D  +20     A8  A9          B8                  B9      
%D 2D                                                      
%D 2D  +20     a8  a9          b8                  b9      
%D 2D
%D 2D  +20                 C0  C1  C2  C3  D0  D1  D2  D3 
%D 2D                                                     
%D 2D  +20                 C4  C5  C6  C7  D4  D5  D6  D7 
%D 2D                                                     
%D 2D  +20                     C8  C9          D8  D9     
%D 2D                                                     
%D 2D  +20                     c8  c9          d8  d9     
%D 2D
%D ren A4 A5 A6 A0 ==> A A s_*A s^*s_*A
%D ren A3 A2 A1 A7 ==> B B s^*B s_*s^*B
%D ren A8 A9 a8 a9 ==> \Set^\catA \Set^\catB \catA \catB
%D
%D ren B4 B5 B6 B0 ==> B B i_*B i^*i_*B
%D ren B3 B2 B1 B7 ==> D D i^*D i_*i^*D
%D ren B8 B9 b8 b9 ==> \Set^\catB \Set^\catD \catB \catD
%D
%D ren C4 C5 C6 C0 ==>  B B d_*B d^*d_*B
%D ren C3 C2 C1 C7 ==> kC C d^*C d_*d^*kC
%D ren C8 C9 c8 c9 ==> \Set^\catB \Set^\catC \catB \catC
%D
%D ren D4 D5 D6 D0 ==> C C c_*C c^*c_*C
%D ren D3 D2 D1 D7 ==> D D c^*D c_*c^*D
%D ren D8 D9 d8 d9 ==> \Set^\catC \Set^\catD \catC \catD
%D
%D (( A0 A4 -> .plabel= l {}
%D    A3 A7 -> .plabel= r \text{(monic)}
%D    A1 A2 <-| A1 A5 -> A2 A6 -> A5 A6 |->
%D    A1 A6 harrownodes nil 20 nil <->
%D    A8 A9 <- sl^ .plabel= a s^*
%D    A8 A9 -> sl_ .plabel= b s_*
%D    a8 a9 ->     .plabel= a s
%D ))
%D 		   
%D (( B0 B4 -> .plabel= l \text{(iso)}
%D    B3 B7 -> .plabel= r {}
%D    B1 B2 <-| B1 B5 -> B2 B6 -> B5 B6 |->
%D    B1 B6 harrownodes nil 20 nil <->
%D    B8 B9 <- sl^ .plabel= a i^*
%D    B8 B9 -> sl_ .plabel= b i_*
%D    b8 b9 ->     .plabel= a i
%D ))
%D 		   
%D (( C0 C4 -> .plabel= l {}
%D    C3 C7 -> .plabel= r \sm{\text{(monic}\\\text{on\;c.p.s)}}
%D    C1 C2 <-| C1 C5 -> C2 C6 -> C5 C6 |->
%D    C1 C6 harrownodes nil 20 nil <->
%D    C8 C9 <- sl^ .plabel= a d^*
%D    C8 C9 -> sl_ .plabel= b d_*
%D    c8 c9 ->     .plabel= a d
%D ))
%D 		   
%D (( D0 D4 -> .plabel= l {}
%D    D3 D7 -> .plabel= r {}
%D    D1 D2 <-| D1 D5 -> D2 D6 -> D5 D6 |->
%D    D1 D6 harrownodes nil 20 nil <->
%D    D8 D9 <- sl^ .plabel= a c^*
%D    D8 D9 -> sl_ .plabel= b c_*
%D    d8 d9 ->     .plabel= a c
%D ))
%D 		   
%D enddiagram
%D
\pu
\def\vtext#1#2{#1\text{ (#2)}}
\def\anygm{any g.m.}

  $
   \diag{factorization-1}
  $

\newpage

% «a-factorization-3»  (to ".a-factorization-3")
% (eb5p 25 "a-factorization-3")
% (eb5     "a-factorization-3")

{\bf A factorization (3)}

\bsk



  $
   \diag{factorization-2}
  $


\newpage

% «a-factorization-4»  (to ".a-factorization-4")
% (eb5p 26 "a-factorization-4")
% (eb5     "a-factorization-4")

{\bf A factorization (4)}

\msk

  \resizebox{1.0\textwidth}{!}{$%
    \diag{fact-characterization}
  $}

\msk

These factorizations are almost completely opaque to people who know
just the basics of toposes... how can we?...

\newpage

% produce a version ``for
% children'' of them in the sense of section \ref{cats-for-children}?
%
% \newpage


%  ____  _                                        _                        
% / ___|| |__   __ _ _ __   ___    __ _ _ __   __| |  _ __ ___   _____   __
% \___ \| '_ \ / _` | '_ \ / _ \  / _` | '_ \ / _` | | '_ ` _ \ / _ \ \ / /
%  ___) | | | | (_| | |_) |  __/ | (_| | | | | (_| | | | | | | | (_) \ V / 
% |____/|_| |_|\__,_| .__/ \___|  \__,_|_| |_|\__,_| |_| |_| |_|\___/ \_/  
%                   |_|                                                    
%
% «shape-and-movement»  (to ".shape-and-movement")
% (eb5p 27 "shape-and-movement")
% (eb5     "shape-and-movement")

{\bf Shape and movement}

This is how I remember the Frobenius Property:


%
%D diagram Frob-std
%D 2Dx    100          +45 +35 +10     +30
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |---------------> b1
%D 2D
%D (( B0 .tex= P                            B1  .tex=  Σ_fP
%D    B2 .tex= P∧f^*Q  B3 .tex= Σ_f(P∧f^*Q) B3' .tex= (Σ_fP)∧Q
%D    B4 .tex= f^*Q                         B5  .tex=     Q
%D    b0 .tex= A                            b1  .tex=     B
%D ))
%D ((
%D    B0 B1 |->   B2 B0 -> B3 B1 -> B3' B1 ->
%D    B4 B5 <-|   B2 B4 -> B3 B5 -> B3' B5 ->
%D    B2 B3 |->   B3 B3' -> sl^ .plabel= a \nat  B3 B3' <- sl_ .plabel= b 𝐬{Frob}
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 b1 -> .plabel= a f
%D ))
%D enddiagram
%

% (idap 1 "mental-space")
% (ida    "mental-space")
% (ida    "mental-space" "frob-sketch.eps")
% (idap 19 "pres-frob-bcc")
% (ida     "pres-frob-bcc")

\bsk
\bsk

$\pu
  \def∧{{\land}}
  %
  \resizebox{!}{40pt}{$\diag{Frob-std}$}
  \quad
  \myvcenter{
  \includegraphics[scale=0.8]{frob-sketch.eps}
  }
$

\bsk
\bsk

\ColorBrown{(From ``Internal Diagrams and Archetypal Reasoning
in

Category Theory'' (Ochs 2013))}


\newpage

%  _____                                 _                     
% |_   _|   _ _ __   ___   ___ _   _ ___| |_ ___ _ __ ___  ___ 
%   | || | | | '_ \ / _ \ / __| | | / __| __/ _ \ '_ ` _ \/ __|
%   | || |_| | |_) |  __/ \__ \ |_| \__ \ ||  __/ | | | | \__ \
%   |_| \__, | .__/ \___| |___/\__, |___/\__\___|_| |_| |_|___/
%       |___/|_|               |___/                           
%
{\bf Formalizing diagrams in type systems}

...so I got lots of diagrams for things in CT --- for example, the
construction that uses a comonad in the 



\end{document}

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