% (find-LATEX "2020seelylccc.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020seelylccc.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2020seelylccc.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020seelylccc.pdf"))
% (defun e () (interactive) (find-LATEX "2020seelylccc.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020seelylccc"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020seelylccc.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020seelylccc.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020seelylccc.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020seelylccc.pdf
%               file:///tmp/2020seelylccc.pdf
%           file:///tmp/pen/2020seelylccc.pdf
% http://angg.twu.net/LATEX/2020seelylccc.pdf
% (find-LATEX "2019.mk")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,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-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")
%
\DeclareFontFamily{U}{matha}{\hyphenchar\font45}
\DeclareFontShape{U}{matha}{m}{n}{
      <5> <6> <7> <8> <9> <10> gen * matha
      <10.95> matha10 <12> <14.4> <17.28> <20.74> <24.88> matha12
      }{}
\DeclareSymbolFont{matha}{U}{matha}{m}{n}
\DeclareMathSymbol{\thinsubset}{3}{matha}{"80}
\DeclareMathSymbol{\thinsupset}{3}{matha}{"81}
\def\limp{\thinsupset}   % See: (find-es "tex" "limp-abx")
%
% (find-es "tex" "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

% (find-LATEX "2020hyp.tex" "limp-2020")
% \def\limpbody{%
%   \begin{picture}%(4,2)
%                  (5.1,2.5)(-0.5,-0.25)
%     \Line(0,0)(3,0)
%     \Line(0,2)(3,2)
%     \put(3,1){\arc[-90,90]{1}}
%   \end{picture}%
%   }
% \def\limp{%
%   \mathrel{\vcenter{\hbox{%
%     \unitlength=2pt%
%     \linethickness{0.4pt}%
%     \limpbody%
%   }}}}
\catcode`⊸=13 \def⊸{\limp}


{\setlength{\parindent}{0em}
\footnotesize

Notes on [Seely84], a.k.a.:

``Locally cartesian closed categories and type theory'', available at:

\url{http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf}

\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020seelylccc.pdf}

}




\section*{1. The type theory ML}

% (find-books "__cats/__cats.el" "seely-lccc")
% (find-seelylcccpage (+ -32 33) "1. The type theory ML")
% (find-seelylccctext (+ -32 33) "1. The type theory ML")
% (find-seelylcccpage (+ -32 34) "Type formation rules")
% (find-seelylccctext (+ -32 34) "Type formation rules")



1.1.1. Type formation rules. The following are to be types:

    (i) If $F$ is a type-valued function constant, and $a_1, ... ,
a_n$ are terms of the appropriate types, then $F(a_1, ..., a_n)$ is a
type.

   (ii) 1 is a type.

   (iii) If $a, b ∈ A$, then $I(a, b)$ is a type.

   (iv) If $A,B[x]$ are types, $x∈A$, where $x,B$ satisfy the c.o.v.,
then $Π_{x∈A}B[x]$ and $Σ_{x∈A} B[x]$ are types. If $x$ does not in
fact occur in $B$, these are written $A ⊸ B$ and $A×B$ respectively.

\msk

% 1.1.2. Term formation rules. The following are to be terms of the
% indicated types:
% 
%    (vbl) For each type $A$, there are variables $x∈A$; (such $x$ could
% also be denoted $x_A$, if the type of x is not clear from the
% context.)
% 
%    (fen) If / is a term-valued function constant, and a1)...,an are terms of the
% appropriate types, then f(av..., an) is a term of the appropriate type.
% 
%    (II) * e 1 .
% 
%    (III) If t[x]eB[x], where xA,t (and a;^,.B) satisfy the c.o.v., then
% 
% 
% (also written AxA t[x] e HxA B[x]).
%    (TIE) IffeYlxAB[x], aeA, thenf(a)eB[a].
%    (El) If aeA,beB[a], then <a,b}e'LxeAB[x'].
%    (SE) If ce'LxeAB[x], then7r(c)e4, 7T'(c)eB[n(c)].
%    (=1) If aeA, then r(a)el{a, a).
%
%    (= E) If a,beA, cel(a,b), deC[a,a,r(a)], where C[x,y,z] is a type depending on
% x,yeA, zeI(x,y), then a(d)[a,b,c]eC[a,b,c].
%   1-1-3. Equality rules. Using the notation of § 1-1-2, we have the following equations:
%   (f eq) Any imposed equations on function constants induce the obvious equations.
%   (lred) If<el,then< = *.
%   (Tired) (*xeAt[x])(a) = t[a].
%   (UexV)f=AxeAf(x).
%   (S red) n«a,b)) = a; n'((a,b)) = b.
%   (Sexp) c = (n(c),n'(c)y.
%   (= red) cr(d) [a, a, r(a)] = d.
%   (= exp) If/[a, b, c] e C[a, b, c], then/ = <r(f[a, a, r(a)]) [a, b, c].
%   (I rule) If a[x], b[x]eA, t[x]el(a[x], b[x]), then a[x] = b[x], and t[x] = r(a[x]).
% Furthermore, an ML theory may have axioms of the form S = T for types S, T. (We
% suppose similar axioms for terms are given by function constants of the appropriate
% I-type.)
%    Finally, we have the usual rules for = : for types or terms o, b, c (as appropriate):
%   If a = b then c[a] = c[b]. If a -- b then b = a.
%   If a = b and b = c, then a = c. a = a.
%   If cea and a = b, then ce6. If aec and a = b, then 6ec.

% (hypp 7 "bcc-seely-lccc")
% (hyp    "bcc-seely-lccc")


% (find-books "__cats/__cats.el" "seely-lccc")
% (find-seelylcccpage (+ -32 37)    "(iv)    P satisfies the Beck condition:")
% (find-seelylccctext (+ -32 37)    "(iv)    P satisfies the Beck condition:")
% (find-TH "dednat6" "a-big-example")
% (find-dednat6 "tug-slides.tex" "BCC")

{\bf BCC in the SeelyLCCC paper}

\def\BCCL{\mathsf{BCCL}}


%D diagram BCC-Seely-LCCC-1
%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 A0 |---------------------> A1
%D 2D        |->                        |->
%D 2D +35        A2 |--------------------> A3
%D 2D
%D ((
%D    B0 .tex=       h^*φ            B1 .tex=       φ
%D    B2 .tex= k^*f^*Σ_gφ            B3 .tex= g^*Σ_gφ
%D   B2' .tex= h^*g^*Σ_gφ
%D    B4 .tex=    Σ_kh^*φ            B5 .tex= Σ_gφ
%D    B6 .tex=    f^*Σ_gφ            B7 .tex= Σ_gφ
%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 (( A0 .tex= D   A1 .tex= C   A2 .tex= A   A3 .tex= B 
%D    A0 A1 -> .plabel= b h
%D    A0 A2 -> .plabel= l k
%D    A1 A3 -> .plabel= r g
%D    A2 A3 -> .plabel= a f
%D    A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
  \diag{BCC-Seely-LCCC-1}
$$

\newpage

{\bf BCC in the SeelyLCCC paper (2)}

%D diagram BCC-Seely-LCCC-my
%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 A0 |---------------------> A1
%D 2D        |->                        |->
%D 2D +35        A2 |--------------------> A3
%D 2D
%D ((
%D    B0 .tex=       h^*φ            B1 .tex=       φ
%D    B2 .tex= k^*f^*Σ_gφ            B3 .tex= g^*Σ_gφ
%D   B2' .tex= h^*g^*Σ_gφ
%D    B4 .tex=    Σ_kh^*φ            B5 .tex= Σ_gφ
%D    B6 .tex=    f^*Σ_gφ            B7 .tex= Σ_gφ
%D
%D    B0 .tex=   \bsm{x\\b,a,c}      B1 .tex= \bsm{x\\b,c}
%D    B2 .tex= \bsm{c,x\\b,a,c}      B3 .tex= \bsm{c,x\\b,c}
%D   B2' .tex= \bsm{c,x\\b,a,c}
%D    B4 .tex= \bsm{c,x\\b,a}        B5 .tex= \bsm{c,x\\b}
%D    B6 .tex= \bsm{c,x\\b,a}        B7 .tex= \bsm{c,x\\b}
%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 (( A0 .tex= D         A1 .tex= C       A2 .tex= A      A3 .tex= B
%D    A0 .tex= [b,a,c]   A1 .tex= [b,c]   A2 .tex= [b,a]  A3 .tex= [b] 
%D    A0 A1 -> .plabel= b h
%D    A0 A2 -> .plabel= l k
%D    A1 A3 -> .plabel= r g
%D    A2 A3 -> .plabel= a f
%D    A0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\pu
  \scalebox{0.9}{$
  \diag{BCC-Seely-LCCC-my}
  $}
$$

\newpage

{\bf BCC in the SeelyLCCC paper (2)}

% (nmop 2 "components")
% (nmo    "components")

%:
%:            φ
%:          ----
%:          Σ_gφ
%:     -------------
%:     \id:Σ_gφ→Σ_gφ                              φ
%:   -----------------         -------------    ----
%:   η=\id^♯:φ→g^*Σ_gφ         h^*g^*≅k^*f^*    Σ_gφ
%:   --------------------    -----------------------
%:   h^*η:h^*φ→h^*g^*Σ_gφ    α:h^*g^*Σ_gφ→k^*f^*Σ_gφ
%:   -----------------------------------------------
%:           α∘h^*η:h^*φ→k^*f^*Σ_gφ
%:         ----------------------------
%:         ♮=(α∘h^*η)^♭:Σ_kh^*φ→f^*Σ_gφ
%:   
%:         ^BCC-Seely-LCCC-1
%:
$$\pu
  \ded{BCC-Seely-LCCC-1}
$$



\end{document}

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