|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2026jacobs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2026jacobs.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2026jacobs.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2026jacobs.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2026jacobs.pdf"))
% (defun e () (interactive) (find-LATEX "2026jacobs.tex"))
% (defun o () (interactive) (find-LATEX "2026jacobs.tex"))
% (defun u () (interactive) (find-latex-upload-links "2026jacobs"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2026jacobs.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun oe () (interactive) (find-2a '(o) '(e)))
% (code-eec-LATEX "2026jacobs")
% (find-pdf-page "~/LATEX/2026jacobs.pdf")
% (find-sh0 "cp -v ~/LATEX/2026jacobs.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2026jacobs.pdf /tmp/pen/")
% (find-xournalpp "/tmp/2026jacobs.pdf")
% file:///home/edrx/LATEX/2026jacobs.pdf
% file:///tmp/2026jacobs.pdf
% file:///tmp/pen/2026jacobs.pdf
% http://anggtwu.net/LATEX/2026jacobs.pdf
% https://anggtwu.net/LATEX/2026jacobs.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps "Caepro5 Piecewise2 Maxima2 TocLines3")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2026jacobs" "2" "jac2026" "jac")
% «.geometry» (to "geometry")
% «.edrx26a» (to "edrx26a")
% «.biber» (to "biber")
% «.edrx26b» (to "edrx26b")
% «.edrx26c» (to "edrx26c")
% «.defs» (to "defs")
% «.footer» (to "footer")
% «.defs-T-and-B» (to "defs-T-and-B")
% «.defs-bookmark» (to "defs-bookmark")
%
% «.title» (to "title")
% «.toc» (to "toc")
% «.links» (to "links")
% «.cartesianness-jacobs» (to "cartesianness-jacobs")
% «.cartesianness-edrx» (to "cartesianness-edrx")
% «.poor-mans-string-diags» (to "poor-mans-string-diags")
% «.fibred-equality» (to "fibred-equality")
% «.BCC-equality» (to "BCC-equality")
% «.subset-types» (to "subset-types")
%
% «.writetoc» (to "writetoc")
% «.references» (to "references")
% «.make-with-bib» (to "make-with-bib")
% ;-- defs
\documentclass[oneside,12pt]{article}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb} % (find-es "tex" "colorweb")
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage[atend]{bookmark} % (find-es "tex" "bookmark")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
%\usepackage{tikz}
%
% (find-LATEX "dednat7-test1.tex")
\usepackage{proof} % 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")
%
% «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
% «defs» (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")
% «footer» (to ".footer")
% (find-LATEX "edrxheadfoot.tex")
\def\drafturl{http://anggtwu.net/LATEX/2026-1-C2.pdf}
\def\drafturl{http://anggtwu.net/2026.1-C2.html}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
% «defs-T-and-B» (to ".defs-T-and-B")
\long\def\ColorDarkOrange#1{{\color{orange!90!black}#1}}
\def\T(Total: #1 pts){{\bf(Total: #1)}}
\def\T(Total: #1 pts){{\bf(Total: #1 pts)}}
\def\T(Total: #1 pts){\ColorRed{\bf(Total: #1 pts)}}
\def\B (#1 pts){\ColorDarkOrange{\bf(#1 pts)}}
\def\Eq {\mathsf{Eq}}
\def\BCCL {\mathsf{BCCL}}
\def\Prop {\mathsf{Prop}}
\def\Type {\mathsf{Type}}
\def\sfi {\mathsf{i}}
\def\sfo {\mathsf{o}}
% «defs-bookmark» (to ".defs-bookmark")
% (find-es "tex" "bookmark")
\def\slidebookmark#1{
\hypertarget{#1}{}
\bookmark[dest=#1]{#1}
}
% ;-- title
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title» (to ".title")
% (jac2026p 1 "title")
% (jac2026a "title")
\thispagestyle{empty}
\begin{center}
\vspace*{1.2cm}
{\bf \Large Notes about Jacobs's book}
\bsk
%Aula nn: ponha o título aqui
%
%\bsk
Eduardo Ochs - RCN/PURO/UFF
Psicopata do CEFET
\url{https://anggtwu.net/math-b.html}
\end{center}
%\newpage
% ;-- toc
% «toc» (to ".toc")
% (to "writetoc")
% ;-- links
% «links» (to ".links")
% (jac2026p 2 "links")
% (jac2026a "links")
%{\bf Links}
%
%\scalebox{0.6}{\def\colwidth{16cm}\firstcol{
%}\anothercol{
%}}
% (jac2020p)
% (jac2020a)
% (find-books "__cats/__cats.el" "freyd76")
% (find-books "__cats/__cats.el" "freyd-scedrov" "28" "1.39. The language of diagrams")
% (find-books "__cats/__cats.el" "heller-tierney" "55" "Freyd")
% (misp 17 "freyd-notation")
% (misa "freyd-notation")
% (misa "freyd-notation" "equalizers")
% (misp 18 "freyd-with-functors")
% (misa "freyd-with-functors")
% (misp 44 "ness")
% (misa "ness")
\newpage %-- cartesianness-jacobs
%
% ____ _ _ _
% / ___|__ _ _ __| |_ | | __ _ ___ ___ | |__ ___
% | | / _` | '__| __| _ | |/ _` |/ __/ _ \| '_ \/ __|
% | |__| (_| | | | |_ | |_| | (_| | (_| (_) | |_) \__ \
% \____\__,_|_| \__| \___/ \__,_|\___\___/|_.__/|___/
%
% «cartesianness-jacobs» (to ".cartesianness-jacobs")
% (jac2026p 99 "cartesianness-jacobs")
% (jac2026a "cartesianness-jacobs")
% (find-books "__cats/__cats.el" "jacobs" "27" "Finally, we come to the definition of 'fibration'")
% (find-es "tex" "bookmark")
\slidebookmark{1.1.3 Cartesianness}
\SLIDE{Cartesianness (Jacobs)}
\scalebox{0.8}{\def\colwidth{14cm}\firstcol{
From \cite[p.27]{Jacobs}:
\ssk
{\bf 1.1.3. Definition.} Let $p:\bbE→\bbB$ be a functor.
(i) A morphism $f:X→Y$ in $\bbE$ is {\bf Cartesian over} $u:I→J$ in
$\bbB$ if $pf=u$ and every $g:Z→Y$ in $\bbE$ for which one has
$pg=u∘w$ for some $w:pZ→I$, uniquely determines an $h:Z→X$ in $\bbE$
above $w$ with $f∘h=g$. In a diagram:
%
%L forths["-"] = function () pusharrow("-") end
%
%D diagram cartesianness-jacobs
%D 2Dx 100 +20 +20 +30
%D 2D 100 A0 ____
%D 2D +15 E \ \
%D 2D +10 | A1 - A2
%D 2D |
%D 2D +10 v A3 ____
%D 2D +15 B \ \
%D 2D +10 A4 - A5
%D
%D ren E B A0 A1 A2 A3 A4 A5 ==> \bbE \bbB Z X Y pZ I J
%D
%D (( E B -> .plabel= l p
%D
%D A0 A1 --> .plabel= l h
%D A1 A2 -> .plabel= b f
%D A0 A2 -> .plabel= a g
%D A3 A4 -> .plabel= l w
%D A4 A5 -> .plabel= b u
%D A3 A5 -> .plabel= a u∘w=pg
%D ))
%D enddiagram
\pu
$$\diag{cartesianness-jacobs}
$$
We call $f:X→Y$ in the total category $\bbE$ Cartesian if it is
Cartesian over its underlying map $pf$ in $\bbB$.
}\anothercol{
}}
\newpage %-- cartesianness-edrx
% ____ _ _____ _
% / ___|__ _ _ __| |_ | ____|__| |_ ____ __
% | | / _` | '__| __| | _| / _` | '__\ \/ /
% | |__| (_| | | | |_ | |__| (_| | | > <
% \____\__,_|_| \__| |_____\__,_|_| /_/\_\
%
% «cartesianness-edrx» (to ".cartesianness-edrx")
% (jac2026p 99 "cartesianness-edrx")
% (jac2026a "cartesianness-edrx")
\SLIDE{Cartesianness (Edrx)}
%L forths["-"] = function () pusharrow("-") end
%
%D diagram cartesianness-edrx
%D 2Dx 100 +00 +20 +15 +15 +10 +20 +15 +15 +10 +20
%D 2D 100 U0 U1
%D 2D | |
%D 2D +10 A0 ____ | B0 ____ | C0 ____
%D 2D \ \ | \ \ | \ \
%D 2D +15 A1 - A2 | B1 - B2 | C1 - C2
%D 2D | |
%D 2D +10 A3 ____ | B3 ____ | C3 ____
%D 2D \ \ | \ \ | \ \
%D 2D +15 A4 - A5 | B4 - B5 | C4 - C5
%D 2D | |
%D 2D +10 L0 L1
%D
%D ren A0 A1 A2 A3 A4 A5 ==> {} Q R {} {} {}
%D ren U0 L0 B0 B1 B2 B3 B4 B5 ==> ∀ {} P Q R A B C
%D ren U1 L1 C0 C1 C2 C3 C4 C5 ==> ∃! {} P Q R A B C
%D
%D (( A1 A2 -> .plabel= a β
%D
%D U0 L0 -
%D
%D # B0 B1 -> .plabel= l α
%D B1 B2 -> .plabel= b β
%D B0 B2 -> .plabel= a γ
%D B3 B4 -> .plabel= l f
%D B4 B5 -> .plabel= b g
%D B3 B5 -> .plabel= a h
%D
%D U1 L1 -
%D
%D C0 C1 -> .plabel= l α
%D C1 C2 -> .plabel= b β
%D C0 C2 -> .plabel= a γ
%D C3 C4 -> .plabel= l f
%D C4 C5 -> .plabel= b g
%D C3 C5 -> .plabel= a h
%D ))
%D enddiagram
\pu
\scalebox{0.8}{\def\colwidth{9cm}\firstcol{
Let $p:\bbE \to \bbB$ be our projection functor.
$β:Q→R$ is {\sl cartesian} when:
%
$$\diag{cartesianness-edrx}
$$
The details:
%
$$∀\pmat{P,A,B,C,
γ,f,g,h,\\
A=pP,B=pQ,C=pR,\\
g=pβ,h=pγ,h=g∘f
}.
∃!\pmat{α,\\
γ=β∘α,\\
f=pα}
$$
}\anothercol{
}}
\newpage
% (find-es "tex" "bookmark")
% (find-books "__cats/__cats.el" "jacobs" "47" "1.4 Cloven and split")
\slidebookmark{1.4 Cloven and split fibrations}
\SLIDE{Cloven and split fibrations (Jacobs)}
%D diagram p47-choose-cartesian
%D 2Dx 100 +30
%D 2D 100 A0 A1
%D 2D
%D ren A0 A1 ==> u^*(X) X
%D
%D (( A0 A1 -> .plabel= a \ovl{u}(X)
%D ))
%D enddiagram
%D
\pu
%D diagram p48-u*
%D 2Dx 100 +30
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 A4 A5
%D 2D
%D ren A0 A1 ==> u^*(X) X
%D ren A2 A3 ==> u^*(Y) Y
%D ren A4 A5 ==> I J
%D
%D (( A0 A1 -> .plabel= a \ovl{u}(X)
%D A2 A3 -> .plabel= a \ovl{u}(Y)
%D A4 A5 -> .plabel= b u
%D
%D A0 A2 --> .plabel= l u^*(f)
%D A1 A3 -> .plabel= r f
%D ))
%D enddiagram
%D
\pu
\scalebox{0.5}{\def\colwidth{9.5cm}\firstcol{
{}
The definition of a fibration is of the form ``for every $x$ and $y$
there is a $z$ such that ...''. This does not imply that we are given
for each pair $x,y$ an explicit $z$, unless we make use of the Axiom
of Choice. The differences in the way the structure of a fibration may
be given will concern us in this section. Briefly, a fibration is
called {\bf cloven} if it comes together with a choice of Cartesian
liftings; and it is called {\bf split} if it is cloven and the given
liftings are well-behaved in the sense that they satisfy certain
functoriality conditions. These fibrations behave more pleasantly, and
therefore we prefer to work with fibrations in split form (if this is
possible). Cloven and split fibrations give rise to so-called indexed
categories $\bbB^\op \to \Cat$. These generalise set-valued functors
(or presheaves) $\bbB^\op \to \Cat$.
\msk
We recall that a functor $\psm{\bbE\\↓p\\\bbP}$ is a fibration if for
every map $u:I→J$ in the base category $\bbB$ and every object
$X∈\bbE$ above $J$ in the total category, there is a Cartesian lifting
$•→X$ in $\bbE$. Assume now we choose for every such $u$ and $X$ a
specific Cartesian lifting and write it as
%
$$\diag{p47-choose-cartesian}
$$
%
(By Proposition 1.1.4 we can only choose up-to vertical isomorphisms.)
}\def\colwidth{12cm}\anothercol{
{}
We claim that, having made such choices, every map $u:I→J$ in $\bbB$
determines a functor $u^*$ from the fibre $\bbE_J$ over $J$ to the
fibre $\bbE_I$ over $I$. (Note the direction!) The recipe for
$u^*:\bbE_J→\bbE_I$ is as follows.
\begin{itemize}
\item for an object $X∈\bbE_J$ one has $pX=J$ and so we take
$u*(X)∈\bbE_I$ to be the domain of the previously determined
Cartesian lifting $\ovl{u}(X):u^*(X)→X$;
\item for a map $f:X→Y$ in $\bbE_J$, consider the following diagram in
$\bbE$.
%
$$\diag{p48-u*}
$$
The composite $f∘\ovl{u}(X):u^*(X)→Y$ is above $u$, since $f$ is
vertical. Because $u(Y)$ is by definition the {\sl terminal} lifting
of $u$ with codomain $Y$, there is a unique map
$u^*(X) \dashrightarrow u^*(Y)$, call it $u^*(f)$, with
$\ovl{u}(Y)∘u^*(f) = f∘\ovl{u}(X)$.
\end{itemize}
By uniqueness, $u*$ preserves identities and composition. Thus one
obtains a functor $u^*:\bbE_J→\bbE_I$. Such functors $u*$ are known
under various names: as {\bf reindexing} functors, {\bf substitution}
functors, {\bf relabelling} functors, {\bf inverse image} functors or
sometimes also as {\bf change-of-base} or as {\bf pullback functors}.
We mostly use the first two names.
}}
\newpage
% (find-LATEX "edrxgac2.tex" "C2" "\\veq")
\def\dnito{\raise 8pt\hbox{\rotatebox{270}{$\ito$}}}
\Sa{Prop1}#1#2#3{#3}
\Sa{Prop2}#1#2#3{\setofst{#1∈#2}{#3}}
\Sa{Prop3}#1#2#3{\pmat{\setofst{#1∈#2}{#3}\\\dnito\\#2}}
%$\ga{Prop1}{a}{A}{P(a)}
% \ga{Prop2}{a}{A}{P(a)}
% \ga{Prop3}{a}{A}{P(a)}
%$
%D diagram change-of-base-prop
%D 2Dx 100 +75 +65 +65 +45 +30
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +25 A2 A3 B2 B3 C2 C3
%D 2D
%D ren A0 A1 ==> \ga{Prop3}{a}{A}{P(f(a))} \ga{Prop3}{b}{B}{P(b)}
%D ren B0 B1 ==> \ga{Prop2}{a}{A}{P(f(a))} \ga{Prop2}{b}{B}{P(b)}
%D ren C0 C1 ==> \ga{Prop1}{a}{A}{P(f(a))} \ga{Prop1}{b}{B}{P(b)}
%D ren A2 A3 ==> A B
%D ren B2 B3 ==> A B
%D ren C2 C3 ==> A B
%D
%D (( A0 A1 <-|
%D B0 B1 <-|
%D C0 C1 <-|
%D A2 A3 -> .plabel= a f
%D B2 B3 -> .plabel= a f
%D C2 C3 -> .plabel= a f
%D ))
%D enddiagram
%D
\pu
\scalebox{0.5}{\def\colwidth{9cm}\firstcol{
% (find-books "__cats/__cats.el" "jacobs" "23" "cod: Sets^\\\\to -> Sets")
$$\diag{change-of-base-prop}
$$
}\anothercol{
}}
\newpage
%D diagram cod-is-cloven
%D 2Dx 100 +45 +30
%D 2D 100 A0 A1 A2
%D 2D
%D 2D +20 A3 A4 A5
%D 2D
%D ren A0 A1 A2 ==> A{×}_B(B{×}_CD) B{×}_CD D
%D ren A3 A4 A5 ==> A B C
%D
%D (( A0 A1 -> .plabel= a π'
%D A1 A2 -> .plabel= a π'
%D A0 A3 -> .plabel= l π
%D A1 A4 -> .plabel= l π
%D A2 A5 -> .plabel= r h
%D A3 A4 -> .plabel= a f
%D A4 A5 -> .plabel= a g
%D ))
%D enddiagram
\pu
$$\diag{cod-is-cloven}
$$
\newpage
% ;-- poor-mans-string-diags
% «poor-mans-string-diags» (to ".poor-mans-string-diags")
% (jac2026p 7 "poor-mans-string-diags")
% (jac2026a "poor-mans-string-diags")
\SLIDE{Poor man's string diagrams}
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 55) "1. Universal Arrows")
%
%D diagram univ-arrow-cwm-my-letters
%D 2Dx 100 +25 +25
%D 2D 100 A0 A1 A2
%D 2D
%D 2D +25 A3 A4 A5
%D 2D
%D ren A0 A1 A2 ==> A RB B
%D ren A3 A4 A5 ==> A RB', B'.
%D
%D (( A0 A1 -> .plabel= a η
%D A0 A3 midpoint .TeX= \veq place
%D A1 A4 .> .plabel= r Rf
%D A2 A5 .> .plabel= r f
%D A3 A4 -> .plabel= a g
%D ))
%D enddiagram
%D diagram universal-arrow-stages
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 U0 U1
%D 2D
%D 2D +10 A1 B1 C1
%D 2D | | |
%D 2D +20 A2 A3 B2 B3 C2 C3
%D 2D | | | | | |
%D 2D +20 A4 A5 B4 B5 C4 C5
%D 2D
%D 2D +15 A6 A7 B6 B7 C6 C7
%D 2D
%D 2D +10 L0 L1
%D 2D
%D ren A1 A2 A3 A4 A5 A6 A7 ==> A B RB B' RB' \catB \catA
%D ren B1 B2 B3 B4 B5 B6 B7 ==> A B RB B' RB' \catB \catA
%D ren C1 C2 C3 C4 C5 C6 C7 ==> A B RB B' RB' \catB \catA
%D ren U0 L0 ==> ∀ {}
%D ren U1 L1 ==> ∃! {}
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A6 A7 -> .plabel= a R
%D U0 L0 -
%D ))
%D (( B1 B3 -> .plabel= r η
%D B2 B3 |->
%D B4 B5 |->
%D B1 B5 -> .slide= 15pt .plabel= r g
%D B6 B7 -> .plabel= a R
%D U1 L1 -
%D ))
%D (( C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 20pt .plabel= r g
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
\pu
\scalebox{0.45}{\def\colwidth{13.5cm}\firstcol{
From ``On the missing...'', section 4.2:
(\url{https://anggtwu.net/LATEX/2022on-the-missing.pdf\#page=18})
\msk
Let me use an example to discuss this. This is the definition of
universal arrow in [CWM2, p.55], including the original diagram,
modulo change of letters:
\begin{quotation}
{\bf Definition.} If $R: \catB→\catA$ is a functor and $A$ an object
of $\catA$, a universal arrow from $A$ to $R$ is a pair $(B,η)$
consisting of an object $B$ of $\catB$ and and arrow $η:A→RB$ of
$\catA$ such that to every pair $(B',g)$ with $B'$ an object of
$\catB$ and $g:A→RB'$ an arrow of $\catA$, there is a unique arrow
$f:B→B'$ of $\catB$ with $Rf∘η=g$. In other words, every arrow $h$
to $R$ factors uniquely through the universal arrow $η$, as in the
commutative diagram:
%
$$\scalebox{0.8}{$
\diag{univ-arrow-cwm-my-letters}
$}
$$
\end{quotation}
The definition itself goes only up to the ``with $Rf∘η=g$.'', so let
me ignore the part starting from ``In other words'', and draw a better
``missing diagram'' for the definition:
%
$$\scalebox{0.8}{$
\diag{universal-arrow-stages}
$}
$$
}\def\colwidth{11cm}\anothercol{
% (find-books "__analysis/__analysis.el" "nakahira")
% (setq ee-includegraphics-dir "~/LATEX/2026jacobs/")
% (find-includegraphics-links "/tmp/nakahira-1.1.pdf")
% https://arxiv.org/pdf/2307.08891
Compare that with the diagram 1.1 from
Nakahira's ``Diagrammatic category theory''
(\url{https://arxiv.org/pdf/2307.08891}),
% (find-pdf-page "~/LATEX/2026jacobs/nakahira-1.1.pdf")
$$\includegraphics[width=10cm]{2026jacobs/nakahira-1.1.pdf}$$
\msk
and with my ``Poor man's cell diagrams'', from:
\url{https://anggtwu.net/LATEX/2026riehl.pdf}
\msk
The equation $η;Rf=g$ becomes:
$$\bmat{A \\ η \\ R \bmat{B \\ f \\ B'}} = \bmat{A \\ g \\ RB'}
$$
}}
%\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
%
%\end{document}
\newpage %-- fibred-equality
% «fibred-equality» (to ".fibred-equality")
% (jac2026p 4 "fibred-equality")
% (jac2026a "fibred-equality")
% (find-books "__cats/__cats.el" "jacobs" "190" "3.4. Fibred equality")
\slidebookmark{3.4 Fibred equality}
\SLIDE{Fibred equality}
\sa {<id,pi'>} {〈\id,π'〉}
\sa {IJ} {I×J}
\sa {KJ} {K×J}
\sa {IJJ} {(I×J)×J}
\sa {KJJ} {(K×J)×J}
\sa {EIJ} {\bbE_{I×J}}
\sa {EIJJ} {\bbE_{(I×J)×J}}
\sa {dd(I,J)} {{δ(I,J)}}
\sa {dd(K,J)} {{δ(K,J)}}
\sa {dd(I,J)*} {{δ(I,J)^*}}
\sa {dd(K,J)*} {{δ(K,J)^*}}
\sa {Eq(I,J)} {{\Eq(I,J)}}
\sa {Eq(K,J)} {{\Eq(K,J)}}
\sa {Eq_IJ} {{\Eq_{I,J}}}
\sa {Eq_KJ} {{\Eq_{K,J}}}
\sa {Ud(I,J)} {{\coprod_\ga{dd(I,J)}}}
\sa {UE(I,J)} {\mat{\ga {Eq_IJ} P =\\
\ga {Ud(I,J)} P }}
%D diagram p190-Eq
%D 2Dx 100 +65 +40 +60
%D 2D 100 A0 |-> A1 B0 |-> B1
%D 2D | | | |
%D 2D v v v v
%D 2D +30 A2 <-| A3 B2 <-| B3
%D 2D
%D 2D +20 EIJ <=> EIJJ
%D 2D +20 IJ --> IJJ IJ' --> IJJ'
%D 2D
%D ren A0 A1 ==> P \ga{UE(I,J)}
%D ren A2 A3 ==> \ga{dd(I,J)*}Q Q
%D ren IJ IJJ ==> \ga{IJ} \ga{IJJ}
%D ren EIJ EIJJ ==> \ga{EIJ} \ga{EIJJ}
%D
%D ren B0 B1 ==> P(i,j) j{=}j'∧P(i,j)
%D ren B2 B3 ==> Q(i,j,j) Q(i,j,j')
%D ren IJ' IJJ' ==> \ga{IJ} \ga{IJJ}
%D
%D (( A0 A1 |->
%D A2 A3 <-|
%D A0 A3 harrownodes nil 20 nil <->
%D A0 A2 ->
%D A1 A3 ->
%D
%D EIJ EIJJ -> sl^ .plabel= a \ga{Eq_IJ}=\ga{Ud(I,J)}
%D EIJ EIJJ <- sl_ .plabel= b \ga{dd(I,J)*}
%D IJ IJJ -> .plabel= a \ga{dd(I,J)}=\ga{<id,pi'>}
%D
%D B0 B1 |->
%D B2 B3 <-|
%D B0 B3 harrownodes nil 20 nil <->
%D B0 B2 ->
%D B1 B3 ->
%D
%D IJ' IJJ' -> .plabel= a (i,j)↦((i,j),j)
%D ))
%D enddiagram
\pu
\scalebox{0.9}{\def\colwidth{9cm}\firstcol{
\vspace*{0.1cm}
{\bf 3.4. Fibred equality}
(From {\cite[p.190]{Jacobs}}):
%
$$\diag{p190-Eq}
$$
}\anothercol{
}}
\newpage %-- BCC-equality
% «BCC-equality» (to ".BCC-equality")
% (jac2026p 99 "BCC-equality")
% (jac2026a "BCC-equality")
\SLIDE{Beck-Chevalley for equality}
%D diagram TP
%D 2Dx 100
%D 2D 100 B4
%D 2D ^
%D 2D |
%D 2D v
%D 2D +20 B6
%D 2D
%D 2D EKJJ
%D 2D
%D 2D +15 KJJ
%D 2D
%D ren B4 B6 ==> \ga{Eq(K,J)}{f'}^*P f^*\ga{Eq(I,J)}P
%D # ren EKJJ ==> \bbE_{(K×J)×J}
%D ren KJJ ==> (K×J)×J
%D
%D (( B4 B6 -> sl_ .plabel= l ♮
%D B4 B6 <- sl^ .plabel= r \BCCL
%D # EKJJ place
%D KJJ place
%D ))
%D enddiagram
\pu
\sa{width1}{9cm}
\sa{width2}{7cm}
\scalebox{0.6}{\def\colwidth{\ga{width1}}\firstcol{
{}
From \cite[p.191]{Jacobs}:
...the Beck-Chevalley condition holds: for each map $u:K→I$ in $\bbB$
(between the parameter objects) the canonical natural transformation
%
$$\ga{Eq(K,J)} (u×\id)^* \Longrightarrow ((u×\id)×\id)^* \ga{Eq(I,J)}$$
%
is an isomorphism.
\bsk
In the diagrams of the following pages we have $f' = u×\id$ and
$f = (u×\id)×\id$, so the canonical natural transformation above is:
%
$$T : \ga{Eq(K,J)} {f'}^* \Longrightarrow f^* \ga{Eq(I,J)}$$
If we apply it to an object $P$ we get the morphism
%
$$TP : \ga{Eq(K,J)} {f'}^* P \to f^* \ga{Eq(I,J)} P$$
in the fiber $\bbE_{(K×J)×J}$, that is drawn as `$♮$' in my diagrams
-- as in the column at the right.
}\def\colwidth{\ga{width2}}\anothercol{
{}
$$\scalebox{2.0}{$
\diag{TP}
$}
$$
}}
\sa {B0} {B0}
\sa {B1} {B1}
\sa {B2} {B2}
\sa {B2'} {B2'}
\sa {B3} {B3}
\sa {B4} {B4}
\sa {B5} {B5}
\sa {B6} {B6}
\sa {B7} {B7}
\sa {b0} {b0}
\sa {b1} {b1}
\sa {b2} {b2}
\sa {b3} {b3}
\sa {f} {f}
\sa {f'} {f'}
\sa {z} {z}
\sa {z'} {z'}
%D diagram BCCL-generic
%D 2Dx 100 +70 +70 +70
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ren B0 B1 ==> \ga{B0} \ga{B1}
%D ren B2 B2' B3 ==> \ga{B2} \ga{B2'} \ga{B3}
%D ren B4 B5 ==> \ga{B4} \ga{B5}
%D ren B6 B7 ==> \ga{B6} \ga{B7}
%D ren b0 b1 ==> \ga{b0} \ga{b1}
%D ren b2 b3 ==> \ga{b2} \ga{b3}
%D ((
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D ((
%D b0 b1 -> .plabel= b \ga{f'}
%D b0 b2 -> .plabel= l \ga{z'}
%D b1 b3 -> .plabel= r \ga{z}
%D b2 b3 -> .plabel= a \ga{f}
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
\pu
\sa {BCCL-equality-jacobs} {{
%
\sa {B1} {P}
\sa {B5} {\ga{Eq_IJ} P}
\sa {B7} {\ga{Eq_IJ} P}
\sa {B3} {z^* \ga{Eq_IJ} P}
\sa {B2'} {{f'}^* z^* \ga{Eq_IJ} P}
%
\sa {B6} {f^* \ga{Eq_IJ} P}
\sa {B2} {{z'}^* f^* \ga{Eq_IJ} P}
%
\sa {B0} {{f'}^* P}
\sa {B4} {\ga{Eq_KJ} {f'}^* P}
%
\sa {b0} {\ga{KJ}} \sa {b1} {\ga{IJ}}
\sa {b2} {\ga{KJJ}} \sa {b3} {\ga{IJJ}}
%
\sa {f'} {f' = u×\id}
\sa {z} {z = \ga{dd(I,J)}}
\sa {z'} {z' = \ga{dd(K,J)}}
\sa {f} {f = (u×\id)×\id}
%
\diag{BCCL-generic}
}}
\sa {BCCL-equality-edrx} {{
%
\sa {B1} {P(i,j)}
\sa {B5} {j{=}j' ∧ P(i,j)}
\sa {B7} {j{=}j' ∧ P(i,j)}
\sa {B3} {j{=}j ∧ P(i,j)}
\sa {B2'} {j{=}j ∧ P(u(k),j)}
%
\sa {B6} {j{=}j' ∧ P(u(k),j)}
\sa {B2} {j{=}j ∧ P(u(k),j)}
%
\sa {B0} {P(u(k),j)}
\sa {B4} {j{=}j' ∧ P(u(k),j)}
%
\sa {b0} {\ga{KJ}} \sa {b1} {\ga{IJ}}
\sa {b2} {\ga{KJJ}} \sa {b3} {\ga{IJJ}}
%
\sa {f'} { (k,j) ↦ (u(k),j)}
\sa {z} {\;\; (i,j) ↦ ((i,j),j)}
\sa {z'} { (k,j) ↦ ((k,j),j) \;\;}
\sa {f} {((k,j),j') ↦ ((u(k),j),j')}
%
\diag{BCCL-generic}
}}
\scalebox{0.58}{\def\colwidth{18cm}\firstcol{
\vspace*{-2cm}
$$\ga{BCCL-equality-jacobs}
$$
\bsk
$$\ga{BCCL-equality-edrx}
$$
\vspace*{-2cm}
}\anothercol{
}}
%D diagram BCCL-std
%D 2Dx 100 +45 +55 +45
%D 2D 100 B0 <====================== B1
%D 2D -\\ -\\
%D 2D | \\ | \\
%D 2D v \\ v \\
%D 2D +20 B2 <\\> B2' ============== B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ B4 \\ B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= f^{\prime*}P B1 .tex= P
%D B2 .tex= z^{\prime*}f^*Σ_zP B2' .tex= f^{\prime*}z^*Σ_zP B3 .tex= z^*Σ_zP
%D B4 .tex= Σ_{z'}f^{\prime*}P B5 .tex= Σ_zP
%D B6 .tex= f^*Σ_zP B7 .tex= Σ_zP
%D B0 B1 <-| B0 B2 -> B0 B2' -> B1 B3 -> B2 B2' <-> B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B5 B7 -> .plabel= r \id
%D B4 B6 -> sl_ .plabel= l ♮ B4 B6 <- sl^ .plabel= r \BCCL
%D B0 B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= X×_{Y}Z b1 .tex= Z b2 .tex= X b3 .tex= Y
%D b0 b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l z'
%D b1 b3 -> .plabel= r z
%D b2 b3 -> .plabel= a f
%D b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
\pu
$$\diag{BCCL-std}$$
\newpage
% «subset-types» (to ".subset-types")
% (jac2026p 8 "subset-types")
% (jac2026a "subset-types")
% (find-books "__cats/__cats.el" "jacobs" "272" "4.6. Subset types")
\slidebookmark{4.6 Subset types}
\SLIDE{Subset types}
\sa{(fullsubsettypes)}{\text{(full subset types)}}
\scalebox{0.55}{\def\colwidth{9cm}\firstcol{
From \cite[p.272]{Jacobs}:
\ga{(fullsubsettypes)}
%:
%: x:σ⊢φ:\Prop
%: -----------------------
%: ⊢\setofst{x:σ}{φ}:\Type
%:
%: ^st-formation
%:
%: b⠆B⊢P(b)⠆\Prop
%: -----------------------
%: ⊢\setofst{b⠆B}{P(b)}:\Type
%:
%: ^st-formation-edrx
%:
%:
%:
%: x:σ⊢φ:\Prop Γ⊢M:σ Γ\,|\,∅⊢φ[M/x]
%: ------------------------------
%: Γ⊢\sfi(M):\setofst{x:σ}{φ}
%:
%: ^st-introduction
%:
%: b⠆B⊢P(b)⠆\Prop a⠆A⊢f(a)⠆B a⠆A\,|\,∅⊢P(b)[b:=f(a)]
%: --------------------------------------
%: a⠆A⊢\sfi(f(a)):\setofst{b⠆B}{P(b)}
%:
%: ^st-introduction-edrx
%:
%:
%:
%: Γ⊢N:\setofst{x:σ}{φ}
%: --------------------
%: Γ⊢\sfo(N):σ
%:
%: ^st-elim-1
%:
%: a⠆A⊢b'⠆\setofst{b⠆B}{P(b)}
%: --------------------
%: a⠆A⊢\sfo(b')⠆B
%:
%: ^st-elim-1-edrx
%:
%:
%:
%: Γ,x:σ\,|\,Θ,φ⊢ψ
%: ----------------------------------------------
%: Γ,y:\setofst{x:σ}{φ}\,|\,Θ[\sfo(y)/x]⊢ψ[\sfo(y)/x]
%:
%: ^st-elim-2
%:
%: a⠆A,b⠆B\,|\,Q(a,b),P(b)⊢R(a,b)
%: ---------------------------------------------------
%: a⠆A,b'⠆\setofst{b⠆B}{P(b)}\,|\,Q(a,b)[b:=\sfo(b')]⊢R(a,b)[b:=\sfo(b')]
%:
%: ^st-elim-2-edrx
%:
%:
\pu
$$\ded{st-formation}$$
$$\ded{st-formation-edrx}$$
$$\ded{st-introduction}$$
$$\ded{st-introduction-edrx}$$
$$\ded{st-elim-1}$$
$$\ded{st-elim-1-edrx}$$
$$\text{with} \quad \ded{st-elim-2}$$
$$\text{with} \quad \ded{st-elim-2-edrx}$$
}\anothercol{
}}
\newpage
% ;-- writetoc
% «writetoc» (to ".writetoc")
\directlua{toclines:writetoc()}
% Writes in: (find-LATEXfile "2026jacobs.mytoc")
% See: (to "toc")
% ;-- references
% «references» (to ".references")
\printbibliography
% ;-- write-dnt-file
% «write-dnt-file» (to ".write-dnt-file")
% (find-fline "~/LATEX/" "2026jacobs.dnt")
% (find-fline "~/LATEX/2026jacobs.dnt")
%L write_dnt_file ("2026jacobs.dnt")
\pu
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% (find-pdfpages2-links "~/LATEX/" "2026jacobs")
% ;-- make-with-bib
% «make-with-bib» (to ".make-with-bib")
% (wiya "make-with-bib")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/LATEX/
# which biber
# biber --version
make -f 2019.mk STEM=2026jacobs veryclean
lualatex 2026jacobs.tex
biber 2026jacobs
lualatex 2026jacobs.tex
# (find-pdf-page "~/LATEX/2026jacobs.pdf")
% Local Variables:
% coding: utf-8-unix
% outline-regexp: "% +;--"
% ee-tla: "jac"
% ee-tla: "jac2026"
% End: