% (find-LATEX "2024leantt.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2024leantt.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2024leantt.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2024leantt.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2024leantt.pdf"))
% (defun e () (interactive) (find-LATEX "2024leantt.tex"))
% (defun u () (interactive) (find-latex-upload-links "2024leantt"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2024leantt.pdf"))
%          (code-eec-LATEX "2024leantt")
% (find-pdf-page   "~/LATEX/2024leantt.pdf")
% (find-sh0 "cp -v  ~/LATEX/2024leantt.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2024leantt.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2024leantt.pdf
%               file:///tmp/2024leantt.pdf
%           file:///tmp/pen/2024leantt.pdf
%  http://anggtwu.net/LATEX/2024leantt.pdf
% (find-LATEX "2019.mk")
% (find-lualatex-links "2024leantt" "ltt")

\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-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{edrx21}               % (find-LATEX "edrx21.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex            % (find-LATEX "edrx21chars.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")
%
%\usepackage[backend=biber,
%   style=alphabetic]{biblatex}            % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (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

\def\pmatl#1{\left(
    \begin{array}{llllllll}
      #1
    \end{array}
  \right)}
\def\setof#1{\{#1\}}

$$Θ = \mathsf{Type}$$

$$\begin{array}{rcl}
  Γ_2 &=&
      \pmatl{
       A:Θ  & \{a:A\}  \\
       Ba:Θ & \{b:Ba\} \\
       Cab:Θ & \{c:Cab\} \\
       Dabc:Θ & \{d:Dabc\} \\
      } \\
      &=&
      \pmatl{
       A:Θ    \\
       B:(a:A)→Θ \\
       C:(a:A)→(b:Ba)→Θ \\
       D:(a:A)→(b:Ba)→(c:Cab)→Θ \\
      } \\
  \end{array}
$$

\bsk

%:
%:   Ba:Θ  \{a:A\}
%:   -------------
%:   B:(a:A)→Θ
%:
%:   ^Ba
%:
%:
%:   Cab:Θ  \{b:Ba\}
%:   ---------------
%:   Ca:(b:Ba)→Θ      \{a:A\}
%:   ------------------------
%:   C:(a:A)→(b:Ba)→Θ
%:
%:   ^Cab
%:
%:
%:   Dabc:Θ  \{c:Cab\}
%:   -----------------
%:   Dab:(c:Cab)→Θ     \{b:Ba\}
%:   --------------------------
%:   Da:(b:Ba)→(c:Cab)→Θ         \{a:A\}
%:   -----------------------------------
%:   D:(a:A)→(b:Ba)→(c:Cab)→Θ
%:
%:   ^Dabc
%:
\pu
$$\ded{Ba}$$

$$\ded{Cab}$$

$$\ded{Dabc}$$


\newpage

\def\Nat{\mathsf{Nat}}
\def\Int{\mathsf{Int}}
\def\P#1{\left(\myvcenter{#1}\right)}

%:
%:            (x∈A)                (x∈A)     
%:          .........             ........
%:   a=c∈A  b(x)∈B(x)   a=c∈\Nat  2-x∈\Int   
%:   ----------------   ------------------ 
%:    b(a)=b(c)∈B(a)     2-a=2-c∈\Int    
%:                                         
%:    ^MartinLof1        ^MartinLof2       
%:
\pu
$$\ded{MartinLof1} \qquad \ded{MartinLof2}$$


$$\P{\ded{MartinLof1}}
  \bmat{A:=\Nat \\
        B(x):=\Int \\
        b(x):=2-x
       }
  =
  \P{\ded{MartinLof2}}
$$






%\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=2024leantt veryclean
make -f 2019.mk STEM=2024leantt pdf

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