% (find-LATEX "2026vdepaiva.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2026vdepaiva.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2026vdepaiva.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2026vdepaiva.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2026vdepaiva.pdf"))
% (defun e () (interactive) (find-LATEX "2026vdepaiva.tex"))
% (defun o () (interactive) (find-LATEX "2026vdepaiva.tex"))
% (defun u () (interactive) (find-latex-upload-links "2026vdepaiva"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2026vdepaiva.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun oe () (interactive) (find-2a '(o) '(e)))
%          (code-eec-LATEX "2026vdepaiva")
% (find-pdf-page   "~/LATEX/2026vdepaiva.pdf")
% (find-sh0 "cp -v  ~/LATEX/2026vdepaiva.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2026vdepaiva.pdf /tmp/pen/")
%     (find-xournalpp "/tmp/2026vdepaiva.pdf")
%   file:///home/edrx/LATEX/2026vdepaiva.pdf
%               file:///tmp/2026vdepaiva.pdf
%           file:///tmp/pen/2026vdepaiva.pdf
%  http://anggtwu.net/LATEX/2026vdepaiva.pdf
% https://anggtwu.net/LATEX/2026vdepaiva.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps   "Caepro5 Piecewise2 Maxima2 DiagForth1")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2026vdepaiva" "2" "vdp2026" "vdp")

% «.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")
%
% «.title»			(to "title")
% «.toc»			(to "toc")
% «.links»			(to "links")
% «.proposition-1»		(to "proposition-1")
% «.proposition-1-compat»	(to "proposition-1-compat")
% «.proposition-1-basic»	(to "proposition-1-basic")
% «.proposition-1-imp»		(to "proposition-1-imp")
%
% «.writetoc»			(to "writetoc")
% «.references»			(to "references")

% ;-- 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)
\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

% «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\P#1{\left(#1\right)}

%L require "DiagForth1"  -- (find-angg "LUA/DiagForth1.lua")
\pu

%L forths["-"] = function () pusharrow("-") end
\pu


% ;-- title
%  _____ _ _   _                               
% |_   _(_) |_| | ___   _ __   __ _  __ _  ___ 
%   | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
%   | | | | |_| |  __/ | |_) | (_| | (_| |  __/
%   |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
%                      |_|          |___/      
%
% «title»  (to ".title")
% (vdp2026p 1 "title")
% (vdp2026a   "title")

\thispagestyle{empty}

\begin{center}

\vspace*{1.2cm}

\par {\bf \Large Notes on Valeria de Paiva's}
\par \ssk
\par {\bf \Large Tecnhical Report (1991)}

\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")
% (vdp2026p 2 "links")
% (vdp2026a   "links")

%{\bf Links}
%
%\scalebox{0.6}{\def\colwidth{16cm}\firstcol{
%}\anothercol{
%}}


%L forths["ab!"] = function ()
%L     node_a = ds:pick(1)
%L     node_b = ds:pick(0)
%L   end
%L forths["abc!"] = function ()
%L     node_a = ds:pick(2)
%L     node_b = ds:pick(1)
%L     node_c = ds:pick(0)
%L   end
%L forths["a@"]   = function () ds:push(node_a) end
%L forths["b@"]   = function () ds:push(node_b) end
%L forths["c@"]   = function () ds:push(node_c) end
%L forths["ab@"]  = function () dxyrun "a@ b@" end
%L forths["<-|-"] = function () dxyrun "ab! ab@ <- .plabel= m \\scriptscriptstyle| ab@ <-" end
%L forths["\\'"]  = function () dxyrun "abc!  a@ c@ -  a@ c@ midpoint .TeX= {} b@ ->" end
%L
%L forthe["\\'-name:"] = "w"
%L forths["\\'-name:"] = function (TeX)
%L     dxyrun "\\'"
%L     dxyrun "b@ c@ midpoint"
%L     forths["relplace"](-4,0,TeX)
%L   end

\newpage
% ;-- proposition-1
% «proposition-1»  (to ".proposition-1")
% (vdp2026p 99 "proposition-1")
% (vdp2026a    "proposition-1")

\SLIDE{Proposition 1}

%D diagram Prop-1
%D 2Dx     100 +30  +25 +30
%D 2D  100 A0  A1   B0  B1
%D 2D
%D 2D  +30 A2  A3
%D 2D
%D 2D  +30 A4  A5   B4  B5
%D 2D
%D ren A0 A1 A2 A3 A4 A5 ==> U X V Y W Z
%D ren B0 B1       B4 B5 ==> U X     W Z
%D
%D (( A0 A1 <-|- .plabel= a α
%D    A2 A3 <-|- .plabel= a β
%D    A4 A5 <-|- .plabel= a γ
%D    A0 A2 ->   .plabel= l f
%D    A2 A4 ->   .plabel= l g
%D    A0 A1 A3   \'-name: F
%D    A2 A3 A5   \'-name: G
%D    
%D    B0 B1 <-|- .plabel= a α
%D    B4 B5 <-|- .plabel= a γ
%D    B0 B4 ->   .plabel= l h
%D    B0 B1 B5   \'-name: H
%D ))
%D enddiagram
\pu


\scalebox{0.55}{\def\colwidth{10cm}\firstcol{

Proposition 1, p.4,

a.k.a: ``composition needs checking''.

\msk

Lets suppose that we are in $\Set$.

Let's omit the types when they can be inferred from the diagrams, {\sl
  and let's use dependent variables.}

\msk

So $A≡(U,X,α)$ is a triple

$(U∈\Sets,X∈\Sets,α:U×X→\{0,1\})$,

So $B≡(V,Y,β)$ is a triple

$(V∈\Sets,Y∈\Sets,β:V×Y→\{0,1\})$,

\msk

and a morphism $(f,F):A→B$

is actually a triple
%
$$\pmat{f:U→V, \\ F:U×Y→X, \\ [∀(u,y).α→β]:\ldots}$$

in which the $[∀(u,y).α→β]$ is a guarantee/witness for:
%
$$\begin{array}{l}
  ∀(u,y).α→β \\
  ≡ \; ∀(u,y).α(u,x)→β(v,y) \\
  ≡ \; ∀(u,y).α(u,x(u,y))→β(v(u),y) \\
  ≡ \; ∀(u,y).α(u,F(u,y))→β(f(u),y) \\
  \end{array}
$$

}\anothercol{

$$\scalebox{1.5}{$
  \diag{Prop-1}
  $}
$$

\bsk
\bsk

We want to compose the

$(f,F,[∀(u,y).α→β])$ with the

$(g,G,[∀(v,z).β→γ])$,

and obtain a:
%
$$(h,H,[∀(u,z).α→γ]).$$

}}



\newpage
% ;-- proposition-1-compat
% «proposition-1-compat»  (to ".proposition-1-compat")
% (vdp2026p 4 "proposition-1-compat")
% (vdp2026a   "proposition-1-compat")

\SLIDE{Proposition 1: compatibility conditions}

%D diagram Prop-1-compat
%D 2Dx     100 +30  +25 +30
%D 2D  100 A0  A1   B0  B1
%D 2D
%D 2D  +30 A2  A3
%D 2D
%D 2D  +30 A4  A5   B4  B5
%D 2D
%D ren A0 A1 A2 A3 A4 A5 ==> U X V Y W Z
%D ren B0 B1       B4 B5 ==> U X     W Z
%D
%D (( # A0 A1 <-|- .plabel= a α
%D    # A2 A3 <-|- .plabel= a β
%D    # A4 A5 <-|- .plabel= a γ
%D    A0 A2 ->   .plabel= l f
%D    A2 A4 ->   .plabel= l g
%D    A0 A1 A3   \'-name: F
%D    A2 A3 A5   \'-name: G
%D    
%D    # B0 B1 <-|- .plabel= a α
%D    # B4 B5 <-|- .plabel= a γ
%D    B0 B4 ->   .plabel= l h
%D    B0 B1 B5   \'-name: H
%D ))
%D enddiagram
\pu

\sa {body:....wz} {\phantom{a}\\\phantom{a}\\w&z}
\sa {body:..v..z} {\phantom{a}\\v&\\&z}
\sa {body:..vy..} {\phantom{a}\\v&y\\\phantom{a}}
\sa {body:..vywz} {\phantom{a}\\v&y\\w&z}
\sa {body:u....z} {u&\\\phantom{a}\\&z}
\sa {body:u..y..} {u&\\&y\\\phantom{a}}
\sa {body:ux....} {u&x\\\phantom{a}\\\phantom{a}}
\sa {body:ux..wz} {u&x\\\phantom{a}\\w&z}
\sa {body:uxvy..} {u&x\\v&y\\\phantom{a}}
\sa {body:uxvywz} {u&x\\v&y\\w&z}

\sa {(..vy..)} {\psm{\ga{body:..vy..}}}
\sa {(....wz)} {\psm{\ga{body:....wz}}}
\sa {(..v..z)} {\psm{\ga{body:..v..z}}}
\sa {(..vywz)} {\psm{\ga{body:..vywz}}}
\sa {(u....z)} {\psm{\ga{body:u....z}}}
\sa {(u..y..)} {\psm{\ga{body:u..y..}}}
\sa {(ux....)} {\psm{\ga{body:ux....}}}
\sa {(ux..wz)} {\psm{\ga{body:ux..wz}}}
\sa {(uxvy..)} {\psm{\ga{body:uxvy..}}}
\sa {(uxvywz)} {\psm{\ga{body:uxvywz}}}

\sa {big(..vy..)} {\pmat{\ga{body:..vy..}}}
\sa {big(....wz)} {\pmat{\ga{body:....wz}}}
\sa {big(..v..z)} {\pmat{\ga{body:..v..z}}}
\sa {big(..vywz)} {\pmat{\ga{body:..vywz}}}
\sa {big(u....z)} {\pmat{\ga{body:u....z}}}
\sa {big(u..y..)} {\pmat{\ga{body:u..y..}}}
\sa {big(ux....)} {\pmat{\ga{body:ux....}}}
\sa {big(ux..wz)} {\pmat{\ga{body:ux..wz}}}
\sa {big(uxvy..)} {\pmat{\ga{body:uxvy..}}}
\sa {big(uxvywz)} {\pmat{\ga{body:uxvywz}}}

\sa {{..vy..}} {\csm{\ga{body:..vy..}}}
\sa {{....wz}} {\csm{\ga{body:....wz}}}
\sa {{..v..z}} {\csm{\ga{body:..v..z}}}
\sa {{..vywz}} {\csm{\ga{body:..vywz}}}
\sa {{u....z}} {\csm{\ga{body:u....z}}}
\sa {{u..y..}} {\csm{\ga{body:u..y..}}}
\sa {{ux....}} {\csm{\ga{body:ux....}}}
\sa {{ux..wz}} {\csm{\ga{body:ux..wz}}}
\sa {{uxvy..}} {\csm{\ga{body:uxvy..}}}
\sa {{uxvywz}} {\csm{\ga{body:uxvywz}}}

\scalebox{0.55}{\def\colwidth{8.5cm}\firstcol{

Let's forget $α$, $β$ and $γ$ for a while,

and let's consider $f$, $F$, $g$ and $G$ as

compatibility conditions...

\msk

I will write $\psm{u,&x, \\ v,&y, \\ w,&z}$, \standout{with} commas,

for a tuple that only obeys

$u∈U$, $x∈X$, $\ldots$, $z∈Z$,

and will write $\psm{u&x \\ v&y \\ w&z}$, \standout{without} commas,

for $\psm{u,&x, \\ v,&y, \\ w,&z}$ plus guarantees for the

``obvious'' compatibility conditions,

that in this case are:
%
$$\begin{array}{l}
    [v=v(u)],   \\{}
    [x=x(u,y)], \\{}
    [w=w(v)],   \\{}
    [y=y(v,z)]  \\
  \end{array}
  \quad
  \text{i.e.,}
  \quad
  \begin{array}{l}
    [v=f(u)],   \\{}
    [x=F(u,y)], \\{}
    [w=g(v)],   \\{}
    [y=G(v,z)]  \\
  \end{array}
$$

So:

\ssk\par $\ga{(uxvywz)}$ has 4 compatibility conditions,
\ssk\par $\ga{(uxvy..)}$ has 2 compatibility conditions,
\ssk\par $\ga{(..vywz)}$ has 2 compatibility conditions,
\ssk\par $\ga{(u..y..)}$ has 0 compatibility conditions...


}\def\colwidth{12cm}\anothercol{

$$\scalebox{1.5}{$
  \diag{Prop-1-compat}
  $}
$$

\bsk
\bsk

...and $\ga{(ux..wz)}$ has these compatibility conditions:
%
$$\begin{array}{rcl}
  w &=& w(v(u)) \\
    &=& g(f(u)) \\\\[-5pt]
  x &=& x(u,y) \\
    &=& x(u,y(v,z)) \\
    &=& x(u,y(v(u),z)) \\
    &=& F(u,G(f(u),z)) \\
  \end{array}
$$

}}




\newpage
% ;-- proposition-1-basic
% «proposition-1-basic»  (to ".proposition-1-basic")
% (vdp2026p 99 "proposition-1-basic")
% (vdp2026a    "proposition-1-basic")

\SLIDE{Proposition 1: basic pullbacks}


%D diagram prop-1-basic
%D 2Dx     100 +30 +30 +30
%D 2D  100     A1  A2  A3
%D 2D
%D 2D  +25 B0  B1      B3
%D 2D
%D 2D  +25     C1  C2  C3
%D 2D
%D ren    A1 A2 A3 ==>               \ga{{u..y..}} \ga{{uxvy..}} \ga{{ux....}}
%D ren B0 B1    B3 ==> \ga{{u....z}} \ga{{uxvywz}}               \ga{{..vy..}}
%D ren    C1 C2 C3 ==>               \ga{{..v..z}} \ga{{..vywz}} \ga{{....wz}}
%D
%D (( A1 A2 <-> A2 A3 ->
%D    B0 B1 <->
%D    C1 C2 <-> C2 C3 ->
%D    B1 A2  -> A2 B3 ->
%D    B1 C2  -> C2 B3 ->
%D ))
%D enddiagram
\pu


\scalebox{0.65}{\def\colwidth{6cm}\firstcol{

Now let's write $\ga{{uxvywz}}$

for the space of all (compatible)

tuples of the form $\ga{(uxvywz)}$,

and do the same for all other

combinations of letters...

\bsk

We have the maps at the right,

and the diamond at the middle

is a pullback.

\bsk

Note that:

$α$ is defined on $\ga{{ux....}}$,

$β$ is defined on $\ga{{..vy..}}$,

$γ$ is defined on $\ga{{....wz}}$,

$α→β$ is defined on $\ga{{u..y..}}$,

$β→γ$ is defined on $\ga{{..v..z}}$, and

$α→γ$ is defined on $\ga{{u....z}}$...

}\def\colwidth{10cm}\anothercol{

$$\scalebox{1.5}{$
  \diag{prop-1-basic}
  $}
$$


}}



\newpage
% ;-- proposition-1-imp
% «proposition-1-imp»  (to ".proposition-1-imp")
% (vdp2026p 99 "proposition-1-imp")
% (vdp2026a    "proposition-1-imp")

\SLIDE{Proposition 1: the implication}


\scalebox{0.7}{\def\colwidth{8cm}\firstcol{

$$\scalebox{1.0}{$
  \diag{Prop-1}
  $}
$$

\bsk
\bsk

Remember that want to compose the

$(f,F,[∀(u,y).α→β])$ with the

$(g,G,[∀(v,z).β→γ])$,

and obtain a:
%
$(h,H,[∀(u,z).α→γ]).$

\msk

We saw that

$h(u) = g(f(u))$ and

$H(u,z) = F(u,G(f(u),z))$.


}\anothercol{

We still need to check this:

\msk

$\pmat{ \P{∀\ga{(u..y..)}.α→β} & ∧ \\\\[-9pt]
        \P{∀\ga{(..v..z)}.β→γ} \\
      } →$

\ssk

$\;\;\;\, \P{∀\ga{(u....z)}.α→γ}$

\bsk
\bsk

Sketch of the proof:
%
%:
%:    ∀\ga{(u..y..)}.α→β    ∀\ga{(..v..z)}.β→γ
%:    ------------------    ------------------
%:    ∀\ga{(uxvy..)}.α→β    ∀\ga{(..vywz)}.β→γ
%:    ------------------    ------------------
%:    ∀\ga{(uxvywz)}.α→β    ∀\ga{(uxvywz)}.β→γ
%:    ----------------------------------------
%:           ∀\ga{(uxvywz)}.α→γ
%:           ------------------
%:           ∀\ga{(u....z)}.α→γ
%:
%:           ^prop-1-imp
%:
\pu
$$\ded{prop-1-imp}$$

}}













% ;-- writetoc
% «writetoc»  (to ".writetoc")
\directlua{toclines:writetoc()}
% Writes in: (find-LATEXfile "2026vdepaiva.mytoc")
% See: (to "toc")

% ;-- references
% «references»  (to ".references")
%\printbibliography

% ;-- write-dnt-file
% «write-dnt-file»  (to ".write-dnt-file")
% (find-fline "~/LATEX/" "2026vdepaiva.dnt")
% (find-fline    "~/LATEX/2026vdepaiva.dnt")
%L write_dnt_file       ("2026vdepaiva.dnt")
\pu


\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

% (find-pdfpages2-links "~/LATEX/" "2026vdepaiva")


% Local Variables:
% coding: utf-8-unix
% outline-regexp: "% +;--"
% ee-tla: "vdp"
% ee-tla: "vdp2026"
% End: