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



\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")


%D diagram Cat
%D 2Dx     100  +20  +20  +20
%D 2D  100 A0
%D 2D  +20 A1
%D 2D  +20 A2
%D 2D  +20 A3
%D 2D  +15 B0
%D 2D
%D ren A0 A1 A2 A3 ==> B C D E
%D ren B0 ==> \catA
%D
%D (( A0 A1 -> .plabel= l f
%D    A1 A2 -> .plabel= l g
%D    A2 A3 -> .plabel= l h
%D    A1 loop (dr,ur) .plabel= r \id_C
%D    A2 loop (dr,ur) .plabel= r \id_D
%D    B0 place
%D ))
%D enddiagram
%D
%D diagram Fun
%D 2Dx     100  +20
%D 2D  100 A0 - A1
%D 2D  +20 A2 - A3
%D 2D  +20 A4 - A5
%D 2D  +20 A6 - A7
%D 2D  +15 B0 - B1
%D 2D
%D ren A0 A1 A2 A3 A4 A5 A6 A7 ==> C FC C FC D FD E FE
%D ren B0 B1 ==> \catA \catB
%D
%D (( A0 A1 |->
%D    A2 A3 |->
%D    A4 A5 |->
%D    A6 A7 |->
%D    A0 A2 -> .plabel= l \id_C    A1 A3 -> .plabel= r \sm{F\id_C\\=\id_{FC}}
%D    A2 A4 -> .plabel= l g        A3 A5 -> .plabel= r Fg
%D    A4 A6 -> .plabel= l h        A5 A7 -> .plabel= r Fh
%D    B0 B1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
  \diag{Cat}
  \qquad
  \diag{Fun}
$$




\begin{code}
module 2022Cats6 where

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

record Cat {ℓ₀ ℓ₁ : Level} : Set (suc (ℓ₀ ⊔ ℓ₁)) where
  infix 10 _◦_
  field
    Objs  : Set ℓ₀
    Hom   : Objs → Objs → Set ℓ₁
    id    : {B : Objs} → (Hom B B)
    _◦_   : {B C D : Objs} → (g : Hom C D) → (f : Hom B C) → (Hom B D)
    idL   : {C D : Objs} → (g : Hom C D) → (g ≡ g ◦ id)
    idR   : {C D : Objs} → (g : Hom C D) → (g ≡ id ◦ g)
    assoc : {B C D E : Objs}
            → (f : Hom B C)
            → (g : Hom C D)
            → (h : Hom D E)
            → (h ◦ (g ◦ f) ≡ (h ◦ g) ◦ f)
  --
  f≡f◦id : {C D : Objs} → {g : Hom C D} → g ≡ g ◦ id
  f≡f◦id {C} {D} {g} = idL g
  f≡id◦f : {C D : Objs} → {g : Hom C D} → g ≡ id ◦ g
  f≡id◦f {C} {D} {g} = idR g
  f◦id≡f : {C D : Objs} → {g : Hom C D} → g ◦ id ≡ g
  f◦id≡f {C} {D} {g} = sym (idL g)
  id◦f≡f : {C D : Objs} → {g : Hom C D} → id ◦ g ≡ g
  id◦f≡f {C} {D} {g} = sym (idR g)
  f◦[g◦h]≡[f◦g]◦h : {B C D E : Objs}
                    → {f : Hom B C} → {g : Hom C D} → {h : Hom D E}
                    → h ◦ (g ◦ f) ≡ (h ◦ g) ◦ f
  f◦[g◦h]≡[f◦g]◦h {B} {C} {D} {E} {f} {g} {h} = assoc f g h
  [f◦g]◦h≡f◦[g◦h] : {B C D E : Objs}
                    → {f : Hom B C} → {g : Hom C D} → {h : Hom D E}
                    → (h ◦ g) ◦ f ≡ h ◦ (g ◦ f)
  [f◦g]◦h≡f◦[g◦h] {B} {C} {D} {E} {f} {g} {h} = sym (assoc f g h)
\end{code}

  % src : {D E : Objs} → (f : Hom D E) → Objs
  % src {D} {E} f = D
  % tgt : {D E : Objs} → (f : Hom D E) → Objs
  % tgt {D} {E} f = E
  % f◦id : {D E : Objs} → {f : Hom D E} → Hom D E
  % f◦id {D} {E} {f} = f ◦ id
  % id◦f : {D E : Objs} → {f : Hom D E} → Hom D E
  % id◦f {D} {E} {f} = id ◦ f

\newpage

\begin{code}
record Functor {ℓ₀ ℓ₁ ℓ₂ ℓ₃ : Level}
               (catB : Cat {ℓ₀} {ℓ₁})
               (catA : Cat {ℓ₂} {ℓ₃})
             : Set (suc (ℓ₀ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  module A = Cat catA
  module B = Cat catB
  field
    ac0      : B.Objs → A.Objs
    ac1      : {C D : B.Objs} → (B.Hom C D) → (A.Hom (ac0 C) (ac0 D))
    respids  : {C : B.Objs} → (ac1 (B.id {C}) ≡ A.id {ac0 C})
    respcomp : {C D E : B.Objs} → {f : B.Hom C D} → {g : B.Hom D E}
               → (ac1 (g B.◦ f) ≡ ((ac1 g) A.◦ (ac1 f)))
  --
  id[FC]≡F[idC] : {C : B.Objs} → ac1 (B.id {C}) ≡ A.id {ac0 C}
  id[FC]≡F[idC] {C} = respids
  F[idC]≡id[FC] : {C : B.Objs} → A.id {ac0 C} ≡ ac1 (B.id {C})
  F[idC]≡id[FC] {C} = sym respids
  F[g◦h]≡Fg◦Fh : {C D E : B.Objs} → {f : B.Hom C D} → {g : B.Hom D E}
                 → (ac1 (g B.◦ f) ≡ ((ac1 g) A.◦ (ac1 f)))
  F[g◦h]≡Fg◦Fh {C} {D} {E} {f} {g} = respcomp
  Fg◦Fh≡F[g◦h] : {C D E : B.Objs} → {f : B.Hom C D} → {g : B.Hom D E}
                 → ((ac1 g) A.◦ (ac1 f)) ≡ (ac1 (g B.◦ f))
  Fg◦Fh≡F[g◦h] {C} {D} {E} {f} {g} = sym respcomp
  --
  -- How to use it:
  -- 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
\end{code}

  % -- open A
  % -- open B

\newpage

\begin{code}
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           
\end{code}



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

\end{document}

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

% (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")

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