% (find-LATEX "2021excuse.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record --synctex=1 2021excuse.tex" :end))
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2021excuse.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2021excuse.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2021excuse.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2021excuse.pdf"))
% (defun e () (interactive) (find-LATEX "2021excuse.tex"))
% (defun l () (interactive) (find-LATEX "2021excuse.lua"))
% (defun h () (interactive) (find-angg "HASKELL/2021excuse.hs"))
% (defun u () (interactive) (find-latex-upload-links "2021excuse"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (find-pdf-page   "~/LATEX/2021excuse.pdf")
% (find-xournalpp  "~/LATEX/2021excuse.pdf")
% (find-sh0 "cp -v  ~/LATEX/2021excuse.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2021excuse.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2021excuse.pdf
%               file:///tmp/2021excuse.pdf
%           file:///tmp/pen/2021excuse.pdf
% http://angg.twu.net/LATEX/2021excuse.pdf
% (find-LATEX "2019.mk")
%
% (find-lualatex-links "2021excuse")

% https://mail.google.com/mail/ca/u/0/#search/categorias+type+theory/KtbxLwGnRQxDGgTltXvbZjZCHvkdspPvlB

% «.defs»			(to "defs")
% «.co»				(to "co")
% «.verbatim»			(to "verbatim")
% «.title-page»			(to "title-page")
% «.rings»			(to "rings")
% «.rings-2»			(to "rings-2")
% «.conventions-CT-1»		(to "conventions-CT-1")
% «.downcasing»			(to "downcasing")
% «.downcasing-2»		(to "downcasing-2")
% «.term-inf-proof-search»	(to "term-inf-proof-search")
% «.haskell»			(to "haskell")
%
% «.universals-CWM-orig»	(to "universals-CWM-orig")
% «.universals-defs»		(to "universals-defs")
% «.universals-CWM»		(to "universals-CWM")
% «.universals-my-letters»	(to "universals-my-letters")
% «.universals-rings»		(to "universals-rings")
%
% «.internal-views»		(to "internal-views")
% «.functors»			(to "functors")
% «.functor-2»			(to "functor-2")
% «.functor-3»			(to "functor-3")
% «.functor-4»			(to "functor-4")
% «.NTs»			(to "NTs")
% «.NTs-2»			(to "NTs-2")
% «.NTs-3»			(to "NTs-3")
% «.yoneda»			(to "yoneda")
% «.kan»			(to "kan")
%
% «.intro-TT»			(to "intro-TT")
% «.untyped-lambda»		(to "untyped-lambda")
% «.types-after-discrete»	(to "types-after-discrete")

% «.dependent-types»		(to "dependent-types")
% «.typing-and-and-implies»	(to "typing-and-and-implies")
% «.typing-forall-and-exists»	(to "typing-forall-and-exists")
%
% «.marsden»			(to "marsden")
%
% «.type-inference»		(to "type-inference")
% «.typing»			(to "typing")
% «.intro-to-the-hard-part»	(to "intro-to-the-hard-part")
% «.some-references»		(to "some-references")
% «.contexts»			(to "contexts")
% «.PTSs»			(to "PTSs")
% «.PTSs-2»			(to "PTSs-2")
% «.judgments»			(to "judgments")
%
% «.guessing-nu-CWM-1»		(to "guessing-nu-CWM-1")
% «.guessing-nu-1»		(to "guessing-nu-1")
% «.guessing-nu-2»		(to "guessing-nu-2")
% «.guessing-nu-2-diag»		(to "guessing-nu-2-diag")

\documentclass[oneside]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{stmaryrd}
\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")
\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex" "defub")
%
\usepackage[backend=biber,
   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\usepackage[paperwidth=11.5cm, paperheight=9cm,
            %total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            %a4paper,
            top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
           ]{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




% «defs»  (to ".defs")
% (find-LATEX "edrx15.sty" "colors-2019")
\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}
\long\def\ColorOrange#1{{\color{orange}#1}}
\long\def\ColorBrown #1{{\color{brown}#1}}

\catcode`«=13 \def«{\llangle}
\catcode`»=13 \def»{\rrangle}

\def\univ{\text{(univ)}}
\def\nameof#1{\ulcorner#1\urcorner}
\def\Rings{\mathbf{Rings}}

\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
\def\smile{\ensuremath{{=})}}
\def\frown{\ensuremath{{=}(}}
\def\smirk{\ensuremath{{=}/}}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}}
\def\ue#1{\und{#1}{expr}}
\def\uC#1{\und{#1}{context}}
\def\uCH#1{\und{#1}{context / hypotheses}}
\def\uvt#1{\und{#1}{v:T}}
\def\uterm#1{\und{#1}{term}}
\def\utype#1{\und{#1}{type}}
\def\uconc#1{\und{#1}{conclusion}}

\def\setofst#1#2{\{\,#1\;|\;#2\,\}}
\def\setofsc#1#2{\{\,#1\;;\;#2\,\}}

% pos-spec colors
% (find-es "tex" "xcolor")
% (find-xcolorpage 17 "2.4       Predefined colors")
% (find-xcolortext 17 "2.4       Predefined colors")
\def\Cnum#1{{\color{magenta}#1}}
\def\Cnum#1{{\color{Red1}#1}}
\def\Cnum#1{{\color{violet}#1}}
\def\Cnum#1{{\color{orange}#1}}
\def\Cstr#1{{\color{violet}#1}}
\def\Cstr#1{{\color{Red1}#1}}
\def\Csex#1{{\color{Red1}#1}}

\def\pdiag#1{\left(\diag{#1}\right)}

% «co»  (to ".co")
% (find-es "tex" "co")
% \co: a low-level way to typeset code; a poor man's "\verb"
\def\cocolor{}
\def\cocolor{\color{DarkGreen!80!black}}
\def\co#1{{%
  \cocolor%
  \def\%{\char37}%
  \def\\{\char92}%
  \def\^{\char94}%
  \def\~{\char126}%
  \tt#1%
  }}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
\def\pco#1{\par\co{#1}}

% «verbatim»  (to ".verbatim")
% (find-angg "LUA/Verbatim1.lua" "Verbatim")
%\directlua{dofile "2021excuse.lua"}   % (find-LATEX "2021excuse.lua")
\def\myhbox#1#2#3{\setbox0=\hbox{#3}\ht0=#1\dp0=#2\box0}
\def\verbahbox#1{\hbox{\tt#1}}
\def\verbahbox#1{\myhbox{7pt}{2pt}{{\tt#1}}}

% (find-dednat6 "tug-slides.tex" "bgcolorhbox")
\def\bgcolorhbox#1#2{{%
  \setbox0\hbox{#2}%
  \setbox0\vbox{\vskip\fboxsep\box0\vskip\fboxsep}%
  \setbox0\hbox{\kern\fboxsep\box0\kern\fboxsep}%
  {\color{#1}{\smashedvrule{\wd0}{\ht0}{\dp0}}}%
  \box0%
  }}
\def\bgbox#1{\bgcolorhbox{YellowOrangeLight}{#1}}

\def\myvcenter#1{\begin{matrix}#1\end{matrix}}
\catcode`\^^O=13 \def{{\color{red}*}}




% From:
% (find-LATEX "2018-1-LA-material.tex" "defs")

\def\tabl#1{\begin{tabular}{l}#1\end{tabular}}
\def\tablt#1{\begin{tabular}[t]{l}#1\end{tabular}}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}

\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\ren{\operatorname{ren}}
\def\app{\operatorname{app}}
\def\pair{\operatorname{pair}}

\def\cur{\mathsf{cur}}
\def\uncur{\mathsf{uncur}}
\def\ren{\mathsf{ren}}
\def\app{\mathsf{app}}
\def\pair{\mathsf{pair}}

\def\Ran{\mathsf{Ran}}
\def\Dn   {\Downarrow}

% \def∧{\&}

\def\namedfunction#1#2#3#4#5{
  \begin{array}{rrcl}
    #1: & #2 & → & #3 \\
        & #4 & ↦ & #5 \\
  \end{array}
  }

\def\IPLai{\text{IPL}_{{∧}{→}}}
\def\NDai {\text{ND} _{{∧}{→}}}



%\noedrxfooter % (find-LATEX "edrxheadfoot.tex")

\def\drafturl{http://angg.twu.net/LATEX/2020-1-C2.pdf}
\def\drafturl{http://angg.twu.net/math-b.html\#2021-excuse-tt}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}

\setlength{\parindent}{0em}


%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page»  (to ".title-page")
% (excp 1 "title-page")
% (exca   "title-page")
% (ecop 1 "title-page")
% (eco    "title-page")

\thispagestyle{empty} % (find-es "tex" "thispagestyle")

\begin{center}

\begin{tabular}{c}
\phantom{a}\\[-15pt]
{\Large {\bf Category Theory}} \\[1pt]
{\Large {\bf as An Excuse to}} \\[1pt]
{\Large {\bf Learn Type Theory}} \\[0pt]
\ColorGray{(talk @ Encontro de Categorias 2021)}\\[-5pt]
{\tiny\url{http://angg.twu.net/math-b.html#2021-excuse-tt}}\\[8pt]
\end{tabular}

\begin{tabular}[c]{r}
  By: \\
  Eduardo Ochs $→$ \\
  \ColorGray{(main author)} \\
  \\
  Selana Ochs $→$ \\
  \ColorGray{(friend and coauthor)} \\
  \\
  \\
\end{tabular}
  \!\!\!\!\!\!\!
\begin{tabular}[c]{c}
  $\includegraphics[height=100pt]{2021excuse-selana1.jpg}$
\end{tabular}
\phantom{mm}

% \msk
% \url{http://angg.twu.net/\#eev}

\end{center}

\newpage

% «rings»  (to ".rings")
% (excp 2 "rings")
% (exca   "rings")

{\bf Rings}

\ssk

A ring $R$ is a tuple $(R,0,1,+,-,·)$ in which:

\ssk

$\begin{array}{ccl}
 R & \text{is} & \text{a set}, \\
 0 & \in & R, \\
 1 & \in & R, \\
 + & : & R×R→R, \\
 - & : & R→R, \\
 · & : & R×R→R \\
 \end{array}
$

\ssk

and this $(R,0,1,+,-,·)$ obeys several conditions.

The part $(R,0,1,+,-,·)$ is called \ColorRed{structure},

and the conditions are called \ColorRed{properties}.

\msk

(For more on structure and properties

see\cite[section 7.5]{FavC}, \cite[p.15]{BaezShulman2007}).

% (favp 39 "ness")
% (fav     "ness")

\newpage

% «rings-2»  (to ".rings-2")
% (excp 3 "rings-2")
% (exca   "rings-2")

{\bf Rings (2)}

\ssk

The symbols $0,1,+,-,·$ in $(R,0,1,+,-,·)$ have

standard conventions that let us infer their

arities, types, and equations --- what they have

to obey to ``deserve their names''.

\msk

Also, if $f:R→S$ is a morphism of rings then

$f$ is a function from the underlying set of $R$

to the underlying set of $S$ that obeys several

equations --- for example $f(a+b)=f(a)+f(b)$,

that is actually
%
$$∀a,b∈R.\,f(a +_R b) = f(a) +_S f(b) \; ...$$

These things can be written in several levels of detail.

\newpage

% «conventions-CT-1»  (to ".conventions-CT-1")
% (excp 4 "conventions-CT-1")
% (exca   "conventions-CT-1")

{\bf Conventions in Category Theory}

\ssk

Category Theory is like that too, only much, much worse.

The notation changes a lot from one text to the other.

Most diagrams are left to the reader.

Some parts of the \ColorRed{structure} are left to the reader too...

For example (see \cite[section 3]{FavC}):

\msk

Fix a set $A$. Let $(A×)$ be \ColorRed{the} functor that takes

each object $B$ to $A×B$.

\msk

This says that the \ColorRed{action on objects} of the functor $(A×)$
is $(A×)_0(B) = A×B$, and the ``\ColorRed{the}'' implies that the
reader knows how to discover that the action on morphisms is:
%
$$(A×)_1(B \ton{f} C) = A×B \xton{〈π,f∘π'〉} A×C.$$

% (favp 11 "to-deserve-a-name")
% (fav     "to-deserve-a-name")


\newpage

% «downcasing»  (to ".downcasing")
% (excp 5 "downcasing")
% (exca   "downcasing")

{\bf A weird idea: downcasing}

\ssk

This looked very natural to me when I was starting to learn

CT and Haskell by myself... it is great as an \ColorRed{informal} tool.

\ssk

Btw, the paper \cite{IDARCT} is about how I tried to formalize

this idea for years, failed miserably, and then found a way

to use it for ``skeletons of proofs''.
%
%D diagram ??
%D 2Dx     100 +20 +30 +25
%D 2D  100 A0  B0  B1  C0
%D 2D
%D 2D  +25 A1  B2  B3  C1
%D 2D
%D 2D  +20     D0  D1
%D 2D
%D ren A0 B0 B1 C0 ==> b B A{×}B (a,b)
%D ren A1 B2 B3 C1 ==> c C A{×}C (a,c)
%D ren    D0 D1    ==>  \Set \Set
%D
%D (( A0 A1 |->
%D    B0 B1 |->
%D    B0 B2  -> .plabel= l f
%D    B1 B3  -> .plabel= r A{×}f
%D    B0 B3 harrownodes nil 20 nil |->
%D    B2 B3 |->
%D    C0 C1 |->
%D    D0 D1  -> .plabel= a (A{×})
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
  \qquad
  \scalebox{0.9}{$
  \begin{array}{l}
  (a,b) \mapsto (a,c) \\
   ≡ (a,b) \mapsto (a,f(b)) \\
   ≡ (a,b) \mapsto (π(a,b),f(π'(a,b))) \\
   ≡ p \mapsto (πp, f(π'p)) \\
   ≡ p \mapsto (π(p), (f∘π')(p)) \\
   ≡ p \mapsto 〈π,f∘π'〉(p) \\
   ≡ 〈π,f∘π'〉 \\
  \end{array}
  $}
$$



\newpage

% «downcasing-2»  (to ".downcasing-2")
% (excp 6 "downcasing-2")
% (exca   "downcasing-2")

{\bf A weird idea: downcasing (2)}

\ssk

Downcasing and upcasing are like

lowercasing and uppercasing, but for terms and types.

\ssk

Downcasing a set gives us a name for \ColorRed{a}

``typical element'' of that set.

Downcasing a type gives us a name for a variable of that type.

\def\CO#1{\ColorOrange{\text{#1}}}

\msk

$\begin{array}{rcll}
               a     &:& A       & \CO{(ok)} \\
               a'    &:& A'      & \CO{(ok)} \\
               a'    &:& A       & \CO{(ok when there's no $A'$)} \\
               b     &:& B       & \CO{(ok)} \\
            (a,b)    &:& A×B     & \CO{(ok?)} \\
     b \mapsto c     &:& B→C     & \CO{(weird)} \\
 (a,b) \mapsto (a,c) &:& A×B→A×C & \CO{(weird)} \\
 \end{array}
$


\newpage

% «term-inf-proof-search»  (to ".term-inf-proof-search")
% (excp 7 "term-inf-proof-search")
% (exca   "term-inf-proof-search")

{\bf Term inference is like proof search}

\ssk

Finding \ColorRed{the} meaning of $A×f$

means finding \ColorRed{a} natural construction

for $\ColorRed{?}:A×B→A×C$ from $f:B→C$...

\ssk

``Natural constructions'' are $λ$-terms.

This is a bit quirky. Details: \cite[section 3]{FavC}.

Main diagrams:

\msk

%L addabbrevs("|->", "\\mapsto ")
%:
%:                           [(a,b)]^1                       p
%:                           ---------                      ---
%:                [(a,b)]^1      b        b|->c    [p]^1    π'p       f
%:                ---------      -------------     -----    -----------
%:                    a                 c          πp          f(π'p)
%:                    -------------------          -------------------
%:     b|->c               (a,c)                        (πp,f(π'p))
%:  =============      -------------1                  --------------1
%:  (a,b)|->(a,c)      (a,b)|->(a,c)                   λp.(πp,f(π'p))
%:
%:  ^nc-1              ^nc-2                            ^nc-3
%:
%:
\pu
$\scalebox{0.9}{$
 \ded{nc-1} \squigto \ded{nc-2} \squigto \;\;\; \ded{nc-3}
 $}
$

% (favp 11 "to-deserve-a-name")
% (fav     "to-deserve-a-name")

\newpage

%:
%:
%:                                     [P∧Q]^1
%:                                     ------
%:                           [P∧Q]^1     Q       Q→R
%:                           -------     -----------
%:                             P           R
%:                             -------------
%:     Q→R                         P∧R
%:   ========                  -------------1
%:   P∧Q→P∧R                     P∧Q→P∧R
%:
%:   ^nc-log-1                   ^nc-log-2
%:
%:                                            [p:A{×}B]^1          
%:                                            ------------          
%:                            [p:A{×}B]^1         π'p:B     f:B→C  
%:                            ------------        ---------------   
%:                                πp:A                f(π'p):C        
%:                                ----------------------------
%:        f:B→C                        (πp,f(π'p)):A{×}C
%:   ====================  =>  -----------------------------------1
%:   (×A)_1f:A{×}C→A{×}C      (λp⠆A{×}B.(πp,f(π'p)):A{×}B→A{×}C
%:
%:   ^nc-4                    ^nc-5
%:
\pu
$\scalebox{0.8}{$
  \ded{nc-log-1} \;\;\; \squigto \ded{nc-log-2}
  $}
$

\msk

$\scalebox{0.8}{$
  \ded{nc-4} \;\;\; \squigto \;\;\; \ded{nc-5}
  $}
$

\newpage

% «haskell»  (to ".haskell")
% (excp 9 "haskell")
% (exca   "haskell")

%:                   [p:A{×}B]^1          
%:                   ------------          
%:   [p:A{×}B]^1         π'p:B     f:B→C  
%:   ------------        ---------------   
%:       πp:A                f(π'p):C       
%:       ----------------------------
%:            (πp,f(π'p)):A{×}C
%:    -----------------------------------1
%:   (λp⠆A{×}B.(πp,f(π'p)):A{×}B→A{×}C
%:
%:   ^nc-5
%:
%:                        [\co{ab}:A{×}B]^1          
%:                        -----------------          
%:   [\co{ab}:A{×}B]^1         \co{b}:B       \co{btoc}:B→C  
%:   -----------------        -----------------------------   
%:       \co{a}:A                \co{c}:C        
%:       --------------------------------
%:            \co{ac}:A{×}C
%:    -----------------------------------1
%:   \co{abtoac}:A{×}B→A{×}C
%:
%:   ^nc-6

%V -- Translation to Haskell:
%V -- (with help from ski @ #haskell)
%V atimes :: (b -> c) -> ((a,b) -> (a,c))
%V atimes btoc = abtoac where
%V   abtoac ab = ac where
%V     a = fst ab
%V     b = snd ab
%V     c = btoc b
%V     ac = (a,c)
%L
%L verbdef "atimesHaskell"

\pu
$\hspace{-0.4cm}
 \scalebox{0.72}{$
  \begin{array}{c}
    \ded{nc-5} \\
    \\
    \cded{nc-6}
    \qquad
    \begin{tabular}{l}
      \co{a = fst ab} \\
      \co{b = snd ab} \\
      \co{c = btoc b} \\
      \co{ac = (a,c)} \\
      \co{abtoac = \\ ab -> ac} \\
      \co{atimes = \\ btoc -> abtoac} \\
    \end{tabular}
    \\
    \\
    \atimesHaskell
  \end{array}
  $}
$

\pu

% $\vcenter{\resizebox{!}{120pt}{\foo}}
% $








\newpage

%  _   _       _                          _     
% | | | |_ __ (_)_   _____ _ __ ___  __ _| |___ 
% | | | | '_ \| \ \ / / _ \ '__/ __|/ _` | / __|
% | |_| | | | | |\ V /  __/ |  \__ \ (_| | \__ \
%  \___/|_| |_|_| \_/ \___|_|  |___/\__,_|_|___/
%                                               
% «universals-CWM-orig»  (to ".universals-CWM-orig")
% (excp 10 "universals-CWM-orig")
% (exca    "universals-CWM-orig")

Here's how \cite[section III.1]{CWM2} defines universals:

% (find-cwm2page (+ 13  55) "III. Universals and Limits")
% (find-cwm2text (+ 13  55) "III. Universals and Limits")
% (find-cwm2page (+ 13  55)   "1. Universal Arrows")

\begin{quote}

{\bf Definition.} If $S: D→C$ is a functor and $c$ an object of $C$, a
universal arrow from $c$ to $S$ is a pair $〈r, u〉$ consisting of an
object $r$ of $D$ and an arrow $u: c→Sr$ of $C$, such that to every
pair $〈d,f〉$ with $d$ an object of $D$ and $f: c→Sd$ an arrow of $C$,
there is a unique arrow $f': r→d$ of $D$ with $S f'∘u = f$.

\end{quote}

This is too hard for my tiny brain.

\ColorRed{Solution:} I need types, diagrams,

a way to use other letters and fonts,

and examples.



%  _   _       _                   _       __     
% | | | |_ __ (_)_   _____ _    __| | ___ / _|___ 
% | | | | '_ \| \ \ / / __(_)  / _` |/ _ \ |_/ __|
% | |_| | | | | |\ V /\__ \_  | (_| |  __/  _\__ \
%  \___/|_| |_|_| \_/ |___(_)  \__,_|\___|_| |___/
%                                                 
% «universals-defs»  (to ".universals-defs")
% (excp 11 "universals-defs")
% (exca    "universals-defs")

\def\OK#1{\ColorGreen{(ok#1)}}
\def\OK#1{\ColorOrange{(ok#1)}}

%D diagram universal-CWM
%D 2Dx     100 +25
%D 2D  100     C1
%D 2D           |
%D 2D  +25 C2  C3
%D 2D      |    |
%D 2D  +25 C4  C5
%D 2D            
%D 2D  +15 C6  C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> c r Sr ∀d Sd D C
%D
%D (( C1 C3 -> .plabel= r \sm{u\\\univ}
%D    C2 C3 |->
%D    C2 C4 -> .plabel= l ∃!f'
%D    C3 C5 -> .plabel= r Sf'
%D    C2 C5 harrownodes nil 20 nil |->
%D    C4 C5 |->
%D    C1 C5 -> .slide= 28pt .plabel= r ∀f
%D    C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
%D diagram universal-my-letters
%D 2Dx     100 +25
%D 2D  100     C1
%D 2D           |
%D 2D  +25 C2  C3
%D 2D      |    |
%D 2D  +25 C4  C5
%D 2D            
%D 2D  +15 C6  C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> A B RB ∀C RC \catB \catA
%D
%D (( C1 C3 -> .plabel= r \sm{η\\\univ}
%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= 28pt .plabel= r ∀g
%D    C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
%D diagram universal-ring
%D 2Dx     100 +30
%D 2D  100     C1
%D 2D           |
%D 2D  +25 C2  C3
%D 2D      |    |
%D 2D  +25 C4  C5
%D 2D            
%D 2D  +15 C6  C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> 1 \Z[x] U\Z[x] ∀R UR \mathbf{Rings} \Set
%D
%D (( C1 C3 -> .plabel= r \sm{\nameof{x}\\\univ}
%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= 28pt .plabel= r ∀\nameof{a}
%D    C6 C7 -> .plabel= a U
%D ))
%D enddiagram
%D
\pu

\def\universaltextCWM{
\begin{tabular}{rl}
  If & $C,D$ are categories,   \\
     & $S:D→C$ is a functor,   \\
     & $c∈C$ is an object,     \\
     & $r∈D$ is an object,     \\
     & $u:C→Sr$ is a morphism, \\
then & $〈r,u〉$ is universal from $c$ to $S$ \\
 iff & $∀d∈D$,    \\
     & $∀f:C→Sd$, \\
     & $∃!f:r→d$ with $Sf'∘u=f$ \\
\end{tabular}
}

\def\universaltextmyletters{
\begin{tabular}{rl}
  If & $\catA,\catB$ are categories,   \\
     & $R:\catA→\catB$ is a functor,   \\
     & $A∈\catA$ is an object,     \\
     & $B∈\catB$ is an object,     \\
     & $η:A→RB$ is a morphism, \\
then & $(B,η)$ is universal from $A$ to $R$ \\
 iff & $∀C∈\catB$,    \\
     & $∀g:A→RC$, \\
     & $∃!f:B→C$ with $Rf∘η=g$ \\
\end{tabular}
}

\def\universaltextRings{
\begin{tabular}{rll}
  If & $\Set,\Rings$ are categories,        & \OK{}                     \\
     & $U:\Rings→\Set$ is a functor,        & \OK{: $U =$ underlying set}     \\
     & $1∈\Set$ is an object,               & \OK{: $1=\{*\}$}          \\
     & $\Z[x]∈\Rings$ is an object,         & \OK{}                     \\
     & $\nameof{x}:1→U\Z[x]$ is a morphism, & \OK{: $\nameof{x}(*)=x$}  \\
then & $(\Z[x],\nameof{x})$ is universal from $A$ to $R$ \\
 iff & $∀R∈\Rings$,    \\
     & $∀\nameof{a}:1→UR$, \\
     & $∃!f:\Z[x]→R$ with $Uf∘\nameof{x}=\nameof{a}$ & \OK{: $f(P(x)) = P(a)$} \\
\end{tabular}
}

\newpage

% «universals-CWM»  (to ".universals-CWM")

$\scalebox{0.9}{$
 \myvcenter{\universaltextCWM}
 \qquad
 \diag{universal-CWM}
 $}
$

\newpage

% «universals-my-letters»  (to ".universals-my-letters")

$\scalebox{0.9}{$
 \begin{array}{c}
 \myvcenter{\universaltextmyletters}
 \qquad
 \diag{universal-my-letters}
 \\
 \\
 \\
 \ColorOrange{
   \qquad
   \qquad
   \begin{tabular}{c}
     $↑$ Looks like \\
     Type Theory
   \end{tabular}
   \qquad
   \qquad
   \qquad
   \begin{tabular}{c}
     $↑$ Looks like \\
     Freyd's notation
   \end{tabular}
 }
 \end{array}
 $}
$

\newpage

% «universals-rings»  (to ".universals-rings")

$\scalebox{0.75}{$
 \begin{array}{c}
 \diag{universal-ring}
 \\ \\
 \myvcenter{\universaltextRings}
 \end{array}
 $}
$




\newpage

%  ___       _                        _         _                   
% |_ _|_ __ | |_ ___ _ __ _ __   __ _| | __   _(_) _____      _____ 
%  | || '_ \| __/ _ \ '__| '_ \ / _` | | \ \ / / |/ _ \ \ /\ / / __|
%  | || | | | ||  __/ |  | | | | (_| | |  \ V /| |  __/\ V  V /\__ \
% |___|_| |_|\__\___|_|  |_| |_|\__,_|_|   \_/ |_|\___| \_/\_/ |___/
%                                                                   
% «internal-views»  (to ".internal-views")
% (excp 13 "internal-views")
% (exca    "internal-views")

{\bf Internal views}
% (favp 19 "internal-views")
% (fav     "internal-views")

\ssk

The internal view of a \ColorRed{function}:

\def\ooo(#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}}
\def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}}
%
%D diagram second-blob-function
%D 2Dx     100 +20   +20
%D 2D  100 a-1 |-->  b-1
%D 2D  +08 a0  |-->  b0
%D 2D  +08 a1  |-->  b1
%D 2D  +08 a2  |-->  b2
%D 2D  +08 a3  |-->  b3
%D 2D  +08 a4  |-->  b4
%D 2D  +14 a5  |-->  b5
%D 2D  +25 \N  --->  \R
%D 2D
%D ren a-1 a0 a1 a2 a3 a4 a5 ==> -1 0 1 2 3 4 n
%D ren b-1 b0 b1 b2 b3 b4 b5 ==> -1 0 1 \sqrt{2} \sqrt{3} 2 \sqrt{n}
%D ((  a0 a5 midpoint .TeX= \oooo(7,23) y+= -2 place
%D    b-1 b5 midpoint .TeX= \oooo(7,25) y+= -2 place
%D       b-1 place
%D    a0 b0 |->
%D    a1 b1 |->
%D    a2 b2 |->
%D    a3 b3 |->
%D    a4 b4 |->
%D    a5 b5 |->
%D    \N \R -> .plabel= a \sqrt{\phantom{a}}
%D    a-1 relplace -7 -7 \phantom{foo}
%D    b5  relplace  7  7 \phantom{bar}
%D ))
%D enddiagram
%D
\pu
$$\scalebox{0.95}{$
  \begin{array}{rrcl}
   \sqrt{\;\;}: & \N &→& \R \\
                &  n &↦& \sqrt{n} \\
   \end{array}
   \qquad
   \diag{second-blob-function}
  $}
$$

\newpage

%  _____                 _                 
% |  ___|   _ _ __   ___| |_ ___  _ __ ___ 
% | |_ | | | | '_ \ / __| __/ _ \| '__/ __|
% |  _|| |_| | | | | (__| || (_) | |  \__ \
% |_|   \__,_|_| |_|\___|\__\___/|_|  |___/
%                                          
% «functors»  (to ".functors")
% (excp 15 "functors")
% (exca    "functors")

{\bf The internal view of a functor}

% (favp 8 "the-conventions")
% (fav    "the-conventions")
% (favp 17 "internal-view-functor")
% (fav     "internal-view-functor")

\ssk

{\sl Above} usually means {\sl inside}. (CAI)

The image of a diagram above $\catA$ by a functor $F:\catA→\catB$

is a a diagram {\sl with the same shape} above $\catB$. (CFSh)
%
%D diagram internal-view-functor-0
%D 2Dx     100 +12 +12   +25 +12 +12
%D 2D  100 A1 ____       B1 ____   
%D 2D  +12 |  ____ A3    |  ____ B3
%D 2D  +12 A2 ____  |    B2 ____  |
%D 2D  +12         A4            B4
%D 2D
%D 2D  +15   \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D
%D (( A1 A2 -> .plabel= l f
%D    A2 A3 -> .plabel= m g
%D    A3 A4 -> .plabel= r h
%D    A1 A3 -> .plabel= a k
%D    A2 A4 -> .plabel= b m
%D    \catA \catB -> .plabel= a F
%D ))
%D enddiagram
%D
%$$\pu
%  \diag{internal-view-functor-0}
%$$
%
%D diagram internal-view-functor-1
%D 2Dx     100 +12 +12   +25 +16 +16
%D 2D  100 A1 ____       B1 ____   
%D 2D  +12 |  ____ A3    |  ____ B3
%D 2D  +12 A2 ____  |    B2 ____  |
%D 2D  +12         A4            B4
%D 2D
%D 2D  +15   \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D ren B1 B2 B3 B4 ==> FA_1 FA_2 FA_3 FA_4
%D
%D (( A1 A2 -> .plabel= l f
%D    A2 A3 -> .plabel= m g
%D    A3 A4 -> .plabel= r h
%D    A1 A3 -> .plabel= a k
%D    A2 A4 -> .plabel= b m
%D    \catA \catB -> .plabel= a F
%D
%D    B1 B2 -> .plabel= l Ff
%D    B2 B3 -> .plabel= m Fg
%D    B3 B4 -> .plabel= r Fh
%D    B1 B3 -> .plabel= a Fk
%D    B2 B4 -> .plabel= b Fm
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.9}{$
  \diag{internal-view-functor-1}
  $}
$$

In this case we don't draw the arrows like $A_1 \mapsto FA_1$ because
there would be too many of them --- we leave them implicit.

\newpage

% «functor-2»  (to ".functor-2")

{\bf The internal view of a functor (2)}

\ssk

We say that the diagram in the previous slide is \ColorRed{an}
internal view of the functor $F$. To draw \ColorRed{the} internal view
of the functor $F: \catA → \catB$ we start with a diagram in $\catA$
that is made of two generic objects and a generic morphism between
them. We get this:

%D diagram internal-view-functor-2
%D 2Dx     100 +20
%D 2D  100 A0  A1
%D 2D
%D 2D  +20 A2  A3
%D 2D
%D 2D  +15 B0  B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> C FC D FD \catA \catB
%D
%D (( A0 A1 |->
%D    A0 A2 ->  .plabel= l g
%D    A1 A3 ->  .plabel= r Fg
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 B1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
  \diag{internal-view-functor-2}
$$

% Compare this with the diagram with blob-sets in Section
% \ref{internal-views}, in which the `$n \mapsto \sqrt{n}$' says where
% a generic element is taken.

\newpage

% «functor-3»  (to ".functor-3")

{\bf The internal view of a functor (3)}

%\ssk

Any arrow of the form $α \mapsto β$ above a functor arrow $\catA
\ton{F} \catB$ is interpreted as saying that $F$ takes $α$ to $β$, or,
that $Fα$ \ColorRed{reduces} to $β$. So this diagram
%
%D diagram internal-view-functor-3
%D 2Dx     100 +25
%D 2D  100 A0  A1
%D 2D
%D 2D  +20 A2  A3
%D 2D
%D 2D  +15 B0  B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D
%D (( A0 A1 |->
%D    A0 A2 ->  .plabel= l f
%D    A1 A3 ->  .plabel= r λp.(πp,f(π'p))
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 B1 -> .plabel= a (A{×})
%D ))
%D enddiagram
%D
$$\pu
  \diag{internal-view-functor-3}
$$
%
\ColorRed{defines} $(A×)$ as:
%
$$\begin{array}{rcl}
  (A×)_0 &:=& λB.\,A×B,\\
  (A×)_1 &:=& λf.λp.(πp,f(π'p)).\\
  \end{array}
$$

\newpage

% «functor-4»  (to ".functor-4")
% (excp 18 "functor-4")
% (exca    "functor-4")

{\bf The internal view of a functor (4)}

\ssk

Here the codomain of $F$ is $\Set$, and so we can also use the
internal view of $(A×)f$ to define $(A×)_1$...
%
%D diagram internal-view-functor-4
%D 2Dx     100 +25 +30 +35
%D 2D  100 A0  A1  C0  D0
%D 2D
%D 2D  +20 A2  A3  C1  D1
%D 2D
%D 2D  +15 B0  B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D ren C0 C1 ==> (a,b) (a,f(b))
%D ren D0 D1 ==> p (πp,f(π'p))
%D
%D (( A0 A1 |->
%D    A0 A2 ->  .plabel= l f
%D    A1 A3 ->  .plabel= r (A{×})f
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |->
%D    B0 B1 -> .plabel= a (A{×})
%D    C0 C1 |->
%D    D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{internal-view-functor-4}
$$

\newpage



%  _   _ _____    
% | \ | |_   _|__ 
% |  \| | | |/ __|
% | |\  | | |\__ \
% |_| \_| |_||___/
%                 
% «NTs»  (to ".NTs")
% (excp 19 "NTs")
% (exca    "NTs")
% (favp 22 "internal-view-NT")
% (fav     "internal-view-NT")

{\bf How to draw the internal view of a NT}

\ssk

If $F,G:\catA \to \catB$ are functors from $\catA$ to $\catB$,

$T:F \to G$ is a natural transformation from $F$ to $G$, and

$h:C \to D$ is a morphism in $\catA$,

then \ColorRed{$Th$ is a commutative square in $\catB$.}

\msk

How do we visualise this?

How do we visualise this with all details?

\newpage

% «NTs-2»  (to ".NTs-2")
% (excp 20 "NTs-2")
% (exca    "NTs-2")

%D diagram NT-img-T-only
%D 2Dx     100     +40
%D 2D  100 C0 ---_
%D 2D        \    v
%D 2D  +20    ---> C3
%D 2D
%D ren C0 C3 ==> \catA \catB
%D
%D (( C0 C3 -> .curve= _12pt .PLABEL= _(0.2) F
%D    C0 C3 -> .curve= ^12pt .PLABEL= ^(0.8) G
%D    newnode: TL at: tow(@C0,@C3)+v(-7,1.5)
%D    newnode: TR at: tow(@C0,@C3)+v(9,1.5)  TL TR => .plabel= a T
%D ))
%D enddiagram
%D
%D diagram NT-img-h-only
%D 2Dx     100
%D 2D  100 C
%D 2D  +20 D
%D 2D  +15 \catA
%D 2D
%D # ren ==>
%D
%D (( C D -> .plabel= l h
%D    \catA place
%D ))
%D enddiagram
%D
%D
%D
%D
%D diagram NT-img-full
%D 2Dx     100 +20 +20 +20
%D 2D  100 A0 -------_
%D 2D      | ->       v
%D 2D  +20 |   A1 ---> A2
%D 2D      v   |        |
%D 2D  +20 B0 -|-----_  |
%D 2D        ->v      v v
%D 2D  +20     B1 ---> B2
%D 2D
%D 2D  +17 C0 ---_
%D 2D        \    v
%D 2D  +20    ---> C3
%D 2D
%D ren A0 A1 A2 ==> C FC GC
%D ren B0 B1 B2 ==> D FD GD
%D ren C0 C3    ==> \catA \catB
%D
%D (( A0 A1 |->
%D    A0 A2 |->
%D    B0 B1 |->
%D    B0 B2 |->
%D    C0 C3 -> .curve= _12pt .PLABEL= _(0.2) F
%D    C0 C3 -> .curve= ^12pt .PLABEL= ^(0.8) G
%D
%D    A0 B0 -> .plabel= l h
%D    A1 B1 -> .plabel= m Fh
%D    A2 B2 -> .plabel= m Gh
%D    A1 A2 -> .plabel= m TC
%D    B1 B2 -> .plabel= m TD
%D
%D    newnode: FL at: tow(tow(@A0,@B0),tow(@A1,@B1),0+0.17)
%D    newnode: FR at: tow(tow(@A0,@B0),tow(@A1,@B1),1-0.17) FL FR |->
%D    newnode: GL at: tow(tow(@A0,@B0),tow(@A2,@B2),0+0.37)
%D    newnode: GR at: tow(tow(@A0,@B0),tow(@A2,@B2),1-0.19) GL GR |->
%D    newnode: TCL at: tow(@A0,tow(@A1,@A2),0.4)
%D    newnode: TCR at: tow(@A0,tow(@A1,@A2),0.8) TCL TCR |->
%D    newnode: TDL at: tow(@B0,tow(@B1,@B2),0.5)
%D    newnode: TDR at: tow(@B0,tow(@B1,@B2),0.85) TDL TDR |->
%D
%D    newnode: TL at: tow(@C0,@C3)+v(-7,1.5)
%D    newnode: TR at: tow(@C0,@C3)+v(9,1.5)  TL TR => .plabel= a T
%D ))
%D enddiagram
%D
$\pu
  \pdiag{NT-img-T-only}
  \pdiag{NT-img-h-only} =
  \left(
  \;\;  \diag{NT-img-full}
  \;\;
  \right)
$


\newpage

% «NTs-3»  (to ".NTs-3")
% (excp 21 "NTs-3")
% (exca    "NTs-3")

%D diagram ??
%D 2Dx     100 +25 +25
%D 2D  100 A0  B0  B1
%D 2D
%D 2D  +25 A1  B2  B3
%D 2D
%D 2D  +20     C0  C1
%D 2D
%D ren A0 B0 B1 ==> C FC GC
%D ren A1 B2 B3 ==> D FD GD
%D ren    C0 C1 ==>   \catA \catB
%D
%D (( A0 A1 -> .plabel= l h
%D    B0 B1 -> .plabel= a TC
%D    B2 B3 -> .plabel= a TD
%D    B0 B2 -> .plabel= l Fh
%D    B1 B3 -> .plabel= r Fg
%D    C0 C1 -> .plabel= a T
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\newpage

% __   __                   _       
% \ \ / /__  _ __   ___  __| | __ _ 
%  \ V / _ \| '_ \ / _ \/ _` |/ _` |
%   | | (_) | | | |  __/ (_| | (_| |
%   |_|\___/|_| |_|\___|\__,_|\__,_|
%                                   
% «yoneda»  (to ".yoneda")
% (excp 22 "yoneda")
% (exca    "yoneda")

{\bf Trailer: Yoneda in a particular case}

(With a representable functor... \cite[section 7.7]{FavC})

% (favp 40 "representable-functors")
% (fav     "representable-functors")
% (favp 42 "representable-functor-ex")
% (fav     "representable-functor-ex")

%D diagram 2.3.4._Z[x]
%D 2Dx     100 +55
%D 2D  100     A1
%D 2D  +20 A2  A3
%D 2D  +20 A4  A5
%D 2D  +15 B0  B1
%D 2D  +15 C1  C2
%D 2D  +20     C3
%D 2D
%D ren    A1 ==>          1
%D ren A2 A3 ==> \Z[x] U(\Z[x])
%D ren A4 A5 ==>     R UR
%D ren B0 B1 ==> \Rings          \Set
%D ren C1 C2 ==> \Rings(\Z[x],-) \Set(1,U-)
%D ren    C3 ==>                           U
%D
%D (( A1 A3  -> .plabel= r \sm{\nameof{x}\\\univ}
%D    A2 A3 |->
%D    A2 A4  -> .plabel= l ϕ
%D    A3 A5  -> .plabel= r Uϕ
%D    A4 A5 |->
%D    A1 A5  -> .slide= 25pt .plabel= r \nameof{ϕ(x)}
%D    A2 A5 harrownodes nil 20 nil |->
%D    B0 B1  -> .plabel= a U
%D    C1 C2 <-> .plabel= b T
%D    C1 C3 <-> .plabel= b T'
%D    C2 C3 <->
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.9}{$
  \diag{2.3.4._Z[x]}
  $}
$$


\newpage

%  _  __           
% | |/ /__ _ _ __  
% | ' // _` | '_ \ 
% | . \ (_| | | | |
% |_|\_\__,_|_| |_|
%                  
% «kan»  (to ".kan")
% (excp 23 "kan")
% (exca    "kan")

{\bf Trailer: (right) Kan Extensions}

(From \cite[section 7.9]{FavC})

% (favp 45 "kan-extensions")
% (fav     "kan-extensions")
% (favp 33 "basic-example-full")
% (fav     "basic-example-full")

%D diagram kan-1
%D 2Dx     100  +35
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +20 A2 - A3
%D 2D      |
%D 2D  +20 A4
%D 2D
%D 2D  +15 B0 = B1
%D 2D
%D 2D  +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF ∀G
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4    ==> H
%D ren B0 B1 ==> \catC^\catA \catC^\catB
%D ren C0 C1 ==>       \catA       \catB
%D
%D (( A0 A1 <-|
%D    A0 A2  -> .plabel= l GU
%D    A1 A3  -> .plabel= r ∃!U
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    A2 A4  -> .plabel= l T
%D    A0 A4  -> .slide= -20pt .plabel= l ∀V
%D    B0 B1 <-  sl^ .plabel= a ∘F
%D    B0 B1  -> sl_ .plabel= b \Ran_F
%D    C0 C1  ->     .plabel= a F
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-1
%D 2Dx     100 +25 +25 +20 +25 +25 +20 +25 +25
%D 2D  100     A1          B1          C1
%D 2D        /   \       /    \      /   \\
%D 2D  +25 A0 ---- A2  B0 ---- B2  C0 ---- C2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D
%D (( A0 A1 ->                .plabel= a F
%D    A1 A2 -> .curve= _10pt  .plabel= m R
%D    A1 A2 -> .curve= ^20pt  .plabel= a ∀G
%D    A0 A2 ->                .plabel= b H
%D    A0 A2 midpoint relplace -4 -8 \Dn{T}
%D    A1 A2 midpoint relplace  2 -3 \Dn{∃!U}
%D ))
%D enddiagram
%D
$$\pu
  \diag{kan-1}
  \qquad
  \quad
  \diag{kan-2-cells-1}
$$


\newpage

%  ___       _               _____ _____ 
% |_ _|_ __ | |_ _ __ ___   |_   _|_   _|
%  | || '_ \| __| '__/ _ \    | |   | |  
%  | || | | | |_| | | (_) |   | |   | |  
% |___|_| |_|\__|_|  \___/    |_|   |_|  
%                                        
% «intro-TT»  (to ".intro-TT")
% (excp 24 "intro-TT")
% (exca    "intro-TT")

\thispagestyle{empty} % (find-es "tex" "thispagestyle")

\begin{center}

\vspace*{1.5cm}

\begin{tabular}{c}
{\Large {\bf Introduction}} \\[1pt]
{\Large {\bf to Type Theory}} \\[1pt]
\end{tabular}

\end{center}

\newpage

% «untyped-lambda»  (to ".untyped-lambda")
% (excp 25 "untyped-lambda")
% (exca    "untyped-lambda")

{\bf A bit of untyped $λ$-calculus}

\ssk

If $h = (λa.a·a+4)$ then...

% (lam181p 5 "lambda")
% (lam181    "lambda")

%D diagram reduce-h
%D 2Dx     100 +35 +35  +40  +30
%D 2D  100 A ----> B
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 CL ---> DL
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 CS ---> DS
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 E       |
%D 2D      | \     |
%D 2D      |  v    |
%D 2D  +20 |   F   |
%D 2D      |    \  |
%D 2D      v     v v
%D 2D  +20 G ----> H -> I -> J
%D 2D
%D ren  A  B  ==>  h(2+3)            h(5)
%D ren  CL DL ==>  (λa.\,a·a+4)(2+3) (λa.\,a·a+4)(5)
%D ren  CS DS ==>  (a·a+4)[a:=2+3]   (a·a+4)[a:=5]
%D ren  E  F  ==>  (2+3)·(2+3)+4     (2+3)·5+4
%D ren  G  H  ==>  5·(2+3)+4         5·5+4
%D ren  I  J  ==>  25+4              29
%D (( A B ->   CS DS ->  CL DL ->   E F -> F H ->   G H ->
%D    A CL ->  CL CS ->  CS E -> E G ->
%D    B DL ->  DL DS ->  DS H -> H I -> I J ->
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.80}{$
  \diag{reduce-h}
  $}
$$



\newpage

% «types-after-discrete»  (to ".types-after-discrete")
% (excp 26 "types-after-discrete")
% (exca    "types-after-discrete")

{\bf Types after Discrete Mathematics}

\ssk
% (lam181p 9 "typed-L1-trees")
% (lam181    "typed-L1-trees")

$\begin{array}{l}
\text{If:} \\
A = \{1,2\}, \\
B = \{3,4\}, \\
C = \{30,40\}, \\
D = \{10,20\}, \\[5pt]
\text{Then:} \\
A×B = \cmat{(1,3),(1,4),\\(2,3),(2,4)} \\[8pt]
B→C = \cmat{
  \csm{(3,30),\\(4,30)},
  \csm{(3,30),\\(4,40)},
  \csm{(3,40),\\(4,30)},
  \csm{(3,40),\\(4,40)}\\
} \\
\end{array}
$

\newpage

If we know \ColorOrange{(the values of)} $a$, $b$, $f$

then we know \ColorOrange{(the value of)} $(a,f(b))$.

If $(a,b)=(2,3)$ and $f=\csm{(3,30),\\(4,40)}$

then $(a,f(b))=(2,30)$.

\msk

In trees:
%:
%:            (a,b)                   (2,3)
%:            -----π'                 -----π'
%:   (a,b)      b      f       (2,3)    3      \csm{(3,30),\\(4,40)}
%:   -----π    --------\app    -----π  --------------------------\app
%:     a         f(b)            2              30
%:     --------------\pair       -----------------\pair
%:        (a,f(b))                  (2,30)
%:
%:        ^idxf1                    ^idxf2
%:
$$\pu
  \scalebox{0.9}{$
  \ded{idxf1} \qquad \ded{idxf2}
  $}
$$

\newpage

\scalebox{0.8}{%
\begin{tabular}{l}
If we know the {\sl types} of $a$, $b$, $f$ \\
we know the type of $(a,f(b))$. \\
If we know the types of $p$, $f$ \\
we know the type of $(πp,f(π'p))$. \\
If we know the types of $p$, $f$ \\
we know the type of $(λp:A×B.(πp,f(π'p)))$. \\
\end{tabular}
}

\msk


%:
%:               (a,b):A×B                             p:A×B
%:               ---------π'                           -----π'
%:   (a,b):A×B      b:B       f:B→C        p:A×B       π'p:B       f:B→C
%:   ---------π     ---------------\app    ------π     ----------------\app
%:       a:A             f(b):C              πp:A            f(π'p):C
%:       ----------------------\pair         ----------------------\pair
%:              (a,f(b)):A×C                      (πp,f(π'p)):A×C             
%:                                                                             
%:              ^idxf3                             ^idxf4                     
%:
%:
%:              p:A×B
%:              -----π'
%:  p:A×B       π'p:B       f:B→C
%:  ------π     ----------------\app
%:    πp:A            f(π'p):C
%:    ----------------------\pair
%:         (πp,f(π'p)):A×C
%:      -----------------------------λ
%:      (λp:A×B.(πp,f(π'p))):A×B→A×C 
%:                                     
%:          ^idxf5                    
\pu
$$\scalebox{0.8}{$
  \begin{array}{l}
  \ded{idxf3}
  \\ \\
  \ded{idxf5}
  \end{array}
  $}
$$

% $$\ded{idxf4}$$

% $$\ded{idxf3} \qquad \ded{idxf4}$$




\newpage

% «type-inference»  (to ".type-inference")
% (excp 29 "type-inference")
% (exca    "type-inference")

\def\und#1#2{\underbrace{#1}_{#2}}

% {\bf Type inference}

% The usual way to type all subexpressions in via trees...

Compare:

\msk

% (lam181p 8 "types")
% (lam181    "types")
% (lam181p 11 "type-inference")
% (lam181     "type-inference")

%UB λ  p  : A×B. (π  p  , f    (π' p    ))
%UB   ----          ----  ----     ----
%UB   :A×B          :A×B  :B→C     :A×B
%UB               ------        -------
%UB                :A             :B
%UB                       ---------------
%UB                            :C
%UB              -------------------------
%UB                     :A×C
%UB --------------------------------------
%UB         :A×B→A×C
%L
%L defub "Axf 1"
%
$\pu
 \scalebox{0.9}{$
 \begin{array}{c}
 \ded{idxf5}
 \\ \\
 \ub{Axf 1}
 \end{array}
 $}
$

\newpage

% «typing»  (to ".typing")
% (excp 30 "typing")
% (exca    "typing")

{\bf Typing}

\def\Co#1{{\color{orange}(#1)}}   % Constraint
\def\Bc#1{{\color{Red}  #1 }}   % Bad constraint (not yet satisfied)
\def\Gc#1{{\color{Green}#1 }}   % Good constraint (satisfied)
\def\Gc#1{{\color{SpringGreen4}#1 }}   % Good constraint (satisfied)

\ssk

Idea: start with lots of type variables,

look at the constraints induced by the underbraces,

try to find a substitution that works...

\msk

%UB λ  p   .     (π  p  , f    (π' p    ))
%UB   ----          ----  ----     ----
%UB   :A            :A    :B       :A  
%UB               ------        -------
%UB                :C             :D
%UB                       ---------------
%UB                            :E
%UB              -------------------------
%UB                     :F  
%UB --------------------------------------
%UB         :G
%L
%L defub "Axf 2"
%
$\pu
 \myvcenter{\ub{Axf 2}}
 \qquad
 \begin{array}{rc}
   \Co{C⇒}  & \Bc{A = C×▁} \\
   \Co{D⇒}  & \Bc{A = ▁×D} \\
   \Co{E⇒}  & \Bc{B = D→E} \\
   \Co{F⇒}  & \Bc{F = C×E} \\
   \Co{G⇒}  & \Bc{G = A→F} \\
 \end{array}
$

\msk

First step: $[A:=C×D]$


\newpage

In the previous slide all the constraints

were red, meaning ``not satisfied yet''.

Let's mark the ones that are satisfied in green

and perform more substituions if needed...

\msk

%UB λ  p   .     (π  p  , f    (π' p    ))
%UB   ----          ----  ----     ----
%UB   :C×D          :C×D   :B      :C×D  
%UB               ------        -------
%UB                :C             :D
%UB                       ---------------
%UB                            :E
%UB              -------------------------
%UB                     :F  
%UB --------------------------------------
%UB         :G
%L
%L defub "Axf 3"
%
$\pu
 \myvcenter{\ub{Axf 3}}
 \qquad
 \begin{array}{rc}
   \Co{C⇒}  & \Gc{C×D = C×▁} \\
   \Co{D⇒}  & \Gc{C×D = ▁×D} \\
   \Co{E⇒}  & \Bc{B = D→E} \\
   \Co{F⇒}  & \Bc{F = C×E} \\
   \Co{G⇒}  & \Bc{G = C×D→F} \\
 \end{array}
$

\msk

Next step: $\bmat{B:=D→E \\ F:=C×E}$



\newpage

Let's

do

it

again...

\msk

%UB λ  p   .     (π  p  , f    (π' p    ))
%UB   ----          ----  ----     ----
%UB   :C×D          :C×D  :D→E     :C×D  
%UB               ------        -------
%UB                :C             :D
%UB                       ---------------
%UB                            :E
%UB              -------------------------
%UB                     :C×E  
%UB --------------------------------------
%UB         :G
%L
%L defub "Axf 4"
%
$\pu
 \scalebox{0.85}{$
 \myvcenter{\ub{Axf 4}}
 \qquad
 \begin{array}{rc}
   \Co{C⇒}  & \Gc{C×D = C×▁} \\
   \Co{D⇒}  & \Gc{C×D = ▁×D} \\
   \Co{E⇒}  & \Gc{D→E = D→E} \\
   \Co{F⇒}  & \Gc{C×E = C×E} \\
   \Co{G⇒}  & \Bc{G = C×D→C×E} \\
 \end{array}
 $}
$

\msk

Next step: $[G := C×D→C×E]$

\newpage

Done! Note that:

1) $C,D,E$ are {\sl type variables},

2) this typing is {\sl universal} --- all other valid typing

are substitution instances of this one. For example...

(see the next page)

\bsk
\bsk

\ColorBrown{

\footnotesize

Exercise:

Compare our naïve approach here

with the ones in \cite[chapter 22]{Pierce}.

% (find-books "__comp/__comp.el" "pierce")
% (find-taplpage (+ 22 317) "22 Type Reconstruction")
% (find-tapltext (+ 22 317) "22 Type Reconstruction")
% (find-taplpage (+ 22 317) "22.1 Type Variables and Substitutions")
% (find-taplpage (+ 22 319) "22.2 Two Views of Type Variables")
% (find-taplpage (+ 22 321) "22.3 Constraint-Based Typing")
% (find-taplpage (+ 22 326) "22.4 Unification")
% (find-taplpage (+ 22 329) "22.5 Principal Types")
% (find-taplpage (+ 22 330) "22.6 Implicit Type Annotations")
% (find-taplpage (+ 22 331) "22.7 Let-Polymorphism")
% (find-taplpage (+ 22 336) "22.8 Notes")

}


\newpage

%UB λ  p   .     (π  p  , f    (π' p    ))
%UB   ----          ----  ----     ----
%UB   :C×D          :C×D  :D→E     :C×D  
%UB               ------        -------
%UB                :C             :D
%UB                       ---------------
%UB                            :E
%UB              -------------------------
%UB                     :C×E  
%UB --------------------------------------
%UB         :C×D→C×E
%L
%L defub "Axf 5"
%
%UB λ  p   .     (π  p  , f    (π' p    ))
%UB   ----          ----  ----     ----
%UB   :A×B          :A×B  :B→C     :A×B  
%UB               ------        -------
%UB                :A             :B
%UB                       ---------------
%UB                            :C
%UB              -------------------------
%UB                     :A×C  
%UB --------------------------------------
%UB         :A×B→A×C
%L
%L defub "Axf 6"
%
$\pu
 \scalebox{0.85}{$
 \begin{array}{c}
 \left(\myvcenter{\ub{Axf 5}}\right) \bmat{C:=A \\ D:=B \\ E:=C} =
 \\ \\
 \left(\myvcenter{\ub{Axf 6}}\right)
 \end{array}
 $}
$



\newpage

{\bf Very very concrete types}

\msk

%UB λ  p     :\A×\B .     (π  p    ,  f     (π' p      ))
%UB   ------                 ------  ------     ------
%UB   :\A×\B                 :\A×\B  :\B→\C     :\A×\B  
%UB                        --------          ---------
%UB                           :\A               :\B
%UB                                  -----------------
%UB                                       :\C
%UB                       ------------------------------
%UB                             :\A×\C  
%UB ----------------------------------------------------
%UB         :\A×\B→\A×\C
%L
%L defub "Axf concrete 1"
%
$\pu
 \def\AA{\{0,1\}}
 \def\BB{\{2,3\}}
 \def\CC{\{4,5\}}
 \scalebox{0.80}{$
 \begin{array}{c}
   {\def\A{A}
    \def\B{B}
    \def\C{C}
    \left(\myvcenter{\ub{Axf concrete 1}}\right)
   }
   \bmat{A:=\AA \\ B:=\BB \\ C:=\CC} =
   \\ \\
   {\def\A{\AA}
    \def\B{\BB}
    \def\C{\CC}
    \left(\myvcenter{\ub{Axf concrete 1}}\right)
   }
 \end{array}
 $}
$

% (find-books "__logic/__logic.el" "damas")
% (find-damasphdpage (+ 8 72) "2.4. The type assignment algorithm W")
% (find-books "__comp/__comp.el" "pierce")
% (find-taplpage (+ 22 317) "22 Type Reconstruction")
% https://papl.cs.brown.edu/2014/Type_Inference.html


\newpage

% «intro-to-the-hard-part»  (to ".intro-to-the-hard-part")
% (excp 36 "intro-to-the-hard-part")
% (exca    "intro-to-the-hard-part")

\thispagestyle{empty} % (find-es "tex" "thispagestyle")

\begin{center}

\vspace*{1.0cm}

\begin{tabular}{c}
{\Large {\bf Introduction}} \\[1pt]
{\Large {\bf to the Hard Part}} \\[1pt]
{\Large {\bf of Basic Type Theory}} \\[1pt]
\end{tabular}

\end{center}

\newpage

% «some-references»  (to ".some-references")
% (excp 37 "some-references")
% (exca    "some-references")

Girard:

\cite{GLT} and \cite{GirardBlind}

\msk

Benjamin Pierce's book, Haskell:

\cite{Pierce}, \cite{HaskellCore}, \cite{Hutton}

\msk

HOTT, Kamareddine:

\cite{HOTT}, \cite{Kamareddine}

\msk

Also:

\cite{Sommaruga}, \cite{BauerGDDTT}

\msk

Some of them don't even mention $Σ$-types...

``$Σ$-types can be constructed from $Π$-types''

\ColorRed{This is not trivial at all! \frown}



\newpage

%   ____            _            _       
%  / ___|___  _ __ | |_ _____  _| |_ ___ 
% | |   / _ \| '_ \| __/ _ \ \/ / __/ __|
% | |__| (_) | | | | ||  __/>  <| |_\__ \
%  \____\___/|_| |_|\__\___/_/\_\\__|___/
%                                        
% «contexts»  (to ".contexts")
% (excp 38 "contexts")
% (exca    "contexts")

% (ntyp 60 "judgments-2")
% (nty     "judgments-2")

\def\und#1#2{\underbrace{#1}_{\text{#2}}}

{\bf Contexts}

$\setofsc {\uC{\ug{a∈\{1,2\}}, \ug{b∈\{2,3\}}, \uf{a<b}}} {\ue{10a+b}}$

here the context has ``generators'' (``{\sl var} $∈$ {\sl set}'')

and ``filters'' (``{\sl this expression must be true}'').

\msk

In

$\uC{\uvt{A⠆Θ}, \uvt{B⠆Θ}, \uvt{C⠆Θ}, \uvt{p:A×B}, \uvt{g:B→C}} ⊢
 \uconc{\uterm{(πp,g(π'p))}:\utype{A×C}}
$

the context is made of several declarations of the form

``variable : type''...

\newpage

%  ____ _____ ____      
% |  _ \_   _/ ___| ___ 
% | |_) || | \___ \/ __|
% |  __/ | |  ___) \__ \
% |_|    |_| |____/|___/
%                       
% «PTSs»  (to ".PTSs")
% (excp 39 "PTSs")
% (exca    "PTSs")

{\bf Derivations in Pure Type Systems}


Derivations in a PTS have {\sl lots} of bureaucracy.

This is what we need to derive $A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ$:

\msk

%:  (fooi-t ":" "⠆")
%:
%:                                ----a  ----a      ----a      ----a  ----a
%:                                ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□       ⊢Θ⠆□   ⊢Θ⠆□ 
%:   ----a  ----a      ----a      -----------w    -------v     -----------w 
%:   ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□        A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ       A⠆Θ⊢Θ⠆□
%:   -----------w    -------v      -----------------------w    -----------v
%:    A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ            A⠆Θ,B⠆Θ⊢A⠆Θ           A⠆Θ,B⠆Θ⊢B⠆Θ
%:    -----------------------w           ---------------------------------w
%:          A⠆Θ,B⠆Θ⊢A⠆Θ                        A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%:              ----------------------------------------------Π_{ΘΘΘ}
%:              A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%:              ^depprod1
%:
%:                                ----a  ----a      ----a      ----a  ----a
%:                                ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□       ⊢Θ⠆□   ⊢Θ⠆□ 
%:   ----a  ----a      ----a      -----------w_□   -------v_□   -----------w_□ 
%:   ⊢Θ⠆□   ⊢Θ⠆□       ⊢Θ⠆□        A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ       A⠆Θ⊢Θ⠆□
%:   -----------w_□   -------v_□   -----------------------w_□  -----------v_□
%:    A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ            A⠆Θ,B⠆Θ⊢A⠆Θ           A⠆Θ,B⠆Θ⊢B⠆Θ
%:    -----------------------w_□         ---------------------------------w_Θ
%:          A⠆Θ,B⠆Θ⊢A⠆Θ                        A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%:          --------------------------------------------------Π_{ΘΘΘ}
%:              A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%:              ^depprod1
%:
%:
%:                                                  ----a      ----a  ----a
%:                                                  ⊢Θ⠆□       ⊢Θ⠆□   ⊢Θ⠆□ 
%:                                 =======        -------v_□   -----------w_□ 
%:                                 A⠆Θ⊢Θ⠆□         A⠆Θ⊢A⠆Θ       A⠆Θ⊢Θ⠆□
%:                                 -----------------------w_□  -----------v_□
%:                                       A⠆Θ,B⠆Θ⊢A⠆Θ           A⠆Θ,B⠆Θ⊢B⠆Θ
%:          ===========                  ---------------------------------w_Θ
%:          A⠆Θ,B⠆Θ⊢A⠆Θ                        A⠆Θ,B⠆Θ,a⠆A⊢B⠆Θ
%:          ---------------------------------------------------Π_{ΘΘΘ}
%:              A⠆Θ,B⠆Θ⊢(Πa⠆A.B)⠆Θ
%:
%:              ^depprod2
%:
\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{depprod1}
$}

\msk

i.e.:

\resizebox{1.0\textwidth}{!}{%
$\ded{depprod2}
$}

\newpage

%  ____ _____ ____                ____  
% |  _ \_   _/ ___|    _____  __ |___ \ 
% | |_) || | \___ \   / _ \ \/ /   __) |
% |  __/ | |  ___) | |  __/>  <   / __/ 
% |_|    |_| |____/   \___/_/\_\ |_____|
%                                       
% «PTSs-2»  (to ".PTSs-2")
% «pts-derivation-2» (to ".pts-derivation-2")

{\bf Pure Type Systems: a derivation (2)}

This is what we need to derive $A⠆Θ⊢(λa⠆A.a)⠆(Πa⠆A.A)$:

\msk

%:                                                  
%:                                                  
%:                                          ----a
%:                                          ⊢Θ⠆□ 
%:                               =======   -------v_□
%:                               A⠆Θ⊢A⠆Θ   A⠆Θ⊢A⠆Θ
%:    =======         =======   -----------------w_Θ
%:    A⠆Θ⊢A⠆Θ         A⠆Θ⊢A⠆Θ     A⠆Θ,a⠆A⊢A⠆Θ
%:  -----------v_Θ    -----------------------Π_{ΘΘΘ}
%:  A⠆Θ,a⠆A⊢a⠆A            A⠆Θ⊢(Πa⠆A.A)⠆Θ
%:  -------------------------------------λ
%:        A⠆Θ⊢(λa⠆A.a)⠆(Πa⠆A.A)
%:
%:              ^depprod3
%:
\pu
\resizebox{1.0\textwidth}{!}{%
$\ded{depprod3}
$}


\bsk
\bsk

\ColorBrown{

\footnotesize

Exercise:

Read the presentation of PTSs in \cite[section 4c]{Kamareddine}.

Translate these trees to the notation of the book.

You will need a few tiny changes.

% (find-books "__logic/__logic.el" "typetheory")
% (find-mpottpage (+ 12 116) "4c Pure Type Systems")
% (find-mpottpage (+ 12 118) "4c1 The Barendregt cube")
% (find-mpottpage (+ 12 121) "4c2 Metaproperties of PTSs")

}


\newpage

%      _           _                            _         _____ 
%     | |_   _  __| | __ _ _ __ ___   ___ _ __ | |_ ___  |___ / 
%  _  | | | | |/ _` |/ _` | '_ ` _ \ / _ \ '_ \| __/ __|   |_ \ 
% | |_| | |_| | (_| | (_| | | | | | |  __/ | | | |_\__ \  ___) |
%  \___/ \__,_|\__,_|\__, |_| |_| |_|\___|_| |_|\__|___/ |____/ 
%                    |___/                                      
%
% «judgments»  (to ".judgments")
% (excp 37 "judgments")
% (exca    "judgments")
% (ntyp 61 "judgments-3")
% (nty     "judgments-3")

{\bf Judgments}

If we think --- \ColorRed{informally} --- that

$Θ$ is the ``set of all sets'' (mnemonic: Theta for ``Theths''),

then we can put these judgments for $λ$-calculus in

a very homogeneous form...

\msk

$\uC{\uvt{A⠆Θ}, \uvt{B⠆Θ}, \uvt{C⠆Θ}, \uvt{p:A×B}, \uvt{g:B→C}} ⊢
 \uconc{\uterm{(πp,g(π'p))}:\utype{A×C}}
$

\msk

the context is a series of declarations of the form ``var : type'',

and the conclusion is of the form ``term : type''.



\newpage



%  ____               _                         
% |  _ \  ___ _ __   | |_ _   _ _ __   ___  ___ 
% | | | |/ _ \ '_ \  | __| | | | '_ \ / _ \/ __|
% | |_| |  __/ |_) | | |_| |_| | |_) |  __/\__ \
% |____/ \___| .__/   \__|\__, | .__/ \___||___/
%            |_|          |___/|_|              
%
% «dependent-types»  (to ".dependent-types")
% (excp 42 "dependent-types")
% (exca    "dependent-types")

% (find-books "__logic/__logic.el" "hott")
% (find-hottpage (+ 12 25) "1.4 Dependent function types (-types)")
% (find-hottpage (+ 12 26) "1.5 Product types")
% (find-hottpage (+ 12 30) "1.6 Dependent pair types (-types)")

{\bf Dependent types for children}

\ssk
\def\ato#1#2{\csm{(0,#1),\\(1,#2)}}

\def\ABCD{
  \begin{array}[t]{c}
    A = \{0,1\}, \\
    B = \{2,3\}, \\
    C_0 = \{4,5\}, \\
    C_1 = \{6,7\} \\
    \\
    f:A→B       \\
    f(a)∈B      \\[5pt]
    g:(a⠆A)→C_a \\
    g(a)∈C_a    \\[5pt]
    p∈A×B       \\
    π'p∈B       \\[5pt]
    q∈(a⠆A)×C_a \\
    π'q∈C_{πq}  \\[5pt]
  \end{array}}

\def\Examples{
  \begin{array}[t]{rcl}
    \multicolumn{3}{l}{\text{Function types and}} \\
    \multicolumn{3}{l}{\text{dependent function types ($Π$-types):}} \\[5pt]
          A→B & = & \cmat{\ato22, \ato23, \ato32, \ato44} \\[10pt]
    (a:A)→C_a & = \\
     Πa:A.C_a & = & \cmat{\ato46, \ato47, \ato56, \ato57} \\
     \\
    \multicolumn{3}{l}{\text{Product types and}} \\
    \multicolumn{3}{l}{\text{dependent pair types ($Σ$-types):}} \\[5pt]
          A×B & = & \{ (0,2),\, (0,3), \, (1,2), \, (1,3) \} \\[5pt]
    (a:A)×C_a & = & \\
     Σa:A.C_a & = & \{ (0,4),\, (0,5), \, (1,6), \, (1,7) \} \\
  \end{array}}

$\scalebox{0.75}{$
 \begin{array}{l}
   \ABCD \quad \Examples \\
   \\
   \begin{tabular}{l}
   Note: ``$(a:A)→C_a$'' and ``$(a:A)×C_a$'' are Agda-isms. \\
   Many places use the terms ``dependent products'' and ``dependent sums''. \\
   \end{tabular}
 \end{array}   
 $}
$


\newpage

%     _              _                   _   _                 
%    / \   _ __   __| |   __ _ _ __   __| | (_)_ __ ___  _ __  
%   / _ \ | '_ \ / _` |  / _` | '_ \ / _` | | | '_ ` _ \| '_ \ 
%  / ___ \| | | | (_| | | (_| | | | | (_| | | | | | | | | |_) |
% /_/   \_\_| |_|\__,_|  \__,_|_| |_|\__,_| |_|_| |_| |_| .__/ 
%                                                       |_|    
%
% «typing-and-and-implies»  (to ".typing-and-and-implies")
% (excp 43 "typing-and-and-implies")
% (exca    "typing-and-and-implies")

{\bf Typing proofs of ``and'' and ``implies''}

$«Q»$ is a proof of $Q$.

$⟦Q⟧$ is the set of all proofs of $Q$.

\msk

$⟦Q∧R⟧$ is the set of all proofs of $Q∧R$.

\ColorRed{A} $«Q∧R»$ is a proof of $Q∧R$.

\ColorRed{A} $«Q∧R»$ is a pair $(«Q»,«R»)$,

so $⟦Q∧R⟧$ = $⟦Q⟧×⟦R⟧$.

\msk

$⟦Q→R⟧$ is the set of all proofs of $Q→R$.

\ColorRed{A} $«Q→R»$ is a proof of $Q→R$.

\ColorRed{A} $«Q→R»$ is an operation that takes $«Q»$s to $«R»$s,

so $⟦Q→R⟧$ = $⟦Q⟧→⟦R⟧$.




\newpage

%  _____                       _   _____      
% |  ___|_ _    __ _ _ __   __| | | ____|_  __
% | |_ / _` |  / _` | '_ \ / _` | |  _| \ \/ /
% |  _| (_| | | (_| | | | | (_| | | |___ >  < 
% |_|  \__,_|  \__,_|_| |_|\__,_| |_____/_/\_\
%                                             
% «typing-forall-and-exists»  (to ".typing-forall-and-exists")
% (excp 44 "typing-forall-and-exists")
% (exca    "typing-forall-and-exists")

{\bf Typing proofs of ``for all'' and ``exists''}


\bsk



% (find-mpottpage (+ 14 103) "II Propositions as Types, Pure Type Systems, AUTOMATH")
% (find-mpottpage (+ 12 105) "4 Propositions as Types and Pure Type Systems")
% (find-mpottpage (+ 12 106) "4a Propositions as Types and Proofs as Terms (PAT)")
% (find-mpottpage (+ 12 106) "4a1 Intuitionistic logic")
% (find-mpottpage (+ 16 123) "A universal quantification")
% (find-mpotttext (+ 16 123) "A universal quantification")
% (find-mpottpage (+ 16 147) "various ways in which PAT")
% (find-mpotttext (+ 16 147) "various ways in which PAT")

\def\und#1#2{\underbrace{#1}_{\text{#2}}}
\def\und#1#2{\underbrace{#1}_{#2}}

%UB  «∀b⠆B.P(b)» = \PFA
%UB ------------   ------------
%UB :⟦∀b⠆B.P(b)⟧   :Πb⠆B.⟦P(b)⟧
%L
%L defub "forall"
%
$\pu
 \def\PFA{\cmat{
   (2,«P(2)»), \\
   (3,«P(3)»)
   }}
 \scalebox{1.0}{$
 \begin{array}{c}
 \ub{forall}
 \end{array}
 $}
$

\bsk
\bsk

%UB  «∃b⠆B.P(b)» = \PEX
%UB ------------   ------------
%UB :⟦∃b⠆B.P(b)⟧   :Σb⠆B.⟦P(b)⟧
%L
%L defub "forall"
%
$\pu
 \def\PEX{(b,«P(b)»)}
 \scalebox{1.0}{$
 \begin{array}{c}
 \ub{forall}
 \end{array}
 $}
$




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



% \newpage
% 
% % «marsden»  (to ".marsden")
% 
% {\bf String diagrams: Marsden}
% 
% % (find-books "__cats/__cats.el" "marsden-dragging")
% % (find-books "__cats/__cats.el" "marsden-ctusd")
% % (favp 44 "2-category-of-cats")
% % (fav     "2-category-of-cats")


% (find-es "haskell" "haskell-to-core")


\newpage

%   ______        ____  __    ____      _       _ 
%  / ___\ \      / /  \/  |  / ___|_ __| |     / |
% | |    \ \ /\ / /| |\/| | | |   | '__| |     | |
% | |___  \ V  V / | |  | | | |___| |  | |___  | |
%  \____|  \_/\_/  |_|  |_|  \____|_|  |_____| |_|
%                                                 
% «guessing-nu-CWM-1»  (to ".guessing-nu-CWM-1")
% (excp 45 "guessing-nu-CWM-1")
% (exca    "guessing-nu-CWM-1")

{\bf CWM: Creation of Limits, theorem V.1}

% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 109) "V. Limits")
% (find-cwm2page (+ 13 109)   "1. Creation of Limits")

\def\Cone{\mathrm{Cone}}
\def\Nat{\mathrm{Nat}}

\def\vcat#1#2#3{\psm{
    & &#2\\
    & &↓ \\
  #1&→&#3\\}}

\def\constvcat#1{\vcat{#1}{#1}{#1}}
\def\smallvcat{{\scalebox{0.50}{$\vcat123$}}}
\def\ACB{A{×_C}B}


%D diagram nu-CWM-1
%D 2Dx     100  +30
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +20 A2 - A3
%D 2D      |
%D 2D  +20 A4
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 ==> Δ* *
%D ren A2 A3 ==> ΔL L
%D ren A4    ==> F
%D ren B0 B1 ==> \text{Set}^J \text{Set}
%D
%D (( A0 A1 <-|
%D    A0 A2  -> .plabel= l Δg
%D    A1 A3  -> .plabel= r ∃!g
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    A2 A4  -> .plabel= l \sm{ν\\\text{(univ)}}
%D    A0 A4  -> .slide= -30pt .plabel= l ∀σ
%D    B0 B1 <-  sl^ .plabel= a Δ
%D    B0 B1  -> sl_ .plabel= b \Lim
%D    newnode: A3R at: @A3+v(28,8) .TeX= \defL place
%D ))
%D enddiagram
%D
%D diagram nu-CWM-X
%D 2Dx     100  +30
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +20 A2 - A3
%D 2D      |
%D 2D  +20 A4
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 ==> ΔX X
%D ren A2 A3 ==> ΔL L
%D ren A4    ==> F
%D ren B0 B1 ==> \text{Set}^J \text{Set}
%D
%D (( A0 A1 <-|
%D    A0 A2  -> .plabel= l Δh
%D    A1 A3  -> .plabel= r ∃!h
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    A2 A4  -> .plabel= l \sm{ν\\\text{(univ)}}
%D    A0 A4  -> .slide= -30pt .plabel= l ∀τ
%D    B0 B1 <-  sl^ .plabel= a Δ
%D    B0 B1  -> sl_ .plabel= b \Lim
%D ))
%D enddiagram
%D
$$\pu
  \def\defL{\begin{array}{l}
    :=\Cone(*,F) \\ =\Nat(Δ*,F) \\ = \Hom(Δ*,F) \\
    \end{array}}
  %
  \scalebox{0.9}{$
  \diag{nu-CWM-1}
  \quad
  \diag{nu-CWM-X}
  $}
$$


\newpage

% «guessing-nu-1»  (to ".guessing-nu-1")
% (excp 46 "guessing-nu-1")
% (exca    "guessing-nu-1")

{\bf Guessing $ν$: first attempt}

%D diagram nu-1-small
%D 2Dx     100  +35
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +20 A2 - A3
%D 2D      |
%D 2D  +20 A4
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 ==> Δ1 1
%D ren A2 A3 ==> Δ\Lim\,F \Lim\,F
%D ren A4    ==> F
%D ren B0 B1 ==> \Set^\catJ \Set
%D
%D (( A0 A1 <-|
%D    A0 A2  -> .plabel= l Δg
%D    A1 A3  -> .plabel= r ∃!g
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    A2 A4  -> .plabel= l \sm{ν\\\text{(univ)}}
%D    A0 A4  -> .slide= -30pt .plabel= l ∀σ
%D    B0 B1 <-  sl^ .plabel= a Δ
%D    B0 B1  -> sl_ .plabel= b \Lim
%D ))
%D enddiagram
%D
%D diagram nu-1
%D 2Dx     100  +50
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +35 A2 - A3
%D 2D      |
%D 2D  +35 A4
%D 2D
%D 2D  +25 B0 - B1
%D 2D
%D ren A0 A1 ==> \constvcat{1} 1
%D ren A2 A3 ==> \constvcat{\ACB} \ACB
%D ren A4    ==> \vcat{A}{B}{C}
%D ren B0 B1 ==> \Set^\smallvcat_{\phantom{a}} \Set
%D
%D (( A0 A1 <-|
%D    A0 A2  -> .plabel= l Δg
%D    A1 A3  -> .plabel= r ∃!g
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    A2 A4  -> .plabel= l \sm{ν\\\text{(univ)}}
%D    A0 A4  -> .slide= -45pt .plabel= l ∀σ
%D    B0 B1 <-  sl^ .plabel= a Δ
%D    B0 B1  -> sl_ .plabel= b \Lim
%D ))
%D enddiagram
%D
$\pu
 \scalebox{0.9}{$
  \diag{nu-1-small}
  \qquad
  \diag{nu-1}
 $}
$


\newpage

In this first attempt the types don't match...

A natural transformation
%
$$σ: \vcat{1}{1}{1} → \vcat{A}{B}{C}$$

is a triple $(\nameof{a}:1→A, \nameof{b}:1→B, \nameof{c}:1→C)$,

but an element of $\ACB$ is a triple $(a,b,c)$...

\bsk

\ColorRed{(I'm omitting the ``obeying certain properties''!)}

\ColorRed{(Why can I do that? Long story...)}


\newpage

% «guessing-nu-2»  (to ".guessing-nu-2")
% (excp 48 "guessing-nu-2")
% (exca    "guessing-nu-2")

{\bf Guessing $ν$: second attempt}

\ssk

...so let's try to guess $ν$, $g$, $h$ by finding their types,

then finding natural constructions that yield

terms of those types, and then checking if

our guesses behave as expected...


\newpage

% «guessing-nu-2-diag»  (to ".guessing-nu-2-diag")
% (excp 49 "guessing-nu-2-diag")
% (exca    "guessing-nu-2-diag")
% (cwmp 14 "creation-of-limits")
% (cwm     "creation-of-limits")

%D diagram nu-attempt-2-1
%D 2Dx     100 +40  +35
%D 2D  100 C0  A0 - A1  
%D 2D      |   |     |
%D 2D  +25 |   A2 - A3
%D 2D      |   |
%D 2D  +25 C1  A4       
%D 2D          
%D 2D  +15 C2  B0 - B1  
%D 2D
%D ren A0 A1 ==> Δ1 1
%D ren A2 A3 ==> ΔL L
%D ren A4    ==> F
%D ren B0 B1 ==> \Set^\catJ \Set
%D ren C0 C1 C2 ==> 1 FJ \Set
%D
%D (( A0 A1 <-|
%D    A0 A2  -> .plabel= l Δg
%D    A1 A3  -> .plabel= r \sm{∃!g\phantom{ooo}\\:=λ*.ℓ}
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    A2 A4  -> .plabel= l \sm{ν:=\\λJ.λℓ.ℓJ*}\!\!   # \sm{ν\\\text{(univ)}}
%D    A0 A4  -> .slide= -40pt .plabel= l ∀ℓ
%D
%D    newnode: A3R at: @A3+v(28,0) .TeX= =\Hom(Δ1,F) place
%D
%D    B0 B1 <-  sl^ .plabel= a Δ
%D    B0 B1  -> sl_ .plabel= b \Lim
%D
%D    C0 C1  -> .plabel= l ℓJ   C2 place
%D ))
%D enddiagram
%D
%D diagram nu-attempt-2-X
%D 2Dx     100 +40  +35
%D 2D  100 C0  A0 - A1  
%D 2D      |   |     |
%D 2D  +25 |   A2 - A3
%D 2D      |   |
%D 2D  +25 C1  A4       
%D 2D          
%D 2D  +15 C2  B0 - B1  
%D 2D
%D ren A0 A1 ==> ΔX ∀X
%D ren A2 A3 ==> ΔL L
%D ren A4    ==> F
%D ren B0 B1 ==> \Set^\catJ \Set
%D ren C0 C1 C2 ==> X FJ \Set
%D
%D (( A0 A1 <-|
%D    A0 A2  -> .plabel= l Δh
%D    A1 A3  -> .plabel= r \sm{∃!h\phantom{oooooooooooo}\\:=λx.λJ.λ*.TJx}
%D    A0 A3 harrownodes nil 20 nil <-|
%D    A2 A3 <-|
%D    A2 A4  -> .plabel= l \sm{ν:=\\λJ.λℓ.ℓJ*\\\text{(univ)}}
%D    A0 A4  -> .slide= -40pt .plabel= l ∀T
%D
%D    newnode: A3R at: @A3+v(28,0) .TeX= =\Hom(Δ1,F) place
%D
%D    B0 B1 <-  sl^ .plabel= a Δ
%D    B0 B1  -> sl_ .plabel= b \Lim
%D
%D    C0 C1  -> .plabel= l TJ   C2 place
%D ))
%D enddiagram
%D

$\pu
 \scalebox{0.60}{$
  \begin{array}{r}
  \diag{nu-attempt-2-1}
  \\ \\ \\
  \diag{nu-attempt-2-X}
  \end{array}
  \qquad
  \begin{array}{l}
    \begin{array}[t]{rcl}
       ℓ &:& Δ1 → F    \\
      ℓJ &:& Δ1J → FJ  \\
      ℓJ &:& 1 → FJ    \\
     ℓJ* &∈& FJ        \\[5pt]
      ν &:& ΔL → F     \\
     νJ &:& ΔLJ → FJ   \\
     νJ &:& L → FJ     \\
     νJℓ &∈& FJ        \\[5pt]
      g &:& 1 \to L    \\
     g* &∈& L          \\
    \end{array}
    \quad
    \begin{array}[t]{rcl}
       T &:& ΔX → F    \\
      TJ &:& ΔXJ → FJ  \\
      TJ &:& X → FJ    \\
     TJx &∈& FJ        \\[5pt]
       h &:& X → L     \\
      hx &∈& L         \\
      hx &:& Δ1 → F    \\
      hxJ &:& Δ1J → FJ \\
      hxJ &:& 1 → FJ   \\
      hxJ* &∈& FJ      \\[5pt]
    \end{array}
    \\
    \\
    \text{Let's try this:} \\ %[5pt]
    \def\IE{\hspace{-0.75em}⇒}
    \begin{array}[t]{rcll}
      νJℓ  &=& ℓJ*           & \IE \\
      νJ   &=& λℓ.ℓJ*        & \IE \\
      ν   &:=& λJ.λℓ.ℓJ*     &     \\[5pt]
      g*   &=& ℓ             & \IE \\
      g   &:=& λ*.ℓ          &     \\[5pt]
      hxJ* &=&           TJx & \IE \\
      hxJ  &=&        λ*.TJx & \IE \\
      hx   &=&     λJ.λ*.TJx & \IE \\
      h    &:=& λx.λJ.λ*.TJx      \\
    \end{array}
  \end{array}
 $}
$





% \newpage
% (find-LATEX "catsem-slides.bib")
% \cite{Riehl}






% (find-books "__comp/__comp.el" "pierce")
% (find-taplpage (+ 22 315) "V Polymorphism")
% (find-taplpage (+ 22 317) "22 Type Reconstruction")
% (find-tapltext (+ 22 317) "22 Type Reconstruction")
% (find-taplpage (+ 22 317) "22.1 Type Variables and Substitutions")
% (find-taplpage (+ 22 319) "22.2 Two Views of Type Variables")
% (find-taplpage (+ 22 321) "22.3 Constraint-Based Typing")
% (find-taplpage (+ 22 326) "22.4 Unification")
% (find-taplpage (+ 22 329) "22.5 Principal Types")
% (find-taplpage (+ 22 330) "22.6 Implicit Type Annotations")
% (find-taplpage (+ 22 331) "22.7 Let-Polymorphism")
% (find-taplpage (+ 22 336) "22.8 Notes")


% http://angg.twu.net/2018.2-MD.html
% http://angg.twu.net/2018.2-MD/20180813_lista_1.pdf
% http://angg.twu.net/2018.2-MD/20180813_lista_2.pdf

% (favp 39 "ness")
% (fav     "ness")

\newpage



\printbibliography

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

\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2021excuse veryclean
make -f 2019.mk STEM=2021excuse pdf

% Local Variables:
% coding: utf-8-unix
% ee-tla: "exc"
% End:
