|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: