% (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:
