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

% «.defs»			(to "defs")
% «.monics-in-Set^2»		(to "monics-in-Set^2")
% «.page-26-yoneda»		(to "page-26-yoneda")
% «.page-32-true-terminal»	(to "page-32-true-terminal")
% «.pages-35-36-Set^2»		(to "pages-35-36-Set^2")
% «.page-57-theorem-1»		(to "page-57-theorem-1")
% «.page-58-theorem-2»		(to "page-58-theorem-2")
% «.pages-58-59-theorem-2»	(to "pages-58-59-theorem-2")
% «.page-63-exercise-8»		(to "page-63-exercise-8")
% «.page-63-exercise-10»	(to "page-63-exercise-10")

\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{edrx21}               % (find-LATEX "edrx21.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[a6paper, landscape,
           %top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
            top=1.5cm, bottom=.25cm, left=0.5cm, right=0.5cm, 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")

\def\drafturl{http://angg.twu.net/LATEX/2021sgl.pdf}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}

\def\Nat     {\text{Nat}}
\def\phop    {{}^{\phantom{\op}}}
\def\Cop     {{\catC^\op}}
\def\SetsCop {\Sets^{\catC^\op}}
\def\hatC    {{\widehat\catC}}
\def\OXop    {\Opens(X)^\op}
\def\SetsOXop{\Sets^{\Opens(X)^\op}}
\def\univ    {\mathsf{univ}}
\def\Spaces  {\mathbf{Spaces}}
\def\Locales {\mathbf{Locales}}
\def\Frames  {\mathbf{Frames}}
\def\Top     {\mathbf{Top}}
\def\Bund    {\mathbf{Bund}}
\def\Loc     {\mathrm{Loc}}
\def\Ker     {\operatorname{Ker}}
\def\Pt      {\operatorname{pt}}
\def\Sh      {\operatorname{Sh}}
\def\PSh     {\operatorname{PSh}}
\def\acz     {\setlength{\arraycolsep}{0pt}}
\def\y       {\mathbf{y}}
\def\HomC    {\Hom_\catC}

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

\def\goneism{\text{$g_1$ is monic}}
\def\gtwoism{\text{$g_2$ is monic}}
\def\gonetwoism{\text{$(g_1,g_2)$ is monic}}

\def\incgr#1#2{\myvcenter{\includegraphics[#1]{#2}}}
\def\scale#1#2{\scalebox{#1}{$#2$}}

% (find-LATEX "2020clops-and-tops.tex" "defs")

\def\Incs     {\mathsf{Incs}}




% «monics-in-Set^2»  (to ".monics-in-Set^2")

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

Proposition: a morphism $g=(g_1,g_2)$ in $\Set^2$ is a monic

if and only if its two components, $g_1$ and $g_2$, are monics in $\Set$.

\msk

With the right abbreviations, this becomes:

$(\gonetwoism) ↔ (\goneism) ∧ (\gtwoism)$

\msk

We will use the diagrams below.

%D diagram ??
%D 2Dx     100  +30 +25  +50   +40  +30 +15  +30
%D 2D  100 A0 = A1  B0 = B1    C0 = C1  D0 = D1
%D 2D         \  |     \  |       \  |     \  |
%D 2D  +30      A2       B2         C2       D2
%D 2D
%D ren A0 A1 A2 ==> ∀A B C
%D ren B0 B1 B2 ==> ∀(A_1,A_2) (B_1,B_2) (C_1,C_2)
%D ren C0 C1 C2 ==> ∀A_1 B_1 C_1
%D ren D0 D1 D2 ==> ∀A_2 B_2 C_2
%D
%D (( A0 A1 -> sl^ .plabel= a ∀f
%D    A0 A1 -> sl_ .plabel= b ∀f'
%D    A0 A2 -> sl^
%D    A0 A2 -> sl_
%D    A1 A2 ->     .plabel= r g
%D ))
%D (( B0 B1 -> sl^ .plabel= a ∀(f_1,f_2)
%D    B0 B1 -> sl_ .plabel= b ∀(f'_1,f'_2)
%D    B0 B2 -> sl^
%D    B0 B2 -> sl_
%D    B1 B2 ->     .plabel= r (g_1,g_2)
%D ))
%D (( C0 C1 -> sl^ .plabel= a ∀f_1
%D    C0 C1 -> sl_ .plabel= b ∀f'_1
%D    C0 C2 -> sl^
%D    C0 C2 -> sl_
%D    C1 C2 ->     .plabel= r g_1
%D ))
%D (( D0 D1 -> sl^ .plabel= a ∀f_2
%D    D0 D1 -> sl_ .plabel= b ∀f'_2
%D    D0 D2 -> sl^
%D    D0 D2 -> sl_
%D    D1 D2 ->     .plabel= r g_2
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.8}{$
  \diag{??}
  $}
$$

\scalebox{0.58}{
\begin{tabular}{l}
  %
  [5pt]
  %
  Def: $B_1 \xton{g_1} C_1$ is a monic in $\Set$ \\
  means $\und{ ∀A_1.\, ∀f_1,f'_1.\,
               (\und{g_1∘f_1=g_1∘f'_1}{α_1} → \und{f_1=f'_1}{β_1})
             }{\text{``$g_1$ is monic''}}
        $ \\
  %
  [55pt]
  %
  Def: $B_2 \xton{g_2} C_2$ is a monic in $\Set$ \\
  means $\und{ ∀A_2.\, ∀f_2,f'_2.\,
               (\und{g_2∘f_2=g_2∘f'_2}{α_2} → \und{f_2=f'_2}{β_2})
             }{\text{``$g_2$ is monic''}}
        $ \\
  %
  [55pt]
  %
  Def: $B \xton{g} C$ is a monic in $\Set^2$, \\
  i.e, $(B_1,B_2) \xton{(g_1,g_2)} (C_1,C_2)$ is a monic in $\Set^2$, \\
  means $∀A.\, ∀f,f'.\, (\und{g∘f=g∘f'}{α} → \und{f=f'}{β})$, \\
  i.e., $∀(A_1,A_2).\, ∀(f_1,f_2),(f'_1,f'_2).\,
     (\und{(g_1,g_2)∘(f_1,f_2)=(g_1,g_2)∘(f'_1,f'_2)}{α_{12}=α}
     → \und{(f_1,f_2)=(f'_1,f'_2)}{β_{12}=β})$,
  \\
  [10pt]
  %
  i.e., $∀(A_1,A_2).\, ∀(f_1,f_2),(f'_1,f'_2).\,
     (\nound{(g_1∘f_1,g_2∘f_2)=(g_1∘f'_1,g_2∘f'_2)}{α_{12}=α}
     → \nound{(f_1,f_2)=(f'_1,f'_2)}{β_{12}=β})$,
  \\
  [5pt]
  %
  i.e., $\und{ ∀A_1,A_2.\, ∀f_1,f_2, f'_1,f'_2.\,
               ((\und{g_1∘f_1=g_1∘f'_1}{α_1}) ∧
                (\und{g_2∘f_2=g_2∘f'_2}{α_2}) →
                (\und{f_1=f'_1}{β_1}) ∧
                (\und{f_2=f'_2}{β_2}))
             }{\text{``$(g_1,g_2)$ is monic''}}
             $.
  \\
  [55pt]
  %
  We want to prove this: $(\gonetwoism) ↔ (\goneism) ∧ (\gtwoism)$
\end{tabular}
}



\newpage

Trick 1: make $f_1$ and $f'_1$ identities. We will need $A_1:=B_1$.

Trick 2: make $f_2$ and $f'_2$ identities. We will need $A_2:=B_2$.

\bsk
%D diagram tricks-1-and-2
%D 2Dx     100  +50    +70  +50
%D 2D  100 A0 = A1     B0 = B1 
%D 2D         \  |  =>    \  | 
%D 2D  +30      A2          B2 
%D 2D
%D 2D  +20 C0 = C1     D0 = D1
%D 2D         \  |  =>    \  |
%D 2D  +30      C2          D2
%D 2D
%D ren A0 A1 A2 ==> ∀(A_1,A_2) (B_1,B_2) (C_1,C_2)
%D ren B0 B1 B2 ==> (B_1,∀A_2) (B_1,B_2) (C_1,C_2)
%D ren C0 C1 C2 ==> ∀(A_1,A_2) (B_1,B_2) (C_1,C_2)
%D ren D0 D1 D2 ==> (∀A_1,B_2) (B_1,B_2) (C_1,C_2)
%D
%D (( A0 A1 -> sl^ .plabel= a ∀(f_1,f_2)
%D    A0 A1 -> sl_ .plabel= b ∀(f'_1,f'_2)
%D    A0 A2 -> sl^
%D    A0 A2 -> sl_
%D    A1 A2 ->     .plabel= r (g_1,g_2)
%D ))
%D (( B0 B1 -> sl^ .plabel= a (\id,∀f_2)
%D    B0 B1 -> sl_ .plabel= b (\id,∀f'_2)
%D    B0 B2 -> sl^
%D    B0 B2 -> sl_
%D    B1 B2 ->     .plabel= r (g_1,g_2)
%D ))
%D (( A0 B2 harrownodes nil 25 nil =>
%D      .plabel= a \sm{A_1:=B_1\;\;\\f_1:=\id_{B_1}\\f'_1:=\id_{B_1}}
%D ))
%D (( C0 C1 -> sl^ .plabel= a ∀(f_1,f_2)
%D    C0 C1 -> sl_ .plabel= b ∀(f'_1,f'_2)
%D    C0 C2 -> sl^
%D    C0 C2 -> sl_
%D    C1 C2 ->     .plabel= r (g_1,g_2)
%D ))
%D (( D0 D1 -> sl^ .plabel= a (∀f_1,\id)
%D    D0 D1 -> sl_ .plabel= b (∀f'_1,\id)
%D    D0 D2 -> sl^
%D    D0 D2 -> sl_
%D    D1 D2 ->     .plabel= r (g_1,g_2)
%D ))
%D (( C0 D2 harrownodes nil 25 nil =>
%D      .plabel= a \sm{A_2:=B_2\;\;\\f_2:=\id_{B_2}\\f'_2:=\id_{B_2}}
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.8}{$
  \diag{tricks-1-and-2}
  $}
$$


\newpage

If we specialize ``$\gonetwoism$''

by doing $A_1:=B_1$, $f_1:=\id$, $f'_1:=\id$,

we get this:
%
%UB ∀A_1,A_2.\, ∀f_1,f_2, f'_1,f'_2.\, (g_1∘f_1=g_1∘f'_1)∧(g_2∘f_2=g_2∘f'_2)→(f_1=f'_1)∧(f_2=f'_2)
%UB  ---         ---      ----              ---     ----   ----------------   --- ----   --------
%UB  B_1         \id      \id               \id     \id          α_2          \id \id      β_2
%UB                                     ------- --------                      --------
%UB                                       g_1     g_1                          \True
%UB                                     ----------------                      --------------------
%UB                                          \True                                   β_2
%UB                                     ------------------------------------
%UB                                                  α_2
%UB ----------------------------------------------------------------------------------------------
%UB    ∀A_2.\, ∀f_2,f'_2.\, α_2→β_2
%UB ----------------------------------------------------------------------------------------------
%UB    \gtwoism
%L
%L defub "trick 1"
%L
$$\pu
 \scale{0.7}{
 \ub{trick 1}
 }
$$

so $(\gonetwoism) → (\gtwoism)$.

The proof of $(\gonetwoism) → (\goneism)$ is similar,

but with $A_2:=B_2$, $f_2:=\id$, $f'_2:=\id$.

So: $(\gonetwoism) → (\goneism) ∧ (\gtwoism)$.



\newpage

This is a proof of

$(\gonetwoism) ← (\goneism) ∧ (\gtwoism)$

in Natural Deduction:

%:
%: [α_1∧α_2]^1  [A_1,f_1,f'_1]^2  \goneism    [α_1∧α_2]^1  [A_2,f_2,f'_2]^2  \gtwoism
%: -----------  ---------------------------   -----------  --------------------------
%:         α_1  α_1→β_1                           α_1        α_2→β_2
%:         ------------                           ------------------
%:               β_1                                 β_2
%:               ---------------------------------------
%:                   β_1∧β_2
%:              ---------------1
%:              α_1∧α_2→β_1∧β_2
%:  ----------------------------------------------2
%:  ∀A_1,A_2,f_1,f_2,f'_1,f'_2.\,(α_1∧α_2→β_1∧β_2)
%:  ----------------------------------------------
%:       \gonetwoism
%:
%:       ^foo
%:
\pu
$$\scale{0.9}{
  \ded{foo}
  }
$$


\newpage


%  ____                    ____   __   
% |  _ \ __ _  __ _  ___  |___ \ / /_  
% | |_) / _` |/ _` |/ _ \   __) | '_ \ 
% |  __/ (_| | (_| |  __/  / __/| (_) |
% |_|   \__,_|\__, |\___| |_____|\___/ 
%             |___/                    
%
% «page-26-yoneda»  (to ".page-26-yoneda")
% (sglp 6 "page-26-yoneda")
% (sgla   "page-26-yoneda")
% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijk-links (+ 11 26) "This makes y into a functor")
% (find-fline "~/LATEX/2021sgl/" "p026-y")

%D diagram p26-b
%D 2Dx     100  +30 +35    +35  +40 +30 +15  +20
%D 2D  100 A0 - A1  C0     D0 - D1  F0  G0 - G1
%D 2D      |     |   |     |     |   |  |  /
%D 2D  +20 A2 - A3  C1     D2 - D3  F1  G2
%D 2D
%D 2D  +12 B0              E0
%D 2D  +8  B1 - B2         E1 - E2
%D 2D
%D ren A0 A1 A2 A3 ==> D \y(C)(D) D' \y(C)(D')
%D ren B0 B1 B2    ==> \catC \phop\catC^\op \Set
%D ren C0 C1       ==> u \y(C)(α)(u)
%D
%D ren D0 D1 D2 D3 ==> D \HomC(D,C) D' \HomC(D',C)
%D ren E0 E1 E2    ==> \catC \phop\catC^\op \Set
%D ren F0 F1       ==> u u∘α
%D ren G0 G1 G2    ==> D C D'
%D
%D (( A0 A1 |->
%D    A0 A2 <-  .plabel= l α
%D    A1 A3  -> .plabel= r \y(C)(α)
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 place
%D    B1 B2  -> .plabel= a \y(C)
%D    C0 C1 |->
%D ))
%D (( D0 D1 |->
%D    D0 D2 <-  .plabel= l α
%D    D1 D3  -> .plabel= r (∘α)
%D    D2 D3 |->
%D    D0 D3 harrownodes nil 20 nil |->
%D    E0 place
%D    E1 E2  -> .plabel= a \HomC(-,C)
%D    F0 F1 |->
%D    G0 G1  -> .plabel= a u
%D    G0 G2 <-  .plabel= l α
%D    G2 G1  -> .plabel= r u∘α
%D ))
%D enddiagram
%D
%D diagram p26-yoneda
%D 2Dx     100  +45  +50 +30 +30
%D 2D  100      A1 
%D 2D            | 
%D 2D  +20 A2 - A3   E0  F0  G0
%D 2D      |     |    |   |   |
%D 2D  +20 A4 - A5    |   |   |
%D 2D                 |   |   |
%D 2D  +20 B0 - B1    |   |   |
%D 2D                 |   |   |
%D 2D  +15 C0 - C1    |   |   |
%D 2D         \  |    |   |   |
%D 2D  +20      C2    |   |   |
%D 2D                 |   |   |
%D 2D  +15 D0 - D1   E1  F1  G1
%D 2D         \  |  
%D 2D  +20      D2 
%D 2D
%D 2D  +20
%D 2D
%D ren A1 A2 A3 A4 A5 ==> 1 C PC D PD
%D ren B0 B1    ==> \phop\catC^\op \Set
%D ren C0 C1 C2 ==> \Hom_\catC(D,C) \Hom(1,PD) PD
%D ren D0 D1 D2 ==> \Hom_\catC(-,C) \Hom(1,P-) P
%D ren E0 E1    ==> PC \Hom_\hatC(\y(C),P)
%D ren F0 F1    ==> α_C(1_C) α
%D ren G0 G1    ==> e λD.λu.Pu∘\nameof{e}
%D
%D (( A1 A3  -> .plabel= r \nameof{e} # \sm{\nameof{θ(α)}=\\\nameof{α_C(1_C)}}
%D    A2 A3 |->
%D    A2 A4 <-  .plabel= l u
%D    A3 A5  -> .plabel= r Pu
%D    A1 A5  -> .slide= 20pt .plabel= r \sm{Pu∘\nameof{e}=\\\nameof{(Pu)(e)}}
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D     B0 relplace 0 -8 \catC
%D    B0 B1  -> .plabel= a P
%D    C0 C1  ->
%D    C1 C2 <->
%D    C0 C2  -> .plabel= b λu.(Pu)(e)\;\;
%D     C0 relplace -38 0 \y(C)(D)=
%D    D0 D1  ->
%D    D1 D2 <->
%D    D0 D2  -> .plabel= b α
%D     D0 relplace -35 0 \y(C)=
%D    E0 E1 <-| sl_ .plabel= l θ
%D    E0 E1 |-> sl^ .plabel= r θ^{-1}
%D    F0 F1 <-|
%D    G0 G1 |->
%D ))
%D enddiagram
%D
\pu

  


% (favp 35 "yoneda-lemma")
% (fava    "yoneda-lemma")


\ColorBrown{\tiny Page 26:}

\msk

$
  % (find-maclanemoerdijk-links (+ 11 26) "This makes y into a functor")
  % (find-pdf-page "~/LATEX/2021sgl/p026-y.pdf")
  \incgr {height=5.5cm}    {2021sgl/p026-y.pdf}
  \quad
  \scalebox{0.45}{$
    \begin{array}{l}
      \diag{p26-b}      \\[50pt]
      \diag{p26-yoneda} \\
    \end{array}
  $}
$

\newpage

%  ____                    _________  
% |  _ \ __ _  __ _  ___  |___ /___ \ 
% | |_) / _` |/ _` |/ _ \   |_ \ __) |
% |  __/ (_| | (_| |  __/  ___) / __/ 
% |_|   \__,_|\__, |\___| |____/_____|
%             |___/                   
%
% «page-32-true-terminal»  (to ".page-32-true-terminal")
% (sglp 7 "page-32-true-terminal")
% (sgla   "page-32-true-terminal")

\ColorBrown{\tiny Page 32:}
%
\def\rito{\rotatebox[origin=c]{270}{$\ito$}}                     % \ito rotated right
\def\rmon{\rotatebox[origin=c]{270}{$\monicto$}}                 % \monic rotated right
\def\aninc#1#2#3#4{\pmat{#1 \\ #2 \rito #3 \\ #4}}               % an inclusion
\def\amon #1#2#3#4{\pmat{#1 \\ #2 \rmon #3 \\ #4}}               % a  monic
\def\inctrue{{\aninc {1\ph{mm}}  {}{\,\text{true}} {Ω\ph{mm} }}} % true: 1 \ito Ω
\def\montrue{{\amon  {1\ph{mm,}} {}{\,\text{true}} {Ω\ph{mm,}}}} % true: 1 \ito Ω
\def\incSX  {{\aninc {S}  {}{} {X}}}                             %  S \ito      X
\def\monSX  {{\amon  {S}  {}{} {X}}}                             %  S \monicto  X
\def\incSY  {{\aninc {S'} {}{} {Y}}}                             %  S' \ito     Y
\def\monSY  {{\amon  {S'} {}{} {Y}}}                             %  S' \monicto Y
%
%$\inctrue
% \montrue
% \incSX
% \monSX
% \incSY
% \monSY
%$
%
%D diagram p32-1-monics
%D 2Dx     100  +45
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +25 A2 - A3
%D 2D
%D 2D  +25 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 ==> ∀S 1 ∀X Ω
%D ren B0 B1       ==> ∀\monSX \montrue
%D
%D (( A0 A1  -> .plabel= a ϕ'=!
%D    A0 A2 >-> .plabel= l ∀
%D    A1 A3 >-> .plabel= r \text{true}
%D    A2 A3  -> .plabel= a ϕ
%D    A0 relplace 7 7 \pbsymbol{7}
%D    B0 B1 -> .plabel= a ∃!\psm{ϕ'\\ϕ}
%D ))
%D enddiagram
%D
%D diagram p32-1-inclusions
%D 2Dx     100  +45
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +25 A2 - A3
%D 2D
%D 2D  +25 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 ==> ∀S 1 ∀X Ω
%D ren B0 B1       ==> ∀\incSX \inctrue
%D
%D (( A0 A1  -> .plabel= a ϕ'=!
%D    A0 A2 `-> .plabel= l ∀
%D    A1 A3 `-> .plabel= r \text{true}
%D    A2 A3  -> .plabel= a ϕ
%D    A0 relplace 7 7 \pbsymbol{7}
%D    B0 B1 -> .plabel= a ∃!\psm{ϕ'\\ϕ}
%D ))
%D enddiagram
%D
\pu
%$$\diag{p32-1-monics}
%  \quad
%  \diag{p32-1-inclusions}
%$$
%
%D diagram p32-2-monics
%D 2Dx     100  +50  +25
%D 2D  100 A0 - A1 - A2
%D 2D      |    |     |
%D 2D  +20 A3 - A4 - A5
%D 2D
%D 2D  +20 B0 - B1
%D 2D
%D 2D  +20 C0 - C1
%D 2D      |     |
%D 2D  +20 C2 - C3
%D 2D
%D ren A0 A1 A2 ==> S' S 1
%D ren A3 A4 A5 ==> Y  X Ω
%D ren B0 B1    ==> \monSY \monSX
%D ren C0 C1 C2 C3 ==> \Sub_\catC(Y) \Sub_\catC(X) Y X
%D
%D (( A0 A1 -> A1 A2 ->
%D    A0 A3 -> .plabel= l m'
%D    A1 A4 -> .plabel= l m
%D    A2 A5 -> .plabel= r \text{true}
%D    A3 A4 -> .plabel= a f
%D    A4 A5 ->
%D    A0 relplace 7 7 \pbsymbol{7}
%D    A1 relplace 7 7 \pbsymbol{7}
%D    B0 B1 <-|
%D    C0 C1 <-  .plabel= a \Sub_\catC(f)
%D    C0 C2 <-|
%D    C1 C3 <-|
%D    C2 C3  -> .plabel= b f
%D    C0 C3 varrownodes nil 15 nil <-|
%D ))
%D enddiagram
%D
\pu
%$$\diag{p32-2-monics}
%$$
%
%D diagram p32-3-monics
%D 2Dx     100  +30 +30
%D 2D  100 A0 - A1  C0 
%D 2D      |     |   |
%D 2D  +30 A2 - A3  C1
%D 2D
%D 2D  +20 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 ==> X \Sub_\catC(X) Y \Sub_\catC(Y)
%D ren B0 B1       ==> \catC^\op \Set
%D ren C0 C1       ==> \scale{0.7}{\monSX} \scale{0.7}{\monSY}
%D
%D (( A0 A1 |->
%D    A0 A2 <-  .plabel= l f
%D    A1 A3  -> .plabel= r \Sub_\catC(f)
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 B1  -> .plabel= a \Sub_\catC
%D    newnode: B0' at: @B0+v(-2.5,-7) .TeX= \catC place
%D    C0 C1 |->
%D
%D ))
%D enddiagram
%D
\pu
%$$\diag{p32-3-monics}
%$$


% (find-maclanemoerdijk-links (+ 11 32) "Definition... subobject classifier" "-sc")

$% (find-pdf-page "~/LATEX/2021sgl/p032-sc.pdf")
  \incgr{height=6cm}{2021sgl/p032-sc.pdf}
  \quad
  \scale{0.45}{
  \begin{array}{l}
    \begin{tabular}{l}
      In the category of \\
      monic and pullbacks, \\
    \end{tabular}
    \\
    \diag{p32-1-monics} \\
    \\
    \begin{tabular}{l}
      and $ϕ'=!$, so $∃!ϕ$. \\
      $\scale{0.5}{\monSX}$ is an element of $\Sub_\catC(X)$. \\
      $\scale{0.5}{\monSX}$ is an equivalence class, \\
      and may not be a set. \\
    \end{tabular}
    \\
    \\
    \diag{p32-2-monics} \quad
    \diag{p32-3-monics} \\
  \end{array}
  }
$


\newpage

%  ____                         _________    _______  __   
% |  _ \ __ _  __ _  ___  ___  |___ / ___|  / /___ / / /_  
% | |_) / _` |/ _` |/ _ \/ __|   |_ \___ \ / /  |_ \| '_ \ 
% |  __/ (_| | (_| |  __/\__ \  ___) |__) / /  ___) | (_) |
% |_|   \__,_|\__, |\___||___/ |____/____/_/  |____/ \___/ 
%             |___/                                        
%
% «pages-35-36-Set^2»  (to ".pages-35-36-Set^2")
% (sglp 8 "pages-35-36-Set^2")
% (sgla   "pages-35-36-Set^2")

\ColorBrown{\tiny Pages 35 and 36:}

\msk


\def\monSSXX{{\amon {\ph{mi}(S,S')}
                      {(⊂,⊂)}{\ph{mi}}
                    {\ph{mi}(X,X')}}}
\def\montt  {{\amon  {(1,1)\ph{m}}
                    {\ph{m}}{\,\text{true}}
                     {(1,2)\ph{m}}}}

% $\monSSXX \montt$

%D diagram p35-SxS
%D 2Dx     100 +10  +30  +35  +40  +40  +55
%D 2D  100 A0  A1   B0   C0 - C1
%D 2D  +10  |  |    |    |     |   D0 - D1
%D 2D  +10 A2  A3   B1   C2 - C3
%D 2D
%D 2D  +20 A4  A5   B2
%D 2D
%D ren A0 A1 A2 A3 ==>  Y Y'   X X'
%D ren B0 B1 B2    ==> (Y,Y') (X,Y') \Sets×\Sets
%D ren C0 C1 C2 C3 ==> ∀(S,S') (1,1) ∀(X,X') (2,2)
%D ren D0 D1       ==> ∀\monSSXX \montt
%D
%D (( A0 A2  -> .plabel= l f
%D    A1 A3  -> .plabel= r f'
%D    A4 A5 midpoint .TeX= \Sets place
%D    B0 B1  -> .plabel= r (f,f')
%D    B2 place
%D    C0 C1  -> .plabel= a !
%D    C0 C2 >-> .plabel= l ∀(⊂,⊂)
%D    C1 C3 >-> .plabel= r \text{true}
%D    C2 C3  -> .plabel= b (ϕ_S,ϕ_{S'})
%D    C0 relplace 12 7 \pbsymbol{7}
%D    D0 D1  -> .plabel= a ∃!
%D ))
%D enddiagram
%D
\pu
%
\def\rS  {(S_0 \ton{σ} S_1)}
\def\rX  {(X_0 \ton{σ} X_1)}
\def\rone{(\{0\} \ton{σ} \{0\})}
\def\rOm {(\{0,1,2\} \xton{σ = \csm{0↦0 \\ 1↦0 \\ 2↦1}} \{0,1\})}
\def\rmyone{(\{11\} \ton{σ} \{·1\})}
\def\rmyOm {(\{11,01,00\} \xton{σ = \csm{11↦·1 \\ 01↦·1 \\ 00↦·0}} \{·1,·0\})}
%
%D diagram p35-2
%D 2Dx     100  +80
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +40 A2 - A3
%D 2D
%D ren A0 A1 A2 A3 ==> \rS \rone \rX \rOm
%D
%D (( A0 A1  -> .plabel= a !
%D    A0 A2 >-> .plabel= l (⊂,⊂)
%D    A1 A3 >-> .plabel= r (⊂,⊂)
%D    A2 A3  -> .plabel= b (ϕ_0,ϕ_1)
%D    A0 relplace 15 8 \pbsymbol{7}
%D    newnode: A0' at: @A0+v(-25,0) .TeX= S= place
%D ))
%D enddiagram
%D
%D diagram p35-2-my
%D 2Dx     100  +80
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +40 A2 - A3
%D 2D
%D ren A0 A1 A2 A3 ==> \rS \rmyone \rX \rmyOm
%D
%D (( A0 A1  -> .plabel= a !
%D    A0 A2 >-> .plabel= l (⊂,⊂)
%D    A1 A3 >-> .plabel= r (⊂,⊂)
%D    A2 A3  -> .plabel= b (ψ_0,ψ_1)
%D    A0 relplace 15 8 \pbsymbol{7}
%D    newnode: A0' at: @A0+v(-25,0) .TeX= S= place
%D ))
%D enddiagram
%D
\pu

$ % (find-maclanemoerdijk-links (+ 11 35) "For the arrow category 2 and Sets^2" "-SxS")
  % (find-maclanemoerdijk-links (+ 11 35) "For the arrow category 2 and Sets^2" "-S2")
  % (find-maclanemoerdijk-links (+ 11 36) "For the arrow category 2 and Sets^2" "-S2")
  % (find-pdf-page "~/LATEX/2021sgl/p035-SxS.pdf")
  % (find-pdf-page "~/LATEX/2021sgl/p035-S2.pdf")
  % (find-pdf-page "~/LATEX/2021sgl/p036-S2.pdf")
  \begin{array}{c}
    \incgr{width=6cm}{2021sgl/p035-SxS.pdf} \\
    \incgr{width=6cm}{2021sgl/p035-S2.pdf} \\
    \incgr{width=6cm}{2021sgl/p036-S2.pdf} \\
  \end{array}
  \quad
  \begin{array}{l}
    \scale{0.4}{\diag{p35-SxS}}  \\ \\
    \scale{0.4}{\diag{p35-2}}    \\[20pt]
    \scale{0.4}{\diag{p35-2-my}} \\[20pt]
    \scale{0.4}{
      \begin{array}{cccccc}
        x∈S_0  & σx∈S_1 & ϕ_0x & ϕ_1(σx) & ψ_0x & ψ_1(σx) \\ \hline
        \True  & \True  & 0    & 0       & 11   & ·1 \\
        \False & \True  & 1    & 0       & 01   & ·1 \\
        \False & \False & 2    & 1       & 00   & ·0 \\
      \end{array}
    }
  \end{array}
$

\msk

{\tiny

\ColorBrown{See:}
%
% (cltp 29 "SetD-chi")
% (clta    "SetD-chi")

%    http://angg.twu.net/LATEX/2020clops-and-tops.pdf#page=29
\url{http://angg.twu.net/LATEX/2020clops-and-tops.pdf#page=29}

}



\newpage

%  ____                    ____ _____   _   _                 _ 
% |  _ \ __ _  __ _  ___  | ___|___  | | |_| |__  _ __ ___   / |
% | |_) / _` |/ _` |/ _ \ |___ \  / /  | __| '_ \| '_ ` _ \  | |
% |  __/ (_| | (_| |  __/  ___) |/ /   | |_| | | | | | | | | | |
% |_|   \__,_|\__, |\___| |____//_/     \__|_| |_|_| |_| |_| |_|
%             |___/                                             
%
% «page-57-theorem-1»  (to ".page-57-theorem-1")
% (find-maclanemoerdijkpage (+ 11 57) "9. Quantifiers as Adjoints")
% (find-maclanemoerdijk-links (+ 11 57) "9. Quantifiers as Adjoints" "-thm-1")
% (hypp 18 "quants-for-children")
% (hyp     "quants-for-children")

\ColorBrown{\tiny Page 57, theorem 1:}

$% (find-pdf-page "~/LATEX/2021sgl/p057-thm-1.pdf")
  \incgr{width=5cm}{2021sgl/p057-thm-1.pdf}
$

%  ____                    ____   ___    _   _                 ____  
% |  _ \ __ _  __ _  ___  | ___| ( _ )  | |_| |__  _ __ ___   |___ \ 
% | |_) / _` |/ _` |/ _ \ |___ \ / _ \  | __| '_ \| '_ ` _ \    __) |
% |  __/ (_| | (_| |  __/  ___) | (_) | | |_| | | | | | | | |  / __/ 
% |_|   \__,_|\__, |\___| |____/ \___/   \__|_| |_|_| |_| |_| |_____|
%             |___/                                                  
%
% «page-58-theorem-2»  (to ".page-58-theorem-2")
% (find-maclanemoerdijkpage (+ 11 58) "9. Quantifiers as Adjoints" "-thm-2")

% «pages-58-59-theorem-2»  (to ".pages-58-59-theorem-2")
% (find-maclanemoerdijkpage (+ 11 58) "9. Quantifiers as Adjoints" "-thm-3")


\newpage

%  ____                     __    ___                 ___  
% |  _ \ __ _  __ _  ___   / /_  ( _ )    _____  __  ( _ ) 
% | |_) / _` |/ _` |/ _ \ | '_ \ / _ \   / _ \ \/ /  / _ \ 
% |  __/ (_| | (_| |  __/ | (_) | (_) | |  __/>  <  | (_) |
% |_|   \__,_|\__, |\___|  \___/ \___/   \___/_/\_\  \___/ 
%             |___/                                        
% «page-63-exercise-8»  (to ".page-63-exercise-8")
% (sglp 9 "page-63-exercise-8")
% (sgla   "page-63-exercise-8")
% (find-maclanemoerdijk-links (+ 11 63) "Exercise 8" "-exercise-8")
% https://categorytheory.zulipchat.com/#narrow/stream/300905-SGL-Reading.20Group/topic/stream.20events/near/257669027
% https://ncatlab.org/nlab/show/category+of+presheaves
% (code-pdf-page "swarajch1ex8" "~/SGL/sgl-swaraj-ch1ex8.pdf")
% (find-swarajch1ex8page)

\ColorBrown{\tiny Page 63, exercise 8:}

\msk

$% (find-pdf-page "~/LATEX/2021sgl/p063-exercise-8.pdf")
  \incgr{width=5.5cm}{2021sgl/p063-exercise-8.pdf}
$

\msk

%  ____                     __  _____               _  ___  
% |  _ \ __ _  __ _  ___   / /_|___ /    _____  __ / |/ _ \ 
% | |_) / _` |/ _` |/ _ \ | '_ \ |_ \   / _ \ \/ / | | | | |
% |  __/ (_| | (_| |  __/ | (_) |__) | |  __/>  <  | | |_| |
% |_|   \__,_|\__, |\___|  \___/____/   \___/_/\_\ |_|\___/ 
%             |___/                                         
%
% «page-63-exercise-10»  (to ".page-63-exercise-10")
% (sglp 9 "page-63-exercise-10")
% (sgla   "page-63-exercise-10")
% (find-maclanemoerdijk-links (+ 11 63) "Exercise 10" "-exercise-10")

\ColorBrown{\tiny Page 63, exercise 10:}

\msk

$% (find-pdf-page "~/LATEX/2021sgl/p063-exercise-10.pdf")
  \incgr{width=6cm}{2021sgl/p063-exercise-10.pdf}
$




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

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