LATEX/2022Cats3.lagda.tex (htmlized)

Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.
% This file:
%   http://angg.twu.net/LATEX/2022Cats3.lagda.tex.html
%   http://angg.twu.net/LATEX/2022Cats3.lagda.tex
%           (find-angg "LATEX/2022Cats3.lagda.tex")
%   http://angg.twu.net/LATEX/2022Cats3.pdf
% Author: Eduardo Ochs <eduardoochs@gmail.com>
%
% (find-LATEX "2022Cats3.lagda.tex")
% (code-eec-LATEX "2022Cats3")
% (defun c  () (interactive) (eec-agdalatex-sh "2022Cats3" "-record" :end))
% (defun C  () (interactive) (eec-agdalatex-sh "2022Cats3" "" "Success!!!"))
% (defun D  () (interactive) (find-pdf-page      "~/LATEX/2022Cats3.pdf"))
% (defun d  () (interactive) (find-pdftools-page "~/LATEX/2022Cats3.pdf"))
% (defun e  () (interactive) (find-angg "LATEX/2022Cats3.lagda.tex"))
% (defun et () (interactive) (find-angg "LATEX/2022Cats3.tex"))
% (defun a  () (interactive) (find-angg  "AGDA/2022Cats3.agda"))
% (defun u  () (interactive) (find-latex-upload-links "2022Cats3"))
% (defun v  () (interactive) (find-2a '(e) '(d)))
% (defun v  () (interactive) (find-pdftoolsr-page "~/LATEX/2022Cats3.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2022Cats3.pdf"))
%
% (find-2a nil '(find-LATEX "2022template.lagda.tex"))
% (find-dired-re  "~/LATEX/" ".lagda.tex$")
% (find-agdalatex-links "2022Cats3")
% (find-agdafile-links  "2022Cats3")
% (find-lualatex-links  "2022Cats3")

\documentclass{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{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")
%
\usepackage{agda}                 % (find-LATEX "agda.sty")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")


\catcode`⟨=13 \def⟨{\ensuremath{\langle}}
\catcode`⟩=13 \def⟩{\ensuremath{\rangle}}

% \catcode`₀=13 \def₀{{\ensuremath{{}_0}}}
% \catcode`₁=13 \def₁{{\ensuremath{{}_1}}}
% \catcode`₂=13 \def₂{{\ensuremath{{}_2}}}
% \catcode`₃=13 \def₃{{\ensuremath{{}_3}}}
% \catcode`∎=13 \def∎{\blacksquare}
% \catcode`∎=13 \def∎{{\ensuremath{HELLO}}}

% % $ ₀ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉ ₊ ₋ ₌ ₍ ₎ ₐ ₑ ₒ ₓ ₕ ₖ ₗ ₘ ₙ ₚ ₛ ₜ$

%  ____  _                   _ 
% |  _ \(_) __ _  __ _ ___  / |
% | | | | |/ _` |/ _` / __| | |
% | |_| | | (_| | (_| \__ \ | |
% |____/|_|\__,_|\__, |___/ |_|
%                |___/         
%
%D diagram Yoneda-names
%D 2Dx     100  +30
%D 2D  100      A1
%D 2D            |
%D 2D  +25 A2 - A3
%D 2D      |     |
%D 2D  +25 A4 - A5
%D 2D      |     |
%D 2D  +25 A6 - A7
%D 2D      |     |
%D 2D  +25 A8 - A9
%D 2D
%D 2D  +15 B0 - B1
%D 2D
%D ren    A1 ==>    A
%D ren A2 A3 ==> C RC
%D ren A4 A5 ==> D RD
%D ren A6 A7 ==> E RE
%D ren A8 A9 ==> F RF
%D ren B0 B1 ==> \catB \catA
%D
%D (( A1 A3  -> .plabel= r η
%D    A2 A3 |->
%D    A2 A4  -> .plabel= l f
%D    A3 A5  -> .plabel= r Rf
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D    A4 A6  -> .plabel= l g
%D    A5 A7  -> .plabel= r Rg
%D    A4 A7 harrownodes nil 20 nil |->
%D    A6 A7 |->
%D    A6 A8  -> .plabel= l m
%D    A7 A9  -> .plabel= r Rm
%D    A6 A9 harrownodes nil 20 nil |->
%D    A8 A9 |->
%D
%D    A1 A5  -> .slide=  20pt .plabel= r h
%D    A1 A7  -> .slide=  35pt .plabel= r ℓ
%D    A2 A6  -> .slide= -15pt .plabel= l k
%D
%D    B0 B1  -> .plabel= a R
%D ))
%D enddiagram
%D
$$\pu
  \diag{Yoneda-names}
$$

\def\oB{∘_\catB}
\def\oA{∘_\catA}
\def\oBC{∘_{\catB(C,-)}}
\def\oAA{∘_{\catA(A,R-)}}

\sa{catB(C,idD)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catB(C,\id_D) \\
    = λf.\;\id_D \oB f \\
    = λf.\;f \\
    = \id_{\catB(C,D)} \\
  \end{array}
  $}
  }

\sa{catB(C,g)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catB(C,g) \\
    = λf.\;g \oB f \\
  \end{array}
  $}
  }
\sa{catB(C,m)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catB(C,m) \\
    = λk.\;m \oB k \\
  \end{array}
  $}
  }
\sa{catB(C,mog)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catB(C,m) \oBC \catB(C,g) \\
    = (λk.\;m \oB k)∘(λf.\;g \oB f) \\
    = λf.\;((λk.\;m \oB k)∘(λf.\;g \oB f))(f) \\
    = λf.\;(λk.\;m \oB k)((λf.\;g \oB f)(f)) \\
    = λf.\;(λk.\;m \oB k)(g \oB f) \\
    = λf.\;m \oB (g \oB f) \\
    = λf.\;(m \oB g) \oB f \\
    = \catB(C,m \oB g) \\
  \end{array}
  $}
  }




%D diagram B(C,-)-equalities
%D 2Dx     100   +30  +60   +30
%D 2D  100 LA0 - LA1  LB0 - LB1
%D 2D      |       |  |     |
%D 2D  +25 |       |  LB2 - LB3
%D 2D      |       |  |     |
%D 2D  +25 LA2 - LA3  LB4 - LB5
%D 2D
%D 2D  +15 LC0 - LC1  LD0 - LD1
%D 2D
%D ren LA0 LA1 ==> D \catB(C,D)
%D ren LA2 LA3 ==> D \catB(C,D)
%D ren LB0 LB1 ==> D \catB(C,D)
%D ren LB2 LB3 ==> E \catB(C,E)
%D ren LB4 LB5 ==> F \catB(C,F)
%D ren LC0 LC1 ==> \catB \Set
%D ren LD0 LD1 ==> \catB \Set
%D
%D (( LA0 LA1 |->
%D    LA0 LA2  -> .plabel= l \id_D
%D    LA1 LA3  -> .plabel= r \ga{catB(C,idD)}
%D    LA0 LA3 harrownodes nil 20 nil |->
%D    LA2 LA3 |->
%D
%D    LB0 LB1 |->
%D    LB0 LB2  -> .plabel= l g
%D    LB1 LB3  -> .plabel= r \ga{catB(C,g)}
%D    LB0 LB3 harrownodes nil 20 nil |->
%D    LB2 LB3 |->
%D    LB2 LB4  -> .plabel= l m
%D    LB3 LB5  -> .plabel= r \ga{catB(C,m)}
%D    LB2 LB5 harrownodes nil 20 nil |->
%D    LB4 LB5 |->
%D
%D    LB0 LB4  -> .slide= -15pt .plabel= l m∘g
%D    LB1 LB5  -> .slide=  60pt .plabel= r \ga{catB(C,mog)}
%D
%D    LC0 LC1 -> .plabel= a \catB(C,-)
%D    LD0 LD1 -> .plabel= a \catB(C,-)
%D ))
%D enddiagram
%D
$$\pu
  \diag{B(C,-)-equalities}
$$


\sa{catA(A,RidD)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catA(A,R\id_D) \\
    = λh.\;R\id_D∘h \\
    = λh.\;\id_{RD}∘h \\
    = λh.\;h \\
    = \id_{\catA(A,RD)} \\
  \end{array}
  $}
  }

\sa{catA(A,Rg)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catA(A,Rg) \\
    = λh.\;Rg∘h \\
  \end{array}
  $}
  }
\sa{catA(A,Rm)}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catA(A,Rm) \\
    = λℓ.\;Rm∘ℓ \\
  \end{array}
  $}
  }
\sa{catA(A,R(log))}{
  \scalebox{0.7}{$
  \begin{array}{l}
    \catA(RC,m) \oAA \catA(RC,g) \\
    = (λℓ.\;Rm∘ℓ)∘(λh.\;Rg∘h) \\
    = λh.\;((λℓ.\;Rm∘ℓ)∘(λh.\;Rg∘h))(h) \\
    = λh.\;(λℓ.\;Rm∘ℓ)((λh.\;Rg∘h)(h)) \\
    = λh.\;(λℓ.\;Rm∘ℓ)(Rg∘h) \\
    = λh.\;Rm∘(Rg∘h) \\
    = λh.\;(Rm∘Rg)∘h \\
    = \catA(A,R(m∘g)) \\
  \end{array}
  $}
  }





%D diagram A(A,R-)-equalities
%D 2Dx     100   +30  +60   +30
%D 2D  100 RA0 - RA1  RB0 - RB1
%D 2D      |       |  |     |
%D 2D  +25 |       |  RB2 - RB3
%D 2D      |       |  |     |
%D 2D  +25 RA2 - RA3  RB4 - RB5
%D 2D
%D 2D  +15 RC0 - RC1  RD0 - RD1
%D 2D
%D ren RA0 RA1 ==> D \catA(A,RD)
%D ren RA2 RA3 ==> D \catA(A,RD)
%D ren RB0 RB1 ==> D \catA(A,RD)
%D ren RB2 RB3 ==> E \catA(A,RE)
%D ren RB4 RB5 ==> F \catA(A,RF)
%D ren RC0 RC1 ==> \catB \Set
%D ren RD0 RD1 ==> \catB \Set
%D
%D (( RA0 RA1 |->
%D    RA0 RA2  -> .plabel= l \id_D
%D    RA1 RA3  -> .plabel= r \ga{catA(A,RidD)}
%D    RA0 RA3 harrownodes nil 20 nil |->
%D    RA2 RA3 |->
%D
%D    RB0 RB1 |->
%D    RB0 RB2  -> .plabel= l g
%D    RB1 RB3  -> .plabel= r \ga{catA(A,Rg)}
%D    RB0 RB3 harrownodes nil 20 nil |->
%D    RB2 RB3 |->
%D    RB2 RB4  -> .plabel= l m
%D    RB3 RB5  -> .plabel= r \ga{catA(A,Rm)}
%D    RB2 RB5 harrownodes nil 20 nil |->
%D    RB4 RB5 |->
%D
%D    RB0 RB4  -> .slide= -15pt .plabel= l m∘g
%D    RB1 RB5  -> .slide=  60pt .plabel= r \ga{catA(A,R(log))}
%D
%D    RC0 RC1 -> .plabel= a \catA(A,R-)
%D    RD0 RD1 -> .plabel= a \catA(A,R-)
%D ))
%D enddiagram
%D
$$\pu
  \diag{A(A,R-)-equalities}
$$


\newpage

%     _             _       
%    / \   __ _  __| | __ _ 
%   / _ \ / _` |/ _` |/ _` |
%  / ___ \ (_| | (_| | (_| |
% /_/   \_\__, |\__,_|\__,_|
%         |___/             

\begin{code}
module 2022Cats3 where

open import Level
open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning

postulate ext : ∀ {ℓ ℓ'} {A : Set ℓ} {B : A → Set ℓ'} {f g : (a : A) → B a}
                  → (∀ (a : A) → f a ≡ g a) → f ≡ g

module Cats3 where

record Cat {ℓ₀ ℓ₁ : Level} : Set (suc (ℓ₀ ⊔ ℓ₁)) where
  field
    Objs  : Set ℓ₀
    Hom   : Objs → Objs → Set ℓ₁
    id    : (D : Objs) → (Hom D D)
    _◦_   : {C D E : Objs}
            → (g : Hom D E)
            → (f : Hom C D)
            →     (Hom C E)
    idL   : {D E : Objs}
            → (g : Hom D E)
            → (g ≡ g ◦ (id D))
    idR   : {D E : Objs}
            → (g : Hom D E)
            → (g ≡ (id E) ◦ g)
    assoc : {C D E F : Objs}
            → (f : Hom C D)
            → (g : Hom D E)
            → (m : Hom E F)
            → (m ◦ (g ◦ f) ≡ (m ◦ g) ◦ f)

catSet : Cat {suc zero} {zero}
Cat.Objs  catSet = Set
Cat.Hom   catSet = λ A B → (A → B)
Cat.id    catSet = λ A → (λ a → a)
Cat._◦_   catSet = λ g f → (λ a → g (f a))
Cat.idL   catSet = λ f → refl
Cat.idR   catSet = λ f → refl
Cat.assoc catSet = λ f g h → refl

catSetH : Cat {suc zero} {zero}
Cat.Objs  catSetH = Set
Cat.Hom   catSetH = λ A B → (A → B)
Cat.id    catSetH = λ A → (λ a → a)
Cat._◦_   catSetH = λ g f → (λ a → g (f a))
Cat.idL   catSetH = λ f → refl
Cat.idR   catSetH = λ f → refl
Cat.assoc catSetH = λ f g h → refl

record Functor {ℓ₀ ℓ₁ ℓ₂ ℓ₃ : Level}
               (catB : Cat {ℓ₀} {ℓ₁})
               (catA : Cat {ℓ₂} {ℓ₃})
             : Set (suc (ℓ₀ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  field
    ac0      : (Cat.Objs catB) → (Cat.Objs catA)
    ac1      : {C D : Cat.Objs catB}
               → (Cat.Hom catB C D)
               → (Cat.Hom catA (ac0 C) (ac0 D))
    respids  : {C : Cat.Objs catB}
               → (ac1 (Cat.id catB C) ≡ Cat.id catA (ac0 C))
    -- respcomp : {C D E : Cat.Objs catB}
    --            → {f : Cat.Hom catB C D}
    --            → {g : Cat.Hom catB D E}
    --            → (ac1 (Cat._◦_ catB g f) ≡ (Cat._◦_ catA (ac1 g) (ac1 f)))
  --
  -- R.ac0       C                  = RC
  -- R.ac1      {C} {D} f           = R f
  -- R.respids  {C}                 : R(id C) ≡ id(RC)
  -- R.respcomp {C} {D} {E} {f} {g} : R(g∘f) ≡ Rg∘Rf

record NT {ℓ₀ ℓ₁ ℓ₂ ℓ₃ : Level}
          {catC : Cat {ℓ₀} {ℓ₁}}
          {catD : Cat {ℓ₂} {ℓ₃}}
          (F G : Functor catC catD)
             : Set (suc (suc (ℓ₀ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃))) where
  field
    ac       : (A : Cat.Objs catC)
               → (Cat.Hom catD (Functor.ac0 F A) (Functor.ac0 G A))
    sqcond   : {A B : Cat.Objs catC}
               → (f : Cat.Hom catC A B)
               → ((Cat._◦_ catD (ac B) (Functor.ac1 F f)) ≡
                   (Cat._◦_ catD (Functor.ac1 G f) (ac A)))
               → Set
  --
  -- T.ac      A        : Hom(FA,GA)
  -- T.sqcond {A} {B} f : TB∘Ff ≡ Gf∘TA

postulate catA : Cat {zero} {zero}
postulate catB : Cat {zero} {zero}
postulate R : Functor catB catA
postulate A : Cat.Objs catA
postulate C : Cat.Objs catB
postulate η : Cat.Hom catA A (Functor.ac0 R C)

postulate D E F : Cat.Objs catB
postulate f     : Cat.Hom  catB C D
postulate g     : Cat.Hom  catB D E

catB[C,-] : Functor catB catSetH
Functor.ac0      catB[C,-] D           = Cat.Hom catB C D
Functor.ac1      catB[C,-] {D} {E} g f = Cat._◦_ catB g f
Functor.respids  catB[C,-] {D} = trans (ext (λ f → sym (Cat.idR catB f))) refl
-- Functor.respcomp catB[C,-] {D} {E} {F} {g} {m} = {!!}

infix 10 _◦B_

B₀      : Set
B₀      = Cat.Objs catB
B[_,_]  : B₀ → B₀ → Set
B[_,_]  D E = Cat.Hom catB D E
_◦B_    : {D E F : B₀} → (B[_,_] E F) → (B[_,_] D E) → (B[_,_] D F)
_◦B_    {D} {E} {F} m g = Cat._◦_ catB m g
id_B    : (D : B₀) → B[_,_] D D
id_B    D = Cat.id catB D

Set[_,_] : Set → Set → Set
Set[_,_] A B = Cat.Hom catSet A B

B[C,_]₀ : B₀ → Set 
B[C,_]₀ E = Functor.ac0 catB[C,-] E
B[C,_]₁ : {D E : B₀} → (B[_,_] D E) → (B[_,_] C D) → (B[_,_] C E)
B[C,_]₁ {D} {E} g = Functor.ac1 catB[C,-] g

module On_DEF (D E F : Cat.Objs catB) where
  idD          : B[_,_] D D
  idD          = id_B D
  B[C,D]       : Set
  B[C,D]       = B[C,_]₀ D
  B[C,idD]     : Set[_,_] B[C,D] B[C,D]
  B[C,idD]     = B[C,_]₁  idD
  id[B[C,D]]   : Set[_,_] B[C,D] B[C,D]
  id[B[C,D]]   = Cat.id  catSet B[C,D]
  λf⇒[idD◦f]   : (f : B[C,D]) → B[C,D]
  λf⇒[idD◦f]   f = idD ◦B f
  λf⇒f         : (f : B[C,D]) → B[C,D]
  λf⇒f         f = f
  λf⇒<idD◦f≡f> : (f : B[C,D]) → (idD ◦B f) ≡ f
  λf⇒<idD◦f≡f> f = sym (Cat.idR catB f)
  --
  <B[C,idD]≡[λf⇒[idD◦f]]> : B[C,idD] ≡ λf⇒[idD◦f]
  <B[C,idD]≡[λf⇒[idD◦f]]> = refl
  <[λf⇒[idD◦f]]≡[λf⇒f]>   : λf⇒[idD◦f] ≡ λf⇒f
  <[λf⇒[idD◦f]]≡[λf⇒f]>   = ext λf⇒<idD◦f≡f>
  <[λf⇒f]≡id[B[C,D]]>     : λf⇒f ≡ id[B[C,D]]
  <[λf⇒f]≡id[B[C,D]]>     = refl
  --
  <B[C,idD]≡id[B[C,D]]>  : B[C,idD] ≡ id[B[C,D]]
  <B[C,idD]≡id[B[C,D]]>  = begin
      B[C,idD]    ≡⟨ <B[C,idD]≡[λf⇒[idD◦f]]> ⟩
      λf⇒[idD◦f]  ≡⟨ <[λf⇒[idD◦f]]≡[λf⇒f]>   ⟩
      λf⇒f        ≡⟨ <[λf⇒f]≡id[B[C,D]]>     ⟩
      id[B[C,D]]
    ∎
  --
  -- m g f = Cat.assoc catB f g m

  -- g◦f               : (g : B[D,E]) → (f : B[C,D]) → B[C,E]
  -- g◦f               g f = Cat._◦_ catB g f
  -- m◦g               : (m : B[E,F]) → (g : B[D,E]) → B[D,F]
  -- m◦g               m g = Cat._◦_ catB m g
  -- m◦k               : (m : B[E,F]) → (k : B[C,E]) → B[C,F]
  -- m◦k               m k = Cat._◦_ catB m k
  -- m◦[g◦f]           : (m : B[E,F]) → (g : B[D,E]) → (f : B[C,D]) → B[C,F]
  -- m◦[g◦f]           m g f = Cat._◦_ catB m (g◦f g f)
  -- [m◦g]◦f           : (m : B[E,F]) → (g : B[D,E]) → (f : B[C,D]) → B[C,F]
  -- [m◦g]◦f           m g f = Cat._◦_ catB (m◦g m g) f
  -- m◦[g◦f]≡[m◦g]◦f   : (m : B[E,F]) → (g : B[D,E]) → (f : B[C,D])
  --                     → (m◦[g◦f] m g f ≡ [m◦g]◦f m g f)
  -- m◦[g◦f]≡[m◦g]◦f   m g f = Cat.assoc catB f g m

  

-- (find-es "agda" "module-system")

module M = On_DEF D E F -- where
open M

-- foo : {!Set!}
-- foo = <B[C,idD]≡id[B[C,D]]>
-- trans (ext (λ f → sym (Cat.idR catB f))) refl


  --
  -- [λf⇒[id:D◦f]]≡[λf⇒f] : λf⇒[id:D◦f] ≡ λf⇒f
  -- [λf⇒[id:D◦f]]≡[λf⇒f] = {!!}

\end{code}






\end{document}

% (find-fline "~/LATEX/")
% (find-fline "~/AGDA/latex/")
% (find-fline "~/AGDA/latex/Logic2.tex")
% (find-agdausermanualpage (+ 4 195) "4.7 Generating LaTeX")
% (find-agdausermanualtext (+ 4 195) "4.7 Generating LaTeX")
% (find-agdausermanualpage (+ 4 95) "3.19.3 Literate Agda")
% (find-agdausermanualtext (+ 4 95) "3.19.3 Literate Agda")

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
agda --latex --latex-dir=. 2022Cats3.lagda.tex
laf 2022Cats3*
cd ~/LATEX/
lualatex 2022Cats3.tex


% Local Variables:
% coding:  utf-8-unix
% modes:   (latex-mode agda2-mode)
% End: