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: