|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2026lawvere-adjfo.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2026lawvere-adjfo.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2026lawvere-adjfo.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2026lawvere-adjfo.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2026lawvere-adjfo.pdf"))
% (defun e () (interactive) (find-LATEX "2026lawvere-adjfo.tex"))
% (defun o () (interactive) (find-LATEX "2026lawvere-adjfo.tex"))
% (defun u () (interactive) (find-latex-upload-links "2026lawvere-adjfo"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2026lawvere-adjfo.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun oe () (interactive) (find-2a '(o) '(e)))
% (code-eec-LATEX "2026lawvere-adjfo")
% (find-pdf-page "~/LATEX/2026lawvere-adjfo.pdf")
% (find-sh0 "cp -v ~/LATEX/2026lawvere-adjfo.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2026lawvere-adjfo.pdf /tmp/pen/")
% (find-xournalpp "/tmp/2026lawvere-adjfo.pdf")
% file:///home/edrx/LATEX/2026lawvere-adjfo.pdf
% file:///tmp/2026lawvere-adjfo.pdf
% file:///tmp/pen/2026lawvere-adjfo.pdf
% http://anggtwu.net/LATEX/2026lawvere-adjfo.pdf
% https://anggtwu.net/LATEX/2026lawvere-adjfo.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps "Caepro5 Piecewise2 Maxima2 DiagMiddle1")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2026lawvere-adjfo" "2" "ladjfo2026" "ladj")
% «.geometry» (to "geometry")
% «.edrx26a» (to "edrx26a")
% «.biber» (to "biber")
% «.edrx26b» (to "edrx26b")
% «.edrx26c» (to "edrx26c")
% «.footer» (to "footer")
% «.defs» (to "defs")
%
% «.title» (to "title")
% «.diags-adjunction» (to "diags-adjunction")
% «.diags-CCC» (to "diags-CCC")
% «.diags-hyperdoctrine» (to "diags-hyperdoctrine")
% ;-- defs
\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-LATEX "dednat7-test1.tex")
%\usepackage{proof} % For derivation trees ("%:" lines)
%\usepackage{ebproof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
% «geometry» (to ".geometry")
% (find-es "tex" "geometry")
\usepackage[a6paper, landscape,
top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
]{geometry}
%
%
% «edrx26a» (to ".edrx26a")
\usepackage{edrx26a} % (find-LATEX "edrx26a.sty")
\def\dednatjobname{2026lawvere-adjfo} % (find-es "overleaf" "jobname")
%
% «biber» (to ".biber")
%\usepackage[backend=biber,
% style=alphabetic]{biblatex} % (find-es "tex" "biber")
%\addbibresource{catsem-ab.bib} % (find-LATEX "catsem-ab.bib")
%\addbibresource{education.bib} % (find-LATEX "education.bib")
%
\begin{document}
% «edrx26b» (to ".edrx26b")
\input edrx26b.tex % (find-LATEX "edrx26b.tex")
% «edrx26c» (to ".edrx26c")
% (find-LATEX "edrx26c.tex")
%L processsubfile "edrx26c.tex" -- runs the "%L"s
\input edrx26c % loads the defs
\pu % runs the "%L"s
% (find-LATEX "edrx26c.tex" "caepro")
%L -- dofile "Caepro5.lua"
\pu
% «footer» (to ".footer")
% (find-LATEX "edrxheadfoot.tex")
\def\drafturl{https://anggtwu.net/math-b.html}
\def\drafturl{https://anggtwu.net/LATEX/2026-1-C2.pdf}
\def\drafturl{https://anggtwu.net/2026.1-C2.html}
\def\draftfooter{\tiny \href{\drafturl}{\dednatjobname{}} \ColorBrown{\shorttoday{} \hours}}
% «defs» (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")
\def\nameof#1{\ulcorner#1\urcorner}
%L require "DiagForth1" -- (find-angg "LUA/DiagForth1.lua")
%L require "DiagTeX1" -- (find-angg "LUA/DiagTeX1.lua")
%L require "DiagMiddle1" -- (find-angg "LUA/DiagMiddle1.lua")
\pu
% ;-- title
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title» (to ".title")
% (ladjfo2026p 1 "title")
% (ladjfo2026a "title")
\thispagestyle{empty}
\begin{center}
\vspace*{1.2cm}
{\bf \large Notes on Lawvere's}
{\bf \large ``Adjointness in Foundations''}
{\bf \large and ``Equality in Hyperdoctrines''}
\bsk
%Aula nn: ponha o título aqui
\bsk
Eduardo Ochs - RCN/PURO/UFF
\url{https://anggtwu.net/math-b.html}
\end{center}
\newpage
% «diags-adjunction» (to ".diags-adjunction")
\def\objFB#1#2#3{\psm{#1 \!\! \\ & #1F \ton{#2} #3}}
\def\objAU#1#2#3{\psm{& #3 \\ #1 \ton{#2} #3U}}
%D diagram adjunction
%D 2Dx 100 +20 +20 +20 +20 +20
%D 2D 100 E0 C0 A0 <-| A1 D0 F0
%D 2D | | | | | |
%D 2D | | | <-> | | |
%D 2D v v v v v v
%D 2D +20 E1 C1 A2 |-> A3 D1 F1
%D 2D
%D 2D +15 B0 <-> B1
%D 2D
%D ren A0 A1 ==> AF A
%D ren A2 A3 ==> B BU
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 ==> BUF B
%D ren D0 D1 ==> A AFU
%D ren E0 E1 ==> UF \catB
%D ren F0 F1 ==> \catA FU
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l h
%D A1 A3 -> .plabel= r f
%D A2 A3 |->
%D # A0 A3 harrownodes nil 20 nil <->
%D B0 B1 <- sl^ .plabel= a F
%D B0 B1 -> sl_ .plabel= b U
%D C0 C1 -> .plabel= l Bε
%D D0 D1 -> .plabel= r Aη
%D E0 E1 -> .plabel= l ε
%D F0 F1 -> .plabel= r η
%D ))
%D enddiagram
\pu
%D diagram comma:(F,catB)
%D 2Dx 100 +35 +15 +25
%D 2D 100 C0
%D 2D +5 A0 |
%D 2D +5 | | D0 --> D1
%D 2D | v | |
%D 2D +15 v C1 | |
%D 2D +5 A1 v v
%D 2D +5 D2 --> D3
%D 2D
%D 2D +15 B0
%D 2D
%D ren A0 A1 ==> \objFB{A}{h}{B} \objFB{A'}{h'}{B'}
%D ren B0 ==> (F,\catB)
%D ren C0 C1 ==> A A'
%D ren D0 D1 D2 D3 ==> AF B A'F B'
%D
%D (( A0 A1 -> .plabel= l (a,b)
%D B0 place
%D C0 C1 -> .plabel= l a
%D D0 D1 -> .plabel= a h
%D D0 D2 -> .plabel= r aF
%D D1 D3 -> .plabel= r b
%D D2 D3 -> .plabel= a h'
%D ))
%D enddiagram
%D
\pu
%D diagram comma:(catA,U)
%D 2Dx 100 +30 +25 +15
%D 2D 100 D0
%D 2D +5 A0 |
%D 2D +5 | C0 --> C1 |
%D 2D | | | v
%D 2D +15 v | | D1
%D 2D +5 A1 v v
%D 2D +5 C2 --> C3
%D 2D
%D 2D +15 B0
%D 2D
%D ren A0 A1 ==> \objAU{A}{f}{B} \objAU{A'}{f'}{B'}
%D ren B0 ==> (\catA,U)
%D ren C0 C1 C2 C3 ==> A BU A' B'U
%D ren D0 D1 ==> B B'
%D
%D (( A0 A1 -> .plabel= l (a,b)
%D B0 place
%D C0 C1 -> .plabel= a f
%D C0 C2 -> .plabel= l a
%D C1 C3 -> .plabel= l bU
%D C2 C3 -> .plabel= a f'
%D D0 D1 -> .plabel= r b
%D ))
%D enddiagram
%D
\pu
%D diagram adj-via-comma
%D 2Dx 100 +20 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +30 A2
%D 2D
%D ren A0 A1 A2 ==> (F,\catB) (\catA,U) \catA×\catB
%D
%D (( A0 A1 -> sl^ .plabel= a Q
%D A0 A1 <- sl_ .plabel= b Q^{-1}
%D A1 A2 ->
%D A0 A2 ->
%D ))
%D enddiagram
%D
\pu
% «diags-CCC» (to ".diags-CCC")
%D diagram terminal-adj
%D 2Dx 100 +25
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +20 A4 A5
%D 2D
%D 2D +20 B0 B1
%D 2D
%D ren A0 A1 ==> • 0
%D ren A2 A3 ==> • C
%D ren A4 A5 ==> • 1
%D ren B0 B1 ==> \mathbf{1} \catC
%D
%D (( A0 A1 |->
%D A2 A3 <-|
%D A4 A5 |->
%D A0 A2 ->
%D A1 A3 ->
%D A2 A4 ->
%D A3 A5 ->
%D B0 B1 -> sl^^ .plabel= a \mathbf{0}
%D B0 B1 <- .plabel= m !
%D B0 B1 -> sl__ .plabel= b \mathbf{1}
%D ))
%D enddiagram
\pu
%D diagram prod-adj
%D 2Dx 100 +30
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +20 A4 A5
%D 2D
%D 2D +20 B0 B1
%D 2D
%D ren A0 A1 ==> (A,B) A⊔B
%D ren A2 A3 ==> (C,C) C
%D ren A4 A5 ==> (D,E) D×E
%D ren B0 B1 ==> \catC×\catC \catC
%D
%D (( A0 A1 |->
%D A2 A3 <-|
%D A4 A5 |->
%D A0 A2 ->
%D A1 A3 ->
%D A2 A4 ->
%D A3 A5 ->
%D B0 B1 -> sl^^ .plabel= a ⊔
%D B0 B1 <- .plabel= m Δ
%D B0 B1 -> sl__ .plabel= b ×
%D ))
%D enddiagram
\pu
%D diagram exponential-adj
%D 2Dx 100 +20 +20 +25 +20 +20
%D 2D 100 E0 C0 A0 <-| A1 D0 F0
%D 2D | | | | | |
%D 2D | | | <-> | | |
%D 2D v v v v v v
%D 2D +25 E1 C1 A2 |-> A3 D1 F1
%D 2D
%D 2D +15 B0 <-> B1
%D 2D
%D ren A0 A1 ==> A{×}X X
%D ren A2 A3 ==> Y Y^A
%D ren B0 B1 ==> \catC \catC
%D ren C0 C1 ==> A{×}Y^A Y
%D ren D0 D1 ==> X (A{×}X)^A
%D ren E0 E1 ==> UF \catB
%D ren F0 F1 ==> \catA FU
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l h
%D A1 A3 -> .plabel= r f
%D A2 A3 |->
%D # A0 A3 harrownodes nil 20 nil <->
%D B0 B1 <- sl^ .plabel= a A{×}(\,)
%D B0 B1 -> sl_ .plabel= b (\,)^A
%D C0 C1 -> .plabel= l Yε_A
%D D0 D1 -> .plabel= r Xλ_A
%D # E0 E1 -> .plabel= l ε
%D # F0 F1 -> .plabel= r η
%D ))
%D enddiagram
\pu
%D diagram exponential-adj-1
%D 2Dx 100 +20 +20 +25 +20 +20
%D 2D 100 AA
%D 2D ^|
%D 2D |v
%D 2D +20 E0 C0 A0 <-| A1 D0 F0
%D 2D | | | | | |
%D 2D | | | <-> | | |
%D 2D v v v v v v
%D 2D +25 E1 C1 A2 |-> A3 D1 F1
%D 2D
%D 2D +15 B0 <-> B1
%D 2D
%D ren AA ==> A
%D ren A0 A1 ==> A{×}1 1
%D ren A2 A3 ==> Y Y^A
%D ren B0 B1 ==> \catC \catC
%D ren C0 C1 ==> A{×}Y^A Y
%D ren D0 D1 ==> 1 (A{×}1)^A
%D ren E0 E1 ==> UF \catB
%D ren F0 F1 ==> \catA FU
%D
%D (( AA A0 -> sl^ .plabel= r 〈A,1〉
%D AA A0 <- sl_ .plabel= l π_1
%D AA A2 -> .slide= -20pt .plabel= l f
%D A0 A1 <-|
%D A0 A2 -> # .plabel= l h
%D A1 A3 -> .plabel= r \nameof{f}
%D A2 A3 |->
%D # A0 A3 harrownodes nil 20 nil <->
%D B0 B1 <- sl^ .plabel= a A{×}(\,)
%D B0 B1 -> sl_ .plabel= b (\,)^A
%D # C0 C1 -> .plabel= l Yε_A
%D # D0 D1 -> .plabel= r Xλ_A
%D # E0 E1 -> .plabel= l ε
%D # F0 F1 -> .plabel= r η
%D ))
%D enddiagram
\pu
\scalebox{0.5}{\def\colwidth{9cm}\firstcol{
$$\diag{adjunction}
$$
$$\diag{comma:(F,catB)}
$$
$$\diag{comma:(catA,U)}
$$
$$\diag{adj-via-comma}
$$
}\anothercol{
% (find-books "__cats/__cats.el" "lawvere-adjfo" "10" "(2) A product C × C −−−→ C, meaning a right adjoint to the diagonal functor")
$$\diag{terminal-adj}
\qquad
\diag{prod-adj}
$$
$$\diag{exponential-adj}
$$
$$\diag{exponential-adj-1}
$$
}}
% «diags-hyperdoctrine» (to ".diags-hyperdoctrine")
%D diagram adjs-to-change-of-base
%D 2Dx 100 +40
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +20 A4 A5
%D 2D
%D 2D +20 B0 B1
%D 2D
%D 2D +20 C0 C1
%D 2D
%D ren A0 A1 ==> φ φΣf
%D ren A2 A3 ==> f·ψ ψ
%D ren A4 A5 ==> ζ ζΠf
%D ren B0 B1 ==> P(X) P(Y)
%D ren C0 C1 ==> X Y
%D
%D (( A0 A1 |->
%D A2 A3 <-|
%D A4 A5 |->
%D A0 A2 ->
%D A1 A3 ->
%D A2 A4 ->
%D A3 A5 ->
%D B0 B1 -> sl^^ .plabel= a (\,)Σf
%D B0 B1 <- .plabel= m f·(\,)
%D B0 B1 -> sl__ .plabel= b (\,)Πf
%D C0 C1 -> .plabel= a f
%D ))
%D enddiagram
\pu
\scalebox{0.6}{\def\colwidth{9cm}\firstcol{
$$\diag{adjs-to-change-of-base}
$$
}\anothercol{
}}
\newpage
%D diagram equahyp-p5-reflexivity
%D 2Dx 100 +40 +25
%D 2D 100 A0 A1 A1'
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A1' ==> 1_X 1_XΣ(Xδ) =Θ_X
%D ren A2 A3 ==> Xδ·Θ_X Θ_X
%D ren B0 B1 ==> X X×X
%D
%D (( A0 A1 |->
%D A1' place
%D A2 A3 <-|
%D A0 A2 -> .plabel= l \text{refl}
%D A1 A3 -> .plabel= r \text{id}
%D A0 A3 harrownodes nil 20 nil <-|
%D B0 B1 -> sl^ .plabel= a (\,)Σ(Xδ)
%D B0 B1 <- sl_ .plabel= m Xδ·(\,)
%D ))
%D enddiagram
\pu
\scalebox{0.6}{\def\colwidth{9cm}\firstcol{
EquaHyp, p.5:
1. We define, for each type $X$, an attribute of type $X×X$ as follows
%
$$Θ_X=1_XΣ(Xδ)$$
The adjunction then provides a canonical deduction $1_X→(Xδ)·Θ_X$
which we interpret to mean that “reflexivity” holds for “equality” so
defined.
%
$$\diag{equahyp-p5-reflexivity}$$
}\anothercol{
}}
\newpage
%D diagram equahyp-p6-squares
%D 2Dx 100 +40 +40 +40
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +20 B3'
%D 2D +10 A2 A3 B2 B3
%D 2D
%D 2D +20 C0 C1 D0 D1
%D 2D +10 D0'
%D 2D
%D 2D +20 C2 C3 D2 D3
%D 2D
%D ren A0 A1 ==> P(Y) P(Y)
%D ren A2 A3 ==> P(X) P(X)
%D ren B0 B1 ==> ψ α{⇒}ψ
%D ren B3' ==> f{·}(α{⇒}ψ)
%D ren B2 B3 ==> f{·}ψ (f{·}α){⇒}(f{·}ψ)
%D ren C0 C1 ==> P(Y) P(Y)
%D ren C2 C3 ==> P(X) P(X)
%D ren D0 D1 ==> α{∧}(φΣf) φΣf
%D ren D0' ==> ((f{·}α){∧}φ)Σf
%D ren D2 D3 ==> (f{·}α){∧}φ φ
%D
%D (( A0 A1 -> .plabel= a α{⇒}(\,)
%D A0 A2 -> .plabel= l f·(\,)
%D A1 A3 -> .plabel= r f·(\,)
%D A2 A3 -> .plabel= a (f{·}α){⇒}(\,)
%D
%D B0 B1 |->
%D B0 B2 |->
%D B1 B3' |->
%D B2 B3 |->
%D
%D C0 C1 <- .plabel= a α{∧}(\,)
%D C0 C2 <- .plabel= l (\,)Σf
%D C1 C3 <- .plabel= r (\,)Σf
%D C2 C3 <- .plabel= a (f{·}α){∧}(\,)
%D
%D D0 D1 <-|
%D D0' D2 <-|
%D D1 D3 <-|
%D D2 D3 <-|
%D
%D ))
%D enddiagram
\pu
%D diagram equahyp-p6-(3)
%D 2Dx 100 +40 +40
%D 2D 100 A0 |---------> A1
%D 2D
%D 2D +20 A2 |--> A3 <-> A3'
%D 2D
%D 2D +20 A4 <---------| A5
%D 2D
%D 2D +15 B0 ----------> B1
%D 2D
%D ren A0 A1 ==> φ φΣf
%D ren A2 A3 A3' ==> (f{·}α){∧}φ ((f{·}α){∧}φ)Σf α{∧}ψΣf
%D ren A4 A5 ==> f{·}α α
%D ren B0 B1 ==> X Y
%D
%D (( A0 A1 |->
%D A2 A0 ->
%D A3 A1 ->
%D A3' A1 ->
%D A2 A3 |->
%D A3 A3' -> .plabel= a ≈
%D A2 A4 ->
%D A3 A5 ->
%D A3' A5 ->
%D A4 A5 <-|
%D B0 B1 -> .plabel= a f
%D ))
%D enddiagram
\pu
\scalebox{0.6}{\def\colwidth{9cm}\firstcol{
EquaHyp, p.6:
DEFINITION-THEOREM. In any eed, the following are equivalent:
(1) Frobenius Reciprocity holds.
(2) For any $f:X→Y$, $α,ψ∈P(Y)$ $f·(α⇒ψ) \ton{≈} f·α⇒f·ψ$.
(3) For any $f:X→Y$, $φ∈P(X)$, $α∈P(Y)$, $((f·α)∧φ)Σf \ton{≈} α∧(φΣf)$.
$$3) \qquad \diag{equahyp-p6-(3)}
$$
}\anothercol{
$$\diag{equahyp-p6-squares}
$$
}}
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% (find-pdfpages2-links "~/LATEX/" "2026lawvere-adjfo")
% Local Variables:
% coding: utf-8-unix
% outline-regexp: "% +;--"
% ee-tla: "ladj"
% ee-tla: "ladjfo2026"
% End: