% (find-angg "LATEX/2019oxford-diags.tex")
% (find-angg "LATEX/2019oxford-diags.dnt")
% (defun dn () (interactive) (find-angg "LATEX/2019oxford-diags.dnt"))
% (find-LATEXsh "lualatex 2019oxford-diags.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019oxford-diags.tex" :end))
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019oxford-diags.tex 2>&1 | tee /tmp/o" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2019oxford-diags.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019oxford-diags.pdf"))
% (defun e () (interactive) (find-LATEX "2019oxford-diags.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019oxford-diags"))
% (find-xpdfpage "~/LATEX/2019oxford-diags.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019oxford-diags.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019oxford-diags.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019oxford-diags.pdf
%               file:///tmp/2019oxford-diags.pdf
%           file:///tmp/pen/2019oxford-diags.pdf
% http://angg.twu.net/LATEX/2019oxford-diags.pdf
\documentclass[oneside,11pt]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{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{ifluatex}
\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")
%
\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")
%L io.stdout:setvbuf("no")
\pu




% «.defs»		(to "defs")
% «.cats-for-children»	(to "cats-for-children")
% «.internal-diagrams»	(to "internal-diagrams")
% «.ZCategories»	(to "ZCategories")
% «.two-factorizations»	(to "two-factorizations")
% «.characterization»	(to "characterization")
% «.sheaves-on-2CGs»	(to "sheaves-on-2CGs")
% «.references»		(to "references")



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

\input 2017planar-has-defs.tex
% For: (find-LATEX "2017planar-has-defs.tex" "picturedots")
%      (find-LATEX "2017planar-has-defs.tex" "squigbij")
%      (find-LATEX "2017planar-has-defs.tex" "defzha-and-deftcg")
%
\def\termdef#1{{\sl #1}}
\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\bbG{{\mathbb{G}}}
\def\sh{{\mathbf{sh}}}




%   ____      _          __                   _     _ _     _                
%  / ___|__ _| |_ ___   / _| ___  _ __    ___| |__ (_) | __| |_ __ ___ _ __  
% | |   / _` | __/ __| | |_ / _ \| '__|  / __| '_ \| | |/ _` | '__/ _ \ '_ \ 
% | |__| (_| | |_\__ \ |  _| (_) | |    | (__| | | | | | (_| | | |  __/ | | |
%  \____\__,_|\__|___/ |_|  \___/|_|     \___|_| |_|_|_|\__,_|_|  \___|_| |_|
%                                                                            
% «cats-for-children»  (to ".cats-for-children")
\section{Categories for Children}
\label{cats-for-children}

I started using the expression ``for children'' a long time ago, at
first informally. I realized that toposes could be the right tool to
study a variation of Non-Standard Analysis in which the ultrafilters
were replaced by filters, and I tried {\sl very hard} to read
\cite{Johnstone} and \cite{Goldblatt}. I did not go very far, and I
kept saying to my friends ``{\sl I need a version for children of
  this!}''. My problem was that I felt that for stylistical reasons
99\% of the diagrams were omitted from text, and the examples were
mentioned very briefly or not at all... those books were intended for
``adult'' readers who knew --- maybe from contact with the ``oral
culture'' of the area? --- how to produce the ``missing'' diagrams,
examples, and calculations easily by themselves.

In this work we will see a method that can be used to produce these
``missing diagrams'' in a somewhat canonical way. When we define
``children'' precisely, not in the sense of {\sl who they are} but in
the sense of {\sl what kinds of tools and examples they prefer when
  they try to learn something that is too abstract}, we get guidelines
for what kinds of concrete cases we should look for. If we establish
that ``children'' have favourite {\sl shapes} for drawing their
categorical diagrams, then they will draw the diagrams for the general
case and for a particular case in parallel in similar shapes, in a way
that lets them {\sl transfer knowledge} between the general and the
particular cases quite easily; and the same between the ``external
diagrams'' and the ``internal diagrams'' of section
\ref{internal-diagrams}.

In strictly mathematical terms this work is almost trivial. The result
sketched in section \ref{two-factorizations}, that certain
factorizations of geometric morphisms can be performed without leaving
the realm of ZToposes, seems to be new, and the handful of experts to
whom I showed the way of drawing sheaves in section
\ref{sheaves-on-2CGs} told me that that was easy to believe, but
they've never seen that in print and they didn't think it was
folklore.


like to draw
their categorical diagrams all in 


 It turned out that





In this work we will reuse some ideas from \cite{OchsIDARCT}, that was
mostly about how to {\sl erase} and then {\sl reconstruct} information
from proofs; in particular, its sections 10 and 11 are about what
happens when an author discovers a theorem, publishes it, and then a
reader reads that, fills up the gaps in what was left implicit, and
(sort of) reconstructs in his mind the author's intuitions. Here we
will take a much more solid, or harder, view on how this
reconstruction process works.

% (find-angg ".emacs" "idarct-preprint")
% (find-idarctpage 12 "10. Transmission")
% (find-idarcttext 12 "10. Transmission")
% (find-idarctpage 13 "11. Intuition")
% (find-idarcttext 13 "11. Intuition")

The following {\sl definition} of ``children'' turned out to the
especially fruitful:

% (find-LATEX "catsem-u.bib" "bib-Johnstone")
% (find-LATEX "catsem-u.bib" "bib-Goldblatt" "NOT THERE")

% (find-angg       "LATEX/2019ebl-abs.tex")
% (find-pdf-page "~/LATEX/2019ebl-abs.pdf")
% http://angg.twu.net/logic-for-children-2018.html#second-description
% (vivp 7 "bigger-project")
% (viv    "bigger-project")


%  ___       _                        _       _ _                 
% |_ _|_ __ | |_ ___ _ __ _ __   __ _| |   __| (_) __ _  __ _ ___ 
%  | || '_ \| __/ _ \ '__| '_ \ / _` | |  / _` | |/ _` |/ _` / __|
%  | || | | | ||  __/ |  | | | | (_| | | | (_| | | (_| | (_| \__ \
% |___|_| |_|\__\___|_|  |_| |_|\__,_|_|  \__,_|_|\__,_|\__, |___/
%                                                       |___/     
% «internal-diagrams»  (to ".internal-diagrams")
\section{Internal Diagrams}
\label{internal-diagrams}

% (find-LATEXgrep "grep --color -niH -e internal *.tex")
% (vivp 22 "internal-views")
% (viv     "internal-views")




\subsection{Functors}


\subsection{Natural transformations}

\subsection{Adjunctions}

\subsection{Geometric Morphisms}

% (vivp 26 "internal-views-gm-2")
% (viv     "internal-views-gm-2")

%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 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 ==> \calA \calB
%D ren E1 E2 ==> \calA \calB
%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 ))
%D enddiagram
%D
$$\pu
  \diag{internal-gm}
$$




%  _________      _       
% |__  / ___|__ _| |_ ___ 
%   / / |   / _` | __/ __|
%  / /| |__| (_| | |_\__ \
% /____\____\__,_|\__|___/
%                         
% «ZCategories»  (to ".ZCategories")
% (find-LATEX "2017planar-has-1.tex" "positional")
% \section{Categories drawn in a canonical way}

\section{Categories with coordinates}
\label{ZCategories}

Let's see a way to define finite categories whose objects have
coordinates in $\N^2$ and whose arrows can be named by just their
sources and targets. We call these categories \termdef{ZCategories},
and it's easier to start with an example. The figure at the left below
is a ZCategory $\catA$ whose objects are $\catA_0 = \{1,2,3,4,5\}$,
with coordinates $c(1)=(0,2)$, $c(2)=(1,1)$, $c(3)=(2,1)$,
$c(4)=(1,0)$, $c(5)=(2,0)$. The arrow $2→4$ belongs to $\catA$, but it
is not shown. The figure at the right below is a functor
$F:\catA→\Set$ --- a \termdef{ZTopos}.

%D diagram ZCatA
%D 2Dx     100 +20 +20
%D 2D  100 o1
%D 2D
%D 2D  +20     o2  o3
%D 2D
%D 2D  +20     o4  o5
%D 2D
%D ren o1 o2 o3 o4 o5 ==> 1 2 3 4 5
%D
%D (( o1 o2 -> o1 o3 -> o1 o4 ->
%D    o2 o3 -> o2 o4 -> o3 o5 -> o4 o5 ->
%D
%D ))
%D enddiagram
%
%D diagram ZToposF
%D 2Dx     100 +20 +20
%D 2D  100 o1
%D 2D
%D 2D  +20     o2  o3
%D 2D
%D 2D  +20     o4  o5
%D 2D
%D ren o1 o2 o3 o4 o5 ==> F_1 F_2 F_3 F_4 F_5
%D
%D (( o1 o2 -> o1 o3 -> o1 o4 ->
%D    o2 o3 -> o2 o4 -> o3 o5 -> o4 o5 ->
%D
%D ))
%D enddiagram

$$\pu
  \catA =
    \left(
    \diag{ZCatA}
    \right)
  \quad
  F =
    \left(
    \diag{ZToposF}
    \right)
$$

A \termdef{ZSet} is a finite set $P⊂\N^2$ that touches both the
$x$-axis and the $y$-axis. A \termdef{ZDirectedGraph} is a pair
$(P,A)$ where $P$ is a ZSet and $A⊆P×P$ is a set of arrows. We write
$(P,A^*)$ for the transitive-reflexive closure of $(P,A)$.

The section 1 of [PH1] defines positional notations for ZSets and for
functions with ZSets as their domains. They're like this:

% (ph1p 3 "positional")
% (ph1    "positional")
% (ph1    "positional" "(1,3)")

%L defpictdots("a", "Kaxes", 0,0,2,3,nil, " 1,3 0,2 2,2 1,1 1,0 ")
%L defpictdots(nil, "K",     0,0,2,3,nil, " 1,3 0,2 2,2 1,1 1,0 ")
\pu

$$\csm{        (1,3),        \\
        (0,2), \;\;\; (2,2), \\
               (1,1),        \\
               (1,0)         \\
      }
  = \;\pido{Kaxes}\;
  = \;\pido{K}
  %
  \qquad
  %
  \csm{            ((1,3),4),            \\
        ((0,2),5), \;\;\;   ((2,2),6), \\
                   ((1,1),7),            \\
                   ((1,0),8)             \\
      }
  = 
  \sm{    & 4 &   \\
        5 &   & 6 \\
          & 7 &   \\
          & 8 &   \\
      }
$$

The condition ``{\sl ...that touches both the $x$-axis and the
  $y$-axis}'' lets us draw ZSets as just bullets, omitting the axes.

A {\sl ZCategory} $\catB$ is a category plus a structure $((P,A),c)$,
called its {\sl drawing instructions}, obeying: 1) $(P,A)$ is a
ZDirectedGraph; 2) $c:\catB_0→P$ is a bijection between the objects of
$\catB$ and the ZSet $P$; 3) for any objects $D,E∈\catB$ the hom-set
$\Hom_\catB(D,E)$ is singleton when $(c(D),c(E))∈A^*$, and is empty
when $(c(D),c(E)) \not∈ A^*$. The conditions 1--3 imply that a
ZCategory is a finite preorder category; the coordinates say where
each object is to be draw, and the set $A$ says which arrows are to be
draw ``explicitly'' the other arrows are said to be ``implicit''.

A {\sl ZTopos} is a functor category of the form $\Set^\catB$, where
$\catB$ is a ZCategory. Objects of a ZTopos $\Set^\catB$ inheret the
drawing instructions from $\catB$, as the $F$ in the example above.

We call the objects of a ZTopos {\sl ZPresheaves}. Note that a {\sl
  presheaf} $P$ on $\catB$ is an element of $\Set^{\catB^\op}$, which
means that for each arrow $D→E$ in $\catB$ the presheaf $P$ returns an
arrow $P(D→E):PE→PD$ in $\Set$; ZPresheaves don't have this reversal
of direction.






%  _____          _             _          _   _             
% |  ___|_ _  ___| |_ ___  _ __(_)______ _| |_(_) ___  _ __  
% | |_ / _` |/ __| __/ _ \| '__| |_  / _` | __| |/ _ \| '_ \ 
% |  _| (_| | (__| || (_) | |  | |/ / (_| | |_| | (_) | | | |
% |_|  \__,_|\___|\__\___/|_|  |_/___\__,_|\__|_|\___/|_| |_|
%                                                            
% «two-factorizations»  (to ".two-factorizations")

\section{Two factorizations}
\label{two-factorizations}

The Elephant presents in its sections A4.2 and A4.5 two factorizations
of geometric morphisms that can be combined in a single diagram ---
see Figure 1. 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$.

% (elep 10 "elephant-fact-p.182")
% (ele     "elephant-fact-p.182")
% (elep 10 "elephant-A4.2.10" "surjection followed by an inclusion")
% (ele     "elephant-A4.2.10" "surjection followed by an inclusion")
% (find-elephantpage (+ 17 183) "Theorem 4.2.10")

% (elep 16 "elephant-A4.5.20" "factorization" "dense" "closed")
% (ele     "elephant-A4.5.20" "factorization" "dense" "closed")

% (vgmp 15 "a-factorization")
% (vgm     "a-factorization")

%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
$$\pu
  \def\vtext#1#2{#1\text{ (#2)}}
  \def\anygm{any g.m.}
  \diag{factorization-1}
$$

These factorizations are almost completely opaque to people who know
just the basics of toposes. How can we produce a version ``for
children'' of them in the sense of section \ref{cats-for-children}?

The trick is to start with geometric morphisms whose internal views
can be drawn explicity --- the ZGMs of section \ref{?}. Actually we
start with the lower level of Figure 2, and with the belief that all
factorizations can be performed within ZGMs.

%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
$$\pu
  \def\vtext#1#2{#1\text{ (#2)}}
  \def\anygm{any g.m.}
  \diag{factorization-2}
$$

We begin with an arbitrary functor $\catA \ton{g} \catD$ between
ZCategories, and we try to find a factorization $\catA \ton{s} \catB
\ton{i} \catD$ such that geometric morphisms $\Set^\catA \ton{s}
\Set^\catB \ton{i} \Set^\catD$ induced by these functors $s$ and $i$
obey the characterizations for surjections and inclusions in the next
section; then we try to find a factorization $\catB \ton{d} \catC
\ton{c} \catD$ such that the geometric morphisms $d$ and $c$ are dense
and closed. The objects $(\Set^\catA)_\bbG$ and $\sh_j(\Set^\catD)$
become secondary: the functors $s$, $i$, $d$, $c$ and their
corresponding geometric morphisms give us some feeling of what being a
surjection, inclusion, dense or closed ``mean'', and we can learn the
comonad-based construction of $(\Set^\catA)_\bbG$ and the sheaf-based
construction $\sh_j(\Set^\catD)$ at a later stage, knowing that their
toposes will be isomorphic to $\Set^\catB$ and $\Set^\catC$.





%   ____ _                          _            _          _   _             
%  / ___| |__   __ _ _ __ __ _  ___| |_ ___ _ __(_)______ _| |_(_) ___  _ __  
% | |   | '_ \ / _` | '__/ _` |/ __| __/ _ \ '__| |_  / _` | __| |/ _ \| '_ \ 
% | |___| | | | (_| | | | (_| | (__| ||  __/ |  | |/ / (_| | |_| | (_) | | | |
%  \____|_| |_|\__,_|_|  \__,_|\___|\__\___|_|  |_/___\__,_|\__|_|\___/|_| |_|
%                                                                             
% «characterization»  (to ".characterization")
% (vgmp 18 "surjection-inclusion")
% (vgm     "surjection-inclusion")

\section{A characterization}


% (elep 8 "elephant-A4.2.6" "surjection")
% (elep 9 "elephant-A4.2.6" "surjection" "(iv)")
% (ele    "elephant-A4.2.6" "surjection")
% [EA] 4.2.6 (iv)
%
$f$ is a {\sl surjection} when for every object $C∈\calB$ the unit map
$ηC$ is monic

% (elep 9 "elephant-A4.2.9" "inclusion")
% (ele    "elephant-A4.2.9" "inclusion")
% [EA], 4.2.8-4.2.9
%
$f$ is an {\sl inclusion} when for every object $D∈\calA$ the unit map $εD$ is an iso

% (elep 5 "dense-closed")
% (ele    "dense-closed")
%
$f$ is an {\sl dense} when for every constant presheaf $C$ the unit
map $εD$ is a monic

% (ph2p 29 "polynomial-J-ops" "closed quotient")
% (ph2     "polynomial-J-ops" "closed quotient")
% (ph2p 31 "polynomial-J-ops" "Using this new notation")
% (ph2     "polynomial-J-ops" "Using this new notation")
%
$f$ is {\sl closed} when all the `?'s are below `!'




%  ____  _                                               ____   ____ ____     
% / ___|| |__   ___  __ ___   _____  ___    ___  _ __   |___ \ / ___/ ___|___ 
% \___ \| '_ \ / _ \/ _` \ \ / / _ \/ __|  / _ \| '_ \    __) | |  | |  _/ __|
%  ___) | | | |  __/ (_| |\ V /  __/\__ \ | (_) | | | |  / __/| |__| |_| \__ \
% |____/|_| |_|\___|\__,_| \_/ \___||___/  \___/|_| |_| |_____|\____\____|___/
%                                                                             
% «sheaves-on-2CGs»  (to ".sheaves-on-2CGs")

\section{Sheaves on 2-Column Graphs}
\label{sheaves-on-2CGs}

The preprints [PH1] and [PH2] explain how to use {\sl 2-column graphs}
(``{\sl 2CGs}'') to develop visual intuition about intuitionistic
logic (the first one) and sheaves (the second one).

The central constructions in [PH1] and [PH2] can be stated,
respectively, as: 1) every 2CG is associated to a Planar Heyting
Algebra (a ``ZHA''; see sec.4 of [PH1] for a formal definition), and
vice-versa; and 2) every 2CG with question marks is associated to a
ZHA with a slashing and vice-versa. Formally, a 2CG $(P,A)$ is
associated to a ZHA $H$ when $H$ is isomorphic to the order topology
$\Opens_A(P)$, and a 2CG with question marks $((P,A),Q)$ is associated
with a ZHA with J-operator $(H,J)$ when the equivalence relation that
$Q$ induces on $\Opens_A(P)$ is the same as the one that $J$ induces
on $H$. These correspondences can be represented as Figure 4 ---
`$\squigbijbody$' is pronounced ``is associated to''.

$$\begin{array}{rcl}
      (P,A) & \squigbijbody & \Opens_A(P) \\
  % \\
  ((P,A),Q) & \squigbijbody & (\Opens_A(P),J) \\
  \end{array}
$$




These constructions are easy to
understand from examples but hard to formalize, so let's look at
Figure 2.

%
%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()
\pu

$$\linethickness{0.3pt}
  \begin{array}{ccl}
  \tcg{(P,A)}   & \squigbij & \zha{O_A(P)}   \\
  \\           
  \tcg{(P,A),Q} & \squigbij & \zha{O_A(P),J} \\
  \end{array}
$$



The top half shows a 2CG $(P,A)$, at the left, and its associated
order topology $\Opens_A(P)$ at the right.

Let's define $\pile(a,b) := \{1▁,\dots,a▁, \; ▁1,\ldots,▁b\}$; note
that $\pile(46)=P$. the operation $\pile$ lets us regard a 2-digit
number like 25 at the right of the `$\squigbijbody$' as abbreviation
for $\pile(25)$ and so as a subset of $P$.

The topology $\Opens_A(P)$ is defined by treating each arrow $α→β$ in
$A$ as a condition that subsets of $P$ have to obey in order to be
open. A subset $S⊆P$ is open iff it obeys the conditions associated to
all arrows $α→β$ in $A$. The condition associated to $α→β$ is
$α∈S→β∈S$, but we can convert it to something more visual by using
characteristic functions: $α∈S→β∈S$ is equivalent to
$χ_S(α)=1→χ_S(b)=1$, which is equivalent to $χ_S(α)≤χ_S(b)$. A subset
$S⊆P$ is non-open if it violates the condition associated to some
arrow $α→β$ --- which means that $α∈S$ but $β\not∈S$, or that
$χ_S(α)=1$ and $χ_S(b)$. Here is a graphical representation of
$χ_{\pile(43)}$:

%L write_dnt_file()
\pu
















%  ____       __                                   
% |  _ \ ___ / _| ___ _ __ ___ _ __   ___ ___  ___ 
% | |_) / _ \ |_ / _ \ '__/ _ \ '_ \ / __/ _ \/ __|
% |  _ <  __/  _|  __/ | |  __/ | | | (_|  __/\__ \
% |_| \_\___|_|  \___|_|  \___|_| |_|\___\___||___/
%                                                  
% «references»  (to ".references")
% (find-LATEX "catsem-u.bib" "bib-Johnstone")

% (find-es "tex" "compositionality")
% (find-es "tex" "compositionality" "thebibliography")
% (find-comptfile "compositionality-template.tex" "\\begin{thebibliography}")


\bibliographystyle{plain}
\begin{thebibliography}{9}

% (find-LATEX "catsem-u.bib" "bib-Goldblatt")
\bibitem{Goldblatt}
  Robert Goldblatt,
  \href{https://doi.org/10.22331/ idonotexist}{Topoi: The Categorial
    Analysis of Logic, North Holland, 1984.}

% (find-LATEX "catsem-u.bib" "bib-Johnstone")
\bibitem{Johnstone}
  Peter T. Johnstone,
  \href{https://doi.org/10.22331/ idonotexist}{Topos Theory, Academic
    Press, 1977.}

% (find-LATEX "catsem-u.bib" "bib-Johnstone" "Elephant1")
\bibitem{Elephant1}
  Peter T. Johnstone,
  \href{https://doi.org/10.22331/ idonotexist}{Sketches of an
    Elephant: A Topos Theory Compendium, vol.~1, Oxford University
    Press, 2002}.

% (find-LATEX "catsem-u.bib" "bib-Ochs")
% (find-TH "math-b" "zhas-for-children-2")
\bibitem{PH1}
  Eduardo Ochs,
  \href{http://angg.twu.net/math-b.html\#zhas-for-children-2}{Planar
    Heyting Algebras for Children (2017).}

\bibitem{PH1}
  Eduardo Ochs,
  \href{http://angg.twu.net/math-b.html\#zhas-for-children-2}{Planar
    Heyting Algebras for Children 2: Closure Operators (2018).}

\bibitem{examplecitation}
  Name Surname,
  \href{https://doi.org/10.22331/
        idonotexist}{Compositionality
        \textbf{123}, 123456 (1916).}

\bibitem{biblatexsubmittingtothearxiv}
  StackExchange discussion on
  \href{http://tex.stackexchange.com/questions/26990/biblatex-submitting-to-the-arxiv}{``Biblatex:
    submitting to the arXiv'' (2017-01-10)}

\bibitem{arxivpdfoutput}
  Help article published by the arXiv on
  \href{https://arxiv.org/help/submit_tex}{``Considerations for TeX
    Submissions'' (2017-01-10)}

\bibitem{howtogetdoilinksinbibliography}
  StackExchange discussion on
  \href{http://tex.stackexchange.com/questions/3802/how-to-get-doi-links-in-bibliography}{``How
    to get DOI links in bibliography'' (2016-11-18)}
  
\bibitem{automaticallyaddingdoifieldstoahandmadebibliography}
  StackExchange discussion on
  \href{http://tex.stackexchange.com/questions/6810/automatically-adding-doi-fields-to-a-hand-made-bibliography}{``Automatically
    adding DOI fields to a hand-made bibliography'' (2016-11-18)}

\end{thebibliography}








\end{document}



%
%L write_dnt_file()
% (find-fline "/tmp/o")
% (find-fline "/tmp/o" :end)
% (find-angg "LATEX/2019oxford-diags.dnt")
%\end{document}

\directlua{print "HELLO"}
$\tcg{(P,A)}
 \zha{O_A(P)}
$
\directlua{print "HELLO"}

\end{document}
























%L tdims = TCGDims {qrh=5, q=10, crh=3.5, h=20, v=7, crv=3.5}   -- \chi with scriptsize
%L tspec_PA  = TCGSpec.new("46; 11 22 34 45, 25")
%L tspec_PA :tcgq({tdef="pile(43)", meta="1pt p s"}, "h ap"):digits("1111", "111000"):output()
%
$$\pu
  \tcg{pile(43)}
$$

We see that it has an arrow $1→0$ at the position corresponding to the
arrow $3▁→▁4$, so $\pile(43)\not∈\Opens_A(P)$.

Due to the vertical arrows an intercolumn arrow $a▁→▁b$ in $A$ can
also be interpreted as a condition in another way. on piles









\end{document}



 (that turns out to be a Planar Heyting Algebra in the
sense of the sections 4 and 15 of [PH1]). There are several equivalent
ways to define this topology, and some of them are very visual. We
interpret each 


The top half shows a 2CG $(P,A)$ and its associated ZHA $H$.

This $H$ can be seen as the ``order topology'' $\Opens_A(P)$. We
define $\pile(a,b) := \{1▁,\dots,a▁, \; ▁1,\ldots,▁b\}$ --- note that
$P=\pile(4,6)$ and we write the characteristic function of a subset
$S⊆P$ as $χ_S$. So:
%
$$
  χ_{\pile(1,5)} =
  \psm{
      & 0 \\
      & 1 \\
    0 & 1 \\
    0 & 1 \\
    0 & 1 \\
    1 & 1 \\
  },
  \qquad
  χ_{\pile(2,5)} =
  \psm{
      & 0 \\
      & 1 \\
    0 & 1 \\
    0 & 1 \\
    1 & 1 \\
    1 & 1 \\
  }
$$
%

We say that $χ_S$ is {\sl nondecreasing in $A$} if for every arrow
$α→β$ in $A$ we have $χ_S(α)≤χ_S(β)$. 



 to denote characteristic
functions. The notation with `$χ$'s gives us a nice way to define the
order topology: a subset $S⊆P$ is open, i.e., $S∈\Opens_A(P)$, if all
the arrows in $A$ are ``nondecreasing in the characteristic
function''. For example, we have


The top half of the figure below shows a 2CG $(P,A)$ with
specification
%
$\left(4,6, \csm{
         4▁→▁5, \\
         3▁→▁4, \\
         2▁→▁2, \\
         1▁→▁1 \\
       },
       \csm{2▁←▁5}
  \right)
$
%
--- the four components of the specification are the height of the
left column, the height of the right column, the intercolumn arrows
going right, and the intercolumn arrows going left --- and its
associated Planar Heyting Algebra (``ZHA'')

Their central constructions can be represented formally as bijections.
There is a bijection between 2CGs and Planar Heyting Algebras
(``ZHAs''), and there is a bijection between 2CGs with question marks
and ZHAs with slashings. Figure 2 shows an example; we pronounce
`$\squigbijbody$' as ``is associated to''.

Formally, for every 2CG $(P,A)$ we can construct its order topology
$\Opens_A(P)$, that turns out to be a Planar Heyting Algebra (a
``ZHA''); and every ``set of questions marks'' $Q⊆P$ on a 2CG induces
a ``slashing'' on the ZHA $\Opens_A(P)$, which induces a J-operator
$J$ on the ZHA.



; the lower half of the
diagram adds a set of ``question mark points''











\newpage




% (ph1p 3 "positional")
% (ph1    "positional")














% (find-LATEXsh "dednat6load.lua -t 2019oxford-diags.tex")
% (find-LATEX "dednat6load.lua")


\end{document}

% Local Variables:
% coding: utf-8-unix
% End:
