% (find-LATEX "2020on-a-broken-dnc.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020on-a-broken-dnc.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2020on-a-broken-dnc.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020on-a-broken-dnc.pdf"))
% (defun e () (interactive) (find-LATEX "2020on-a-broken-dnc.tex"))
% (defun b () (interactive) (find-LATEX "2020on-a-broken-dnc.bib"))
% (defun u () (interactive) (find-latex-upload-links "2020on-a-broken-dnc"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020on-a-broken-dnc.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020on-a-broken-dnc.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020on-a-broken-dnc.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020on-a-broken-dnc.pdf
%               file:///tmp/2020on-a-broken-dnc.pdf
%           file:///tmp/pen/2020on-a-broken-dnc.pdf
% http://angg.twu.net/LATEX/2020on-a-broken-dnc.pdf
% (find-LATEX "2019.mk")

% «.title»			(to "title")
% «.freyd»			(to "freyd")
% «.variants»			(to "variants")
% «.pullbacks»			(to "pullbacks")
% «.formalizing-pullback»	(to "formalizing-pullback")
% «.propositions-as-types»	(to "propositions-as-types")
% «.my-variant»			(to "my-variant")
% «.nd-dep-types»		(to "nd-dep-types")
% «.make»			(to "make")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb}                 % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\usepackage[backend=biber,
   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
%\addbibresource{catsem-u.bib}            % (find-LATEX "catsem-u.bib")
\addbibresource{2020on-a-broken-dnc.bib}  % (find-LATEX "catsem-u.bib")
%
% (find-es "tex" "geometry")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu


%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title»  (to ".title")

\title{On a (broken) system of Natural Deduction for Categories}
\author{Eduardo Ochs}
\maketitle







One of the things that I intended to do in my PhD thesis was to
formalize a certain system of Natural Deduction for Categories that I
was using quite happily at the time as a mathematical hack, even
though I only had some of its rules --- for example, it had rules with
discharges, similar to the $({→}I)$ of Natural Deduction, that could
be used to define functors and natural transformations...

That system --- I called it ``System DNC'', for ``Dedução Natural para
Categorias'', in Portuguese --- turned out to be too hard to
formalize, and it ended up as a secondary theme in the thesis. It took
me several years more to see how System DNC could be used in a formal
way even if it was incompletely defined; the paper \cite{IDARCT}
is about that.

What I am going to present in these notes is a much better version of
DNC than the one that is sketched (briefly!) in \cite{IDARCT}. Here we
will replace the ``downcased types'' of Section 3 of the paper by some
ideas taken from the ``Logic for Children'' project (\cite{PH1},
\cite{LFC2018}) --- namely, that we can use



%  _____                   _ 
% |  ___| __ ___ _   _  __| |
% | |_ | '__/ _ \ | | |/ _` |
% |  _|| | |  __/ |_| | (_| |
% |_|  |_|  \___|\__, |\__,_|
%                |___/       
%
% «freyd»  (to ".freyd")
% (dnop 2 "freyd")
% (dno    "freyd")

\section{Freyd's diagrammatic language}

When I started learning Category Theory the library of my university
had very few books on that subject. One of them was a collection of papers
in honour of Sammy Eilenberg that contained a paper by Peter Freyd
called ``Properties Invariant within Equivalence Types of Categories''
(\cite{Freyd76}), that presented a diagrammatic language for
statements in CT; I found it absolutely fascinating. There's a scanned
copy of it here:

\msk

\url{http://angg.twu.net/scans/freyd76__properties_invariant_within_equivalence_types_of_categories.pdf}

\msk

Its diagrammatic language later became the basis for Freyd's book with
Scedrov, ``Categories, Allegories'' (\cite{FreydScedrov}). Let me show
briefly how that language works. This is the statement that a category
has equalizers:
%
%L forths["-"] = function () pusharrow("-") end
%
%D diagram cat-has-equalizers
%D 2Dx     100 +00   +15   +20 +15 +15   +20   +20 +15 +15   +20   +20 +15 +15   +20   +20
%D 2D  100 U0                  U1                  U2                  U3                 
%D 2D       |                   |                   |                   |                 
%D 2D  +10  |  A0               |  B0               |  C0               |  D0             
%D 2D       |  |  \             |  |  \             |  |  \             |  |  \           
%D 2D  +20  |  A1 -- A2 == A3   |  B1 -- B2 == B3   |  C1 -- C2 == C3   |  D1 -- D2 == D3 
%D 2D       |                   |                   |                   |                 
%D 2D  +20 L0                  L1                  L2                  L3                 
%D 2D
%D ren U0 L0 A0 A1 A2 A3 ==> ∀  {} X E A B
%D ren U1 L1 B0 B1 B2 B3 ==> ∃  {} X E A B
%D ren U2 L2 C0 C1 C2 C3 ==> ∀  {} X E A B
%D ren U3 L3 D0 D1 D2 D3 ==> ∃! {} X E A B
%D
%D (( U0 L0 -
%D    A2 A3 -> sl^^ .plabel= a f
%D    A2 A3 -> sl__ .plabel= b g
%D    A2 A3 midpoint .TeX= * place
%D ))
%D (( U1 L1 -
%D    B2 B3 -> sl^^ .plabel= a f
%D    B2 B3 -> sl__ .plabel= b g
%D    B2 B3 midpoint .TeX= * place
%D    B1 B2 -> .plabel= b e
%D ))
%D (( U2 L2 -
%D    C2 C3 -> sl^^ .plabel= a f
%D    C2 C3 -> sl__ .plabel= b g
%D    C2 C3 midpoint .TeX= * place
%D    C1 C2 -> .plabel= b e
%D    C0 C2 -> .plabel= r h
%D ))
%D (( U3 L3 -
%D    D2 D3 -> sl^^ .plabel= a f
%D    D2 D3 -> sl__ .plabel= b g
%D    D2 D3 midpoint .TeX= * place
%D    D1 D2 -> .plabel= b e
%D    D0 D2 -> .plabel= r h
%D    D0 D1 -> .plabel= l k
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.8}{$
  \diag{cat-has-equalizers}
  $}
$$

It means: for all diagrams of the shape [first subdiagram] in our
category there exists an extension of it to [second subdiagram] such
that for all extensions of it to [third subdiagram] there exists a
unique extension of it to [fourth subdiagram].

% (find-books "__cats/__cats.el" "freyd76")
% (find-books "__cats/__cats.el" "freyd-scedrov")

More formally (see \cite[p.28 onwards]{Freyd76}):

\msk

For all $f,g$ such that $□f=□g$, $f□=g□$,

there exists $e$ such that $e□=□f$, $ef=eg$, such that

for all $h$ such that $h□=e□$,

there exists a unique $h$ such that $□k=□h$, $k□=□e$, $ke=e$.

\msk

The default is for all cells to commute; non-commuting cells are
marked with a `$*$'. After the first few diagrams in the book the
objects are morphism stop being named, and the diagrams become like
this:
%
%D diagram cat-has-equalizers-2
%D 2Dx     100 +00   +15   +20 +15 +15   +20   +20 +15 +15   +20   +20 +15 +15   +20   +20
%D 2D  100 U0                  U1                  U2                  U3                 
%D 2D       |                   |                   |                   |                 
%D 2D  +10  |  A0               |  B0               |  C0               |  D0             
%D 2D       |  |  \             |  |  \             |  |  \             |  |  \           
%D 2D  +20  |  A1 -- A2 == A3   |  B1 -- B2 == B3   |  C1 -- C2 == C3   |  D1 -- D2 == D3 
%D 2D       |                   |                   |                   |                 
%D 2D  +20 L0                  L1                  L2                  L3                 
%D 2D
%D ren U0 L0 A0 A1 A2 A3 ==> ∀  {} • • • •
%D ren U1 L1 B0 B1 B2 B3 ==> ∃  {} • • • •
%D ren U2 L2 C0 C1 C2 C3 ==> ∀  {} • • • •
%D ren U3 L3 D0 D1 D2 D3 ==> ∃! {} • • • •
%D
%D (( U0 L0 -
%D    A2 A3 -> sl^^ # .plabel= a f
%D    A2 A3 -> sl__ # .plabel= b g
%D    A2 A3 midpoint .TeX= * place
%D ))
%D (( U1 L1 -
%D    B2 B3 -> sl^^ # .plabel= a f
%D    B2 B3 -> sl__ # .plabel= b g
%D    B2 B3 midpoint .TeX= * place
%D    B1 B2 -> # .plabel= b e
%D ))
%D (( U2 L2 -
%D    C2 C3 -> sl^^ # .plabel= a f
%D    C2 C3 -> sl__ # .plabel= b g
%D    C2 C3 midpoint .TeX= * place
%D    C1 C2 -> # .plabel= b e
%D    C0 C2 -> # .plabel= r h
%D ))
%D (( U3 L3 -
%D    D2 D3 -> sl^^ # .plabel= a f
%D    D2 D3 -> sl__ # .plabel= b g
%D    D2 D3 midpoint .TeX= * place
%D    D1 D2 -> # .plabel= b e
%D    D0 D2 -> # .plabel= r h
%D    D0 D1 -> # .plabel= l k
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.8}{$
  \diag{cat-has-equalizers-2}
  $}
$$
%
and gradually several kinds of arrows and other symbols are
introduced, to mean ``this arrow is monic'', ``this arrow is epi'',
``this square is a pullack'' and so on.


% __     __         _             _       
% \ \   / /_ _ _ __(_) __ _ _ __ | |_ ___ 
%  \ \ / / _` | '__| |/ _` | '_ \| __/ __|
%   \ V / (_| | |  | | (_| | | | | |_\__ \
%    \_/ \__,_|_|  |_|\__,_|_| |_|\__|___/
%                                         
% «variants»  (to ".variants")
% (dnop 3 "variants")
% (dno     "variants")

\subsection{Variants of Freyd's language}

I started to use variants of these diagrams to study MacLane's
\cite{CWM} (that I found {\sl very} hard). To reduce redundancy, I
experimented with several ways to indicate in which stage each new
entity is introduced. For example, this:
%
%D diagram equalizer-big-1
%D 2Dx     100   +20   +20
%D 2D  100 A0             
%D 2D      |  \           
%D 2D  +20 A1 -- A2 == A3 
%D 2D
%D ren A0 A1 A2 A3 ==> X E A B
%D ren A0 A1 A2 A3 ==> • • • •
%D
%D (( A2 A3 -> sl^^ # .plabel= a f
%D    A2 A3 -> sl__ # .plabel= b g
%D    A2 A3 midpoint .TeX= * place
%D    A1 A2 -> .plabel= b ∃_1
%D    A0 A2 -> .plabel= r ∀_2
%D    A0 A1 -> .plabel= l ∃!_3
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{2}{$
  \diag{equalizer-big-1}
  $}
$$

Also, the ``equalizerness'' of the arrow $e$, that we are expressing
as $∀h\,∃!k$, can be re-expressed as an operation $φ$ that expects an
arrow $h$ and returns an arrow $k$:
%
%D diagram equalizer-big-2
%D 2Dx     100 +15 +15   +30
%D 2D  100 A0             
%D 2D      |  \           
%D 2D  +15 M0  M1           
%D 2D      |     \           
%D 2D  +15 A1 ---- A2 == A3 
%D 2D
%D ren A0 A1 A2 A3 ==> X E A B
%D ren A0 A1 A2 A3 ==> • • • •
%D ren M0 M1 ==> {} {}
%D
%D (( A2 A3 -> sl^^ .plabel= a f
%D    A2 A3 -> sl__ .plabel= b g
%D    A2 A3 midpoint .TeX= * place
%D    A1 A2 -> .plabel= b e
%D    A0 A2 -> .plabel= r h
%D    A0 A1 -> .plabel= l k
%D
%D    M0 M1 harrownodes nil 17 nil <- .plabel= b φ
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{1.5}{$
  \diag{equalizer-big-2}
  $}
$$

There is also a much more natural operation, $♮$, that takes a $k$,
composes it with $e$, and returns $h$. We can draw them at the same
time --- and by doing that it becomes clear that ``equalizerness'' in
this case can be translated to ``$♮$ is invertible''. In a diagram:
%
%D diagram equalizer-big-3
%D 2Dx     100 +18 +12   +30
%D 2D  100 A0             
%D 2D      |  \           
%D 2D  +18 M0  M1           
%D 2D      |     \           
%D 2D  +12 A1 ---- A2 == A3 
%D 2D
%D ren A0 A1 A2 A3 ==> X E A B
%D ren A0 A1 A2 A3 ==> • • • •
%D ren M0 M1 ==> {} {}
%D
%D (( A2 A3 -> sl^^ .plabel= a f
%D    A2 A3 -> sl__ .plabel= b g
%D    A2 A3 midpoint .TeX= * place
%D    A1 A2 -> .plabel= b e
%D    A0 A2 -> .plabel= r h
%D    A0 A1 -> .plabel= l k
%D
%D    M0 M1 harrownodes nil 17 nil -> sl^ .plabel= a ♮
%D    M0 M1 harrownodes nil 17 nil <- sl_ .plabel= b φ
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{1.5}{$
  \diag{equalizer-big-3}
  $}
$$

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

\subsection{An example: pullbacks}

Let's look at another example. ``Pullbackness'' for the square
%
%D diagram PB-0
%D 2Dx     100 100 +20
%D 2D  100 X
%D 2D        \
%D 2D  100     A > B
%D 2D          v   v
%D 2D  +20     C > D
%D 2D
%D # ren ==>
%D
%D (( A B -> A C -> B D -> C D ->
%D ))
%D enddiagram
%D
%D diagram PB-1
%D 2Dx     100 100 +20
%D 2D  100 X
%D 2D        \
%D 2D  100     A > B
%D 2D          v   v
%D 2D  +20     C > D
%D 2D
%D # ren ==>
%D
%D (( A B -> A C -> B D -> C D ->
%D    A relplace 6 6 \pbsymbol{7}
%D ))
%D enddiagram
%D
\pu
$$\diag{PB-1}
$$
%
means that the operation $♮$ that receives an arrow $X→A$ and returns
arrows $X→B$ and $X→C$ making everything commute has an inverse, $φ$.
If we draw $♮$ and $φ$ showing only the arrows that extend the square
diagrams, we get:
%
%D diagram PB-2
%D 2Dx     100 +15 +20
%D 2D  100 X
%D 2D        \
%D 2D  +15     A > B
%D 2D          v   v
%D 2D  +20     C > D
%D 2D
%D ren D ==> \phantom{D}
%D
%D (( X A -> D place
%D ))
%D enddiagram
%D
%D diagram PB-3
%D 2Dx     100 +15 +20
%D 2D  100 X
%D 2D        \
%D 2D  +15     A > B
%D 2D          v   v
%D 2D  +20     C > D
%D 2D
%D ren D ==> \phantom{D}
%D
%D (( X B -> X C -> D place
%D ))
%D enddiagram
%D
\pu
$$\left(\diag{PB-2}\right)
  \two/->`<-/<250>^♮_φ
  \left(\diag{PB-3}\right)
$$

The mnemonics are: `$♮$' stands for ``natural'', `$φ$' for
``factorization''.

The full definition of a pullback in my variation of Freyd's language
is:
%
$$\begin{array}{l}
  \diag{PB-1} \;\; := \\ \\ 
  (\diag{PB-0}, \;\; ∀X.
     \left(\diag{PB-2}\right)
     \two/->`<-/<250>^♮_φ
     \left(\diag{PB-3}\right)
  )
  \end{array}
$$

In English, this is:

\msk

A pullback $\sm{AB\\CD}$ is:

a pair made of a commutative square $\sm{AB\\CD}$ plus:

for all objects $X$ in our category, an inverse for the natural operation

that receives an arrow $X→A$ and returns arrows $X→B$ and $X→C$

[I'm leaving some commutativities implicit].

\bsk

I found that that diagrammatic language was easy to translate to a
formal, first-order language, and I also found something that made me
really ecstatic. Let me explain it in three steps.

\begin{itemize}

\item For me Category Theory, when done diagrammatically, has a
  ``fun'' part, that is made of {\sl diagrams} and {\sl
  constructions}, and a ``boring'' part, that is made of {\sl
  verifying equations} --- and I believe that when we don't have the
  diagrams we have to start by drawing them. See the idea of ``missing
  diagrams'' in \cite{SMDE}.

\item Category Theory is intrinsically dependently typed, and when we
  type things correctly many constructions become almost automatic ---
  because there is essentially only one way to build the result with
  the expected type from our inputs... so it's worthwhile to formalize
  our categorical constructions using Type Theory instead of Set
  Theory.

\item When I expressed categorical concepts using my variation of
  Freyd's diagrammatical language and then translated them to Type
  Theory the ``boring'' part became clearly separated from the ``fun''
  part. The ``boring'' part always lies in the last components of the
  tuples, and it is possible to define an operation that ``projects it
  out''.

\end{itemize}

A good part of the paper \cite{IDARCT} is dedicated to sketch how we
can split categorical constructions and proofs into a ``fun'' part
that we can do first, and we can leave all the ``boring'' part to a
second stage --- or we can wave our hands and leave that second part
to the reader as homework.


%  _____               _ _ _                _    
% |  ___|  _ __  _   _| | | |__   __ _  ___| | __
% | |_    | '_ \| | | | | | '_ \ / _` |/ __| |/ /
% |  _|   | |_) | |_| | | | |_) | (_| | (__|   < 
% |_|     | .__/ \__,_|_|_|_.__/ \__,_|\___|_|\_\
%         |_|                                    
%
% «formalizing-pullback»  (to ".formalizing-pullback")

\section{Formalizing the pullback}



%  ____                                    _                         
% |  _ \ _ __ ___  _ __  ___    __ _ ___  | |_ _   _ _ __   ___  ___ 
% | |_) | '__/ _ \| '_ \/ __|  / _` / __| | __| | | | '_ \ / _ \/ __|
% |  __/| | | (_) | |_) \__ \ | (_| \__ \ | |_| |_| | |_) |  __/\__ \
% |_|   |_|  \___/| .__/|___/  \__,_|___/  \__|\__, | .__/ \___||___/
%                 |_|                          |___/|_|              
%
% «propositions-as-types»  (to ".propositions-as-types")

\section{Propositions as Types}

\def\prf#1{\llangle#1\rrangle}
\def\Typ#1{\llbracket#1\rrbracket}

Let me show a notation that I find quite convenient for working with
propositions-as-types. The type associated to a proposition $P$ is
written as $\Typ{P}$; $\Typ{P}$ is an empty set when $P$ is false, and
a singleton set when $P$ is true. A proof, or witness, of $P$ is
written as $\prf{P}$, and we have $\prf{P}:\Typ{P}$. The meaning of
each ``$\prf{·}$'' depends on the context, and is given by a
dictionary. For example:




%  __  __                         _             _   
% |  \/  |_   _  __   ____ _ _ __(_) __ _ _ __ | |_ 
% | |\/| | | | | \ \ / / _` | '__| |/ _` | '_ \| __|
% | |  | | |_| |  \ V / (_| | |  | | (_| | | | | |_ 
% |_|  |_|\__, |   \_/ \__,_|_|  |_|\__,_|_| |_|\__|
%         |___/                                     
%
% «my-variant»  (to ".my-variant")

\section{My variant of Freyd's language}





\bsk

wave our hands 


After a working a bit with that variation of Freyd's diagrammatic
language, I realized that this definition of a pullback





\section{ND as a formal system}

Curry-Howard

Erasing and reconstructing

Terms as trees

\section{ND as a sloppy system}

Derived rules

Context

Double bars

omitted terms

omitted types

splitting big trees

% (idap 19 "pres-frob-bcc")
% (ida     "pres-frob-bcc")

% «nd-dep-types»  (to ".nd-dep-types")

\section{ND for dependent types}

% (ntyp 89 "pure-type-systems")
% (nty     "pure-type-systems")


\section{Frobenius}

% (find-books "__cats/__cats.el" "lawvere-equahyp")
% (find-lawvereequahyppage 6 "(1) Frobenius Reciprocity holds")
% (find-lawvereequahyptext 6 "(1) Frobenius Reciprocity holds")

% (hypp 11 "preservation-of-imp")
% (hyp     "preservation-of-imp")


%D diagram pres-imp-implies-frob
%D 2Dx     100 +40 +35 +25 +25 +35 +30
%D 2D  100 A0  A1      A3      A5  A6
%D 2D
%D 2D  +25 B0  B1  B2      B4  B5  B6
%D 2D
%D ren A0 A1   A3   A5 A6  ==> Σ_f(P{∧}f^*Q) P{∧}f^*Q P Σ_fP Σ_fP{∧}Q
%D ren B0 B1 B2  B4 B5 B6  ==> R f^*R (f^*Q{→}f^*R) f^*(Q{→}R) Q{→}R R
%D
%D (( A0 B0 ->
%D    A1 B1 ->
%D    A3 B2 ->
%D    A3 B4 ->  B2 B4 <->
%D    A5 B5 ->
%D    A6 B6 ->
%D    
%D    A0 B1 harrownodes nil 20 nil <->
%D    A1 B1 midpoint A3 B2 midpoint harrownodes nil 20 nil <->
%D    A3 B4 midpoint A5 B5 midpoint harrownodes nil 20 nil <->
%D    A5 B6 harrownodes nil 20 nil <->
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{pres-imp-implies-frob}
$$

%D diagram frob-implies-pres-imp
%D 2Dx     100 +20 +20 +20 +20 +20 +20
%D 2Dx     100 +40 +35 +25 +25 +35 +30
%D 2D  100 A0  A1  A2      A4  A5  A6
%D 2D
%D 2D  +25 B0  B1      B3      B5  B6
%D 2D
%D ren A0 A1 A2  A4 A5 A6  ==> P  P{∧}f^*Q  Σ_f(P{∧}f^*Q) Σ_fP∧Q  Σ_fP  P
%D ren B0 B1   B3   B5 B6  ==> (f^*Q{→}f^*R) f^*R R Q{→}R f^*(Q{→}R) 
%D
%D (( A0 B0 ->
%D    A1 B1 ->
%D    A2 B3 ->
%D    A4 B3 ->  A2 A4 <->
%D    A5 B5 ->
%D    A6 B6 ->
%D    
%D    A0 B1 harrownodes nil 20 nil <->
%D    A1 B1 midpoint A2 B3 midpoint harrownodes nil 20 nil <->
%D    A4 B3 midpoint A5 B5 midpoint harrownodes nil 20 nil <->
%D    A5 B6 harrownodes nil 20 nil <->
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{frob-implies-pres-imp}
$$


\section{Yoneda}

\def\ren{\text{ren}}
\def→{{\to}}

%:
%:
%:                           [:C→D]^2  [:D→E]^3
%:                           ------------------
%:                              :C→E
%:                          ------------2
%:                          :(C→D)→(C→E)
%:                       -------------------3
%:   C:  [D:]^1          :(D→E)→((C→D)→(C→E))
%:   ----------        -----------------------
%:     C→D:            :ΠD.(D→E)→((C→D)→(C→E))
%:   -------         --------------------------
%:   λD.C→D:         :ΠD.ΠE.(D→E)→((C→D)→(C→E))
%:   -------\ren     --------------------------\ren
%:   (C→\_)_0:              (C→\_)_1:
%:   --------------------------------
%:            (C→\_):
%:
%:            ^C->_
%:
%:
$$\pu
  \ded{C->_}
$$


%:
%:
%:                                  [:D→E]^3
%:                                  ------
%:                       [:A→RD]^2  :RD→RE
%:                       -----------------
%:                               :A→RE
%:                          --------------2
%:   [D:]^1                 :(A→RD)→(A→RE)
%:   ------             ----------------------3
%:    RD:               :(D→E)→((A→RD)→(A→RE))
%:   -----             -------------------------
%:   A→RD:             :ΠE.(D→E)→((A→RD)→(A→RE))
%:   --------        ----------------------------
%:   ∧D.A→RD:        :ΠD.ΠE.(D→E)→((A→RD)→(A→RE))
%:   --------\ren    ---------------------------\ren
%:   (A→R\_)_0:            (A→R\_)_1:
%:   --------------------------------
%:              (A→R\_):
%:
%:              ^A->R_
%:
%:
$$\pu
  \ded{A->R_}
$$


%:
%:                [:C→D]^1
%:                --------
%:    [:A→RC]^2    :RC→RD
%:    -------------------
%:            :A→RD
%:       -------------1
%:       :(C→D)→(A→RD)
%:     ----------------
%:     :ΠD.(C→D)→(A→RD)           C:    C:   [:(C→\_)→(A→R\_)]^2
%:     ------------------\ren    ----   ----------------------
%:     ((C→\_)→(A→R\_))_0:       :C→C   :(C→C)→(A→RC)
%:     -------------------       ------------
%:     :(C→\_)→(A→R\_)             :A→RC
%:     ---------------------------------2
%:        :(A→RC)↔((C→\_)→(A→R\_))
%:
%:        ^yoneda0-bij
%:
$$\pu
  \ded{yoneda0-bij}
$$



\newpage


\printbibliography




\end{document}

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

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020on-a-broken-dnc veryclean
make -f 2019.mk STEM=2020on-a-broken-dnc pdf

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