limits.tex

%! TEX program = xelatex
\documentclass{beamer}
\usepackage{fancyvrb}
\usepackage{color}
% \usepackage[UTF-8]{inputenc}
\usepackage{inputenc}
\DeclareUnicodeCharacter{1D49E}{\ensuremath{\mathcal{C}}}
\DeclareUnicodeCharacter{1D4A5}{\ensuremath{\mathcal{J}}}
\DeclareUnicodeCharacter{1D49F}{\ensuremath{\mathcal{D}}}
\DeclareUnicodeCharacter{2964}{\ensuremath{\Rightarrow}} %FIXME
\DeclareUnicodeCharacter{3A0}{\ensuremath{\Pi}}
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}
\DeclareUnicodeCharacter{3C0}{\ensuremath{\pi}}
\DeclareUnicodeCharacter{226B}{>>} % FIXME
\DeclareUnicodeCharacter{22D9}{>>>} % FIXME
\DeclareUnicodeCharacter{226A}{<<} % FIXME
\DeclareUnicodeCharacter{27F6}{\ensuremath{\to}}
\DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}}
\DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}}
\DeclareUnicodeCharacter{3BB}{\ensuremath{\lambda}}
\DeclareUnicodeCharacter{2245}{\ensuremath{\cong}}
\DeclareUnicodeCharacter{2190}{\ensuremath{\leftarrow}}
\DeclareUnicodeCharacter{27F9}{\ensuremath{\Rightarrow}}
\DeclareUnicodeCharacter{2192}{\ensuremath{\longrightarrow}} % FIXME
\DeclareUnicodeCharacter{3B9}{\ensuremath{\iota}}
\DeclareUnicodeCharacter{3B1}{\ensuremath{\alpha}}
\DeclareUnicodeCharacter{3B2}{\ensuremath{\beta}}
\DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}}
\DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}}




\makeatletter
\def\PY@reset{\let\PY@it=\relax \let\PY@bf=\relax%
    \let\PY@ul=\relax \let\PY@tc=\relax%
    \let\PY@bc=\relax \let\PY@ff=\relax}
\def\PY@tok#1{\csname PY@tok@#1\endcsname}
\def\PY@toks#1+{\ifx\relax#1\empty\else%
    \PY@tok{#1}\expandafter\PY@toks\fi}
\def\PY@do#1{\PY@bc{\PY@tc{\PY@ul{%
    \PY@it{\PY@bf{\PY@ff{#1}}}}}}}
\def\PY#1#2{\PY@reset\PY@toks#1+\relax+\PY@do{#2}}

\expandafter\def\csname PY@tok@gd\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.63,0.00,0.00}{##1}}}
\expandafter\def\csname PY@tok@gu\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.50,0.00,0.50}{##1}}}
\expandafter\def\csname PY@tok@gt\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.27,0.87}{##1}}}
\expandafter\def\csname PY@tok@gs\endcsname{\let\PY@bf=\textbf}
\expandafter\def\csname PY@tok@gr\endcsname{\def\PY@tc##1{\textcolor[rgb]{1.00,0.00,0.00}{##1}}}
\expandafter\def\csname PY@tok@cm\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
\expandafter\def\csname PY@tok@vg\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\expandafter\def\csname PY@tok@vi\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\expandafter\def\csname PY@tok@mh\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@cs\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
\expandafter\def\csname PY@tok@ge\endcsname{\let\PY@it=\textit}
\expandafter\def\csname PY@tok@vc\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\expandafter\def\csname PY@tok@il\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@go\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.53,0.53,0.53}{##1}}}
\expandafter\def\csname PY@tok@cp\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.74,0.48,0.00}{##1}}}
\expandafter\def\csname PY@tok@gi\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.63,0.00}{##1}}}
\expandafter\def\csname PY@tok@gh\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
\expandafter\def\csname PY@tok@ni\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
\expandafter\def\csname PY@tok@nl\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.63,0.63,0.00}{##1}}}
\expandafter\def\csname PY@tok@nn\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
\expandafter\def\csname PY@tok@no\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.53,0.00,0.00}{##1}}}
\expandafter\def\csname PY@tok@na\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.49,0.56,0.16}{##1}}}
\expandafter\def\csname PY@tok@nb\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@nc\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
\expandafter\def\csname PY@tok@nd\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
\expandafter\def\csname PY@tok@ne\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.82,0.25,0.23}{##1}}}
\expandafter\def\csname PY@tok@nf\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
\expandafter\def\csname PY@tok@si\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.73,0.40,0.53}{##1}}}
\expandafter\def\csname PY@tok@s2\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\expandafter\def\csname PY@tok@nt\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@nv\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\expandafter\def\csname PY@tok@s1\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\expandafter\def\csname PY@tok@ch\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
\expandafter\def\csname PY@tok@m\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@gp\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
\expandafter\def\csname PY@tok@sh\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\expandafter\def\csname PY@tok@ow\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
\expandafter\def\csname PY@tok@sx\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@bp\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@c1\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
\expandafter\def\csname PY@tok@kc\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@c\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
\expandafter\def\csname PY@tok@mf\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@err\endcsname{\def\PY@bc##1{\setlength{\fboxsep}{0pt}\fcolorbox[rgb]{1.00,0.00,0.00}{1,1,1}{\strut ##1}}}
\expandafter\def\csname PY@tok@mb\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@ss\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
\expandafter\def\csname PY@tok@sr\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.40,0.53}{##1}}}
\expandafter\def\csname PY@tok@mo\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@kd\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@mi\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@kn\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@o\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
\expandafter\def\csname PY@tok@kr\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@s\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\expandafter\def\csname PY@tok@kp\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@w\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.73,0.73}{##1}}}
\expandafter\def\csname PY@tok@kt\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.69,0.00,0.25}{##1}}}
\expandafter\def\csname PY@tok@sc\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\expandafter\def\csname PY@tok@sb\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
\expandafter\def\csname PY@tok@k\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
\expandafter\def\csname PY@tok@se\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.73,0.40,0.13}{##1}}}
\expandafter\def\csname PY@tok@sd\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}

\def\PYZbs{\char`\\}
\def\PYZus{\char`\_}
\def\PYZob{\char`\{}
\def\PYZcb{\char`\}}
\def\PYZca{\char`\^}
\def\PYZam{\char`\&}
\def\PYZlt{\char`\<}
\def\PYZgt{\char`\>}
\def\PYZsh{\char`\#}
\def\PYZpc{\char`\%}
\def\PYZdl{\char`\$}
\def\PYZhy{\char`\-}
\def\PYZsq{\char`\'}
\def\PYZdq{\char`\"}
\def\PYZti{\char`\~}
% for compatibility with earlier versions
\def\PYZat{@}
\def\PYZlb{[}
\def\PYZrb{]}
\makeatother


\begin{document}

\begin{frame}[fragile]

\begin{Verbatim}[commandchars=\\\{\}]
\PY{c+c1}{\PYZhy{}\PYZhy{} Copyright (c) 2018 Scott Morrison. All rights reserved.}
\PY{c+c1}{\PYZhy{}\PYZhy{} Released under Apache 2.0 license as described in the file LICENSE.}
\PY{c+c1}{\PYZhy{}\PYZhy{} Authors: Reid Barton, Mario Carneiro, Scott Morrison}

\PY{k+kn}{import} \PY{n}{category\PYZus{}theory.whiskering}
\PY{k+kn}{import} \PY{n}{category\PYZus{}theory.yoneda}
\PY{k+kn}{import} \PY{n}{category\PYZus{}theory.limits.cones}

\PY{k+kn}{open} \PY{n}{category\PYZus{}theory} \PY{n}{category\PYZus{}theory.category} \PY{n}{category\PYZus{}theory.functor}

\PY{k+kn}{namespace} \PY{n}{category\PYZus{}theory.limits}

\PY{k+kd}{universes} \PY{n}{v} \PY{n}{u} \PY{n}{u\PYZsq{}} \PY{n}{u\PYZsq{}\PYZsq{}} \PY{n}{w} \PY{c+c1}{\PYZhy{}\PYZhy{} declare the `v`\PYZsq{}s first; see `category\PYZus{}theory.category` for an explanation}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{J} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{J}\PY{o}{]}
\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{C} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n+nb+bp}{𝒞} \PY{o}{:} \PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{C}\PY{o}{]}
\PY{k+kn}{include} \PY{n+nb+bp}{𝒞}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{A}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{t}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{a}\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{d}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{i}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{e}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{t}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{structure} \PY{n}{is\PYZus{}limit} \PY{o}{(}\PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{o}{(}\PY{n}{lift}  \PY{o}{:} \PY{n+nb+bp}{Π} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)}\PY{o}{,} \PY{n}{s.X} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{)}
\PY{o}{(}\PY{n}{fac\PYZsq{}}  \PY{o}{:} \PY{n+nb+bp}{∀} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)}\PY{o}{,} \PY{n}{lift} \PY{n}{s} \PY{n+nb+bp}{≫} \PY{n}{t.π.app} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{s.π.app} \PY{n}{j} \PY{n+nb+bp}{.} \PY{n}{obviously}\PY{o}{)}
\PY{o}{(}\PY{n}{uniq\PYZsq{}} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{m} \PY{o}{:} \PY{n}{s.X} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{)} \PY{o}{(}\PY{n}{w} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{,} \PY{n}{m} \PY{n+nb+bp}{≫} \PY{n}{t.π.app} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{s.π.app} \PY{n}{j}\PY{o}{)}\PY{o}{,}
  \PY{n}{m} \PY{n+nb+bp}{=} \PY{n}{lift} \PY{n}{s} \PY{n+nb+bp}{.} \PY{n}{obviously}\PY{o}{)}

\PY{n}{restate\PYZus{}axiom} \PY{n}{is\PYZus{}limit.fac\PYZsq{}}
\PY{k+kn}{attribute} \PY{o}{[}\PY{n}{simp}\PY{o}{]} \PY{n}{is\PYZus{}limit.fac}
\PY{n}{restate\PYZus{}axiom} \PY{n}{is\PYZus{}limit.uniq\PYZsq{}}

\PY{k+kn}{namespace} \PY{n}{is\PYZus{}limit}

\PY{k+kd}{instance} \PY{n}{subsingleton} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{:} \PY{n}{subsingleton} \PY{o}{(}\PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{:=}
\PY{o}{⟨}\PY{k+kd}{by} \PY{n}{intros} \PY{n}{P} \PY{n}{Q}\PY{n+nb+bp}{;} \PY{n}{cases} \PY{n}{P}\PY{n+nb+bp}{;} \PY{n}{cases} \PY{n}{Q}\PY{n+nb+bp}{;} \PY{n}{congr}\PY{n+nb+bp}{;} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{solve\PYZus{}by\PYZus{}elim}\PY{o}{⟩}

\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{R}\PY{c+cm}{e}\PY{c+cm}{p}\PY{c+cm}{a}\PY{c+cm}{c}\PY{c+cm}{k}\PY{c+cm}{a}\PY{c+cm}{g}\PY{c+cm}{i}\PY{c+cm}{n}\PY{c+cm}{g}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{h}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{d}\PY{c+cm}{e}\PY{c+cm}{f}\PY{c+cm}{i}\PY{c+cm}{n}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{i}\PY{c+cm}{o}\PY{c+cm}{n}\PY{c+cm}{ }\PY{c+cm}{i}\PY{c+cm}{n}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{e}\PY{c+cm}{r}\PY{c+cm}{m}\PY{c+cm}{s}\PY{c+cm}{ }\PY{c+cm}{o}\PY{c+cm}{f}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{n}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{m}\PY{c+cm}{o}\PY{c+cm}{r}\PY{c+cm}{p}\PY{c+cm}{h}\PY{c+cm}{i}\PY{c+cm}{s}\PY{c+cm}{m}\PY{c+cm}{s}\PY{c+cm}{.}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}

\PY{k+kd}{def} \PY{n}{lift\PYZus{}cone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:} \PY{n}{s} \PY{n+nb+bp}{⟶} \PY{n}{t} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n}{h.lift} \PY{n}{s} \PY{o}{\PYZcb{}}

\PY{k+kd}{lemma} \PY{n}{uniq\PYZus{}cone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{s} \PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{f} \PY{n}{f\PYZsq{}} \PY{o}{:} \PY{n}{s} \PY{n+nb+bp}{⟶} \PY{n}{t}\PY{o}{\PYZcb{}} \PY{o}{:}
  \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{o}{:=}
\PY{k}{have} \PY{n+nb+bp}{∀} \PY{o}{\PYZob{}}\PY{n}{g} \PY{o}{:} \PY{n}{s} \PY{n+nb+bp}{⟶} \PY{n}{t}\PY{o}{\PYZcb{}}\PY{o}{,} \PY{n}{g} \PY{n+nb+bp}{=} \PY{n}{h.lift\PYZus{}cone\PYZus{}morphism} \PY{n}{s}\PY{o}{,} \PY{k+kd}{by} \PY{n}{intro} \PY{n}{g}\PY{n+nb+bp}{;} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{exact} \PY{n}{h.uniq} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}} \PY{n}{g.w}\PY{o}{,}
\PY{n}{this.trans} \PY{n}{this.symm}

\PY{k+kd}{def} \PY{n}{mk\PYZus{}cone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}}
  \PY{o}{(}\PY{n}{lift} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)}\PY{o}{,} \PY{n}{s} \PY{n+nb+bp}{⟶} \PY{n}{t}\PY{o}{)}
  \PY{o}{(}\PY{n}{uniq\PYZsq{}} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{m} \PY{o}{:} \PY{n}{s} \PY{n+nb+bp}{⟶} \PY{n}{t}\PY{o}{)}\PY{o}{,} \PY{n}{m} \PY{n+nb+bp}{=} \PY{n}{lift} \PY{n}{s}\PY{o}{)} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{lift} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s}\PY{o}{,} \PY{o}{(}\PY{n}{lift} \PY{n}{s}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom}\PY{o}{,}
  \PY{n}{uniq\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{m} \PY{n}{w}\PY{o}{,}
    \PY{k}{have} \PY{n}{cone\PYZus{}morphism.mk} \PY{n}{m} \PY{n}{w} \PY{n+nb+bp}{=} \PY{n}{lift} \PY{n}{s}\PY{o}{,} \PY{k+kd}{by} \PY{n}{apply} \PY{n}{uniq\PYZsq{}}\PY{o}{,}
    \PY{n}{congr\PYZus{}arg} \PY{n}{cone\PYZus{}morphism.hom} \PY{n}{this} \PY{o}{\PYZcb{}}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{L}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{i}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{p}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{o}\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{unique} \PY{o}{\PYZob{}}\PY{n}{s} \PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{P} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{s}\PY{o}{)} \PY{o}{(}\PY{n}{Q} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{:} \PY{n}{s} \PY{n+nb+bp}{≅} \PY{n}{t} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n}{Q.lift\PYZus{}cone\PYZus{}morphism} \PY{n}{s}\PY{o}{,}
  \PY{n}{inv} \PY{o}{:=} \PY{n}{P.lift\PYZus{}cone\PYZus{}morphism} \PY{n}{t}\PY{o}{,}
  \PY{n}{hom\PYZus{}inv\PYZus{}id\PYZsq{}} \PY{o}{:=} \PY{n}{P.uniq\PYZus{}cone\PYZus{}morphism}\PY{o}{,}
  \PY{n}{inv\PYZus{}hom\PYZus{}id\PYZsq{}} \PY{o}{:=} \PY{n}{Q.uniq\PYZus{}cone\PYZus{}morphism} \PY{o}{\PYZcb{}}

\PY{k+kd}{def} \PY{n}{of\PYZus{}iso\PYZus{}limit} \PY{o}{\PYZob{}}\PY{n}{r} \PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{P} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{r}\PY{o}{)} \PY{o}{(}\PY{n}{i} \PY{o}{:} \PY{n}{r} \PY{n+nb+bp}{≅} \PY{n}{t}\PY{o}{)} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t} \PY{o}{:=}
\PY{n}{is\PYZus{}limit.mk\PYZus{}cone\PYZus{}morphism}
  \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{s}\PY{o}{,} \PY{n}{P.lift\PYZus{}cone\PYZus{}morphism} \PY{n}{s} \PY{n+nb+bp}{≫} \PY{n}{i.hom}\PY{o}{)}
  \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{m}\PY{o}{,} \PY{k+kd}{by} \PY{n}{rw} \PY{n+nb+bp}{←}\PY{n}{i.comp\PYZus{}inv\PYZus{}eq}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{P.uniq\PYZus{}cone\PYZus{}morphism}\PY{o}{)}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}}

\PY{k+kd}{lemma} \PY{n}{hom\PYZus{}lift} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{m} \PY{o}{:} \PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{)} \PY{o}{:}
  \PY{n}{m} \PY{n+nb+bp}{=} \PY{n}{h.lift} \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{W}\PY{o}{,} \PY{n}{π} \PY{o}{:=} \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{b}\PY{o}{,} \PY{n}{m} \PY{n+nb+bp}{≫} \PY{n}{t.π.app} \PY{n}{b} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}} \PY{o}{:=}
\PY{n}{h.uniq} \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{W}\PY{o}{,} \PY{n}{π} \PY{o}{:=} \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{b}\PY{o}{,} \PY{n}{m} \PY{n+nb+bp}{≫} \PY{n}{t.π.app} \PY{n}{b} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}} \PY{n}{m} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{b}\PY{o}{,} \PY{n}{rfl}\PY{o}{)}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{T}\PY{l+s+sd}{w}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{n}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{i}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{m}\PY{l+s+sd}{p}\PY{l+s+sd}{o}\PY{l+s+sd}{s}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{i}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{a}\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{lemma} \PY{n}{hom\PYZus{}ext} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{f} \PY{n}{f\PYZsq{}} \PY{o}{:} \PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{\PYZcb{}}
  \PY{o}{(}\PY{n}{w} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{j}\PY{o}{,} \PY{n}{f} \PY{n+nb+bp}{≫} \PY{n}{t.π.app} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{n+nb+bp}{≫} \PY{n}{t.π.app} \PY{n}{j}\PY{o}{)} \PY{o}{:} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{rw} \PY{o}{[}\PY{n}{h.hom\PYZus{}lift} \PY{n}{f}\PY{o}{,} \PY{n}{h.hom\PYZus{}lift} \PY{n}{f\PYZsq{}}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{congr}\PY{n+nb+bp}{;} \PY{n}{exact} \PY{n}{funext} \PY{n}{w}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{T}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{i}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{s}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{p}\PY{l+s+sd}{r}\PY{l+s+sd}{o}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{y}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{:}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{W}\PY{l+s+sd}{ }\PY{l+s+sd}{⟶}\PY{l+s+sd}{ }\PY{l+s+sd}{X}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{a}\PY{l+s+sd}{m}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{s}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{e}\PY{l+s+sd}{x}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{W}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{hom\PYZus{}iso} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:} \PY{o}{(}\PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{(}\PY{o}{(}\PY{n}{const} \PY{n}{J}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{obj} \PY{n}{W} \PY{n+nb+bp}{⟹} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{f}\PY{o}{,} \PY{o}{(}\PY{n}{t.extend} \PY{n}{f}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{π}\PY{o}{,}
  \PY{n}{inv} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{π}\PY{o}{,} \PY{n}{h.lift} \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{W}\PY{o}{,} \PY{n}{π} \PY{o}{:=} \PY{n}{π} \PY{o}{\PYZcb{}}\PY{o}{,}
  \PY{n}{hom\PYZus{}inv\PYZus{}id\PYZsq{}} \PY{o}{:=} \PY{k+kd}{by} \PY{n}{ext} \PY{n}{f}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{h.hom\PYZus{}ext}\PY{n+nb+bp}{;} \PY{n}{intro} \PY{n}{j}\PY{n+nb+bp}{;} \PY{n}{simp}\PY{n+nb+bp}{;} \PY{n}{dsimp}\PY{n+nb+bp}{;} \PY{n}{refl} \PY{o}{\PYZcb{}}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{hom\PYZus{}iso\PYZus{}hom} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{is\PYZus{}limit.hom\PYZus{}iso} \PY{n}{h} \PY{n}{W}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n}{f} \PY{n+nb+bp}{=} \PY{o}{(}\PY{n}{t.extend} \PY{n}{f}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{π} \PY{o}{:=} \PY{n}{rfl}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{T}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{p}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{a}\PY{l+s+sd}{k}\PY{l+s+sd}{i}\PY{l+s+sd}{n}\PY{l+s+sd}{g}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{W}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{e}\PY{l+s+sd}{x}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{W}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{nat\PYZus{}iso} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{:} \PY{n}{yoneda.obj} \PY{n}{t.X} \PY{n+nb+bp}{≅} \PY{n}{F.cones} \PY{o}{:=}
\PY{n}{nat\PYZus{}iso.of\PYZus{}components} \PY{o}{(}\PY{n}{is\PYZus{}limit.hom\PYZus{}iso} \PY{n}{h}\PY{o}{)} \PY{o}{(}\PY{k+kd}{by} \PY{n}{tidy}\PY{o}{)}

\PY{k+kd}{def} \PY{n}{hom\PYZus{}iso\PYZsq{}} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t}\PY{o}{)} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{\PYZob{}} \PY{n}{p} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{n}{j}\PY{o}{,} \PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{F.obj} \PY{n}{j} \PY{n+nb+bp}{/}\PY{n+nb+bp}{/} \PY{n+nb+bp}{∀} \PY{o}{\PYZob{}}\PY{n}{j} \PY{n}{j\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{j\PYZsq{}}\PY{o}{)}\PY{o}{,} \PY{n}{p} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{F.map} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{p} \PY{n}{j\PYZsq{}} \PY{o}{\PYZcb{}} \PY{o}{:=}
\PY{n}{h.hom\PYZus{}iso} \PY{n}{W} \PY{n+nb+bp}{≪}\PY{n+nb+bp}{≫}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{π}\PY{o}{,}
  \PY{o}{⟨}\PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{π.app} \PY{n}{j}\PY{o}{,} \PY{n+nb+bp}{λ} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{o}{,}
   \PY{k+kd}{by} \PY{n}{convert} \PY{n+nb+bp}{←}\PY{o}{(}\PY{n}{π.naturality} \PY{n}{f}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{symm}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{id\PYZus{}comp}\PY{o}{⟩}\PY{o}{,}
  \PY{n}{inv} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{p}\PY{o}{,}
  \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{p.1} \PY{n}{j}\PY{o}{,}
    \PY{n}{naturality\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{o}{,} \PY{k+kd}{begin} \PY{n}{dsimp}\PY{o}{,} \PY{n}{rw} \PY{o}{[}\PY{n}{id\PYZus{}comp}\PY{o}{]}\PY{o}{,} \PY{n}{exact} \PY{o}{(}\PY{n}{p.2} \PY{n}{f}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{symm} \PY{k+kd}{end} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{I}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{G}\PY{l+s+sd}{ }\PY{l+s+sd}{:}\PY{l+s+sd}{ }\PY{l+s+sd}{C}\PY{l+s+sd}{ }\PY{l+s+sd}{→}\PY{l+s+sd}{ }\PY{l+s+sd}{D}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{a}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{d}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{,}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{u}\PY{l+s+sd}{f}\PY{l+s+sd}{f}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{c}\PY{l+s+sd}{k}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{n}\PY{l+s+sd}{d}\PY{l+s+sd}{u}\PY{l+s+sd}{c}\PY{l+s+sd}{e}\PY{l+s+sd}{d}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{g}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{t}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{a}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{b}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{t}\PY{l+s+sd}{e}\PY{l+s+sd}{d}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{C}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{of\PYZus{}faithful} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]} \PY{o}{(}\PY{n}{G} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)} \PY{o}{[}\PY{n}{faithful} \PY{n}{G}\PY{o}{]}
  \PY{o}{(}\PY{n}{ht} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{o}{(}\PY{n}{G.map\PYZus{}cone} \PY{n}{t}\PY{o}{)}\PY{o}{)} \PY{o}{(}\PY{n}{lift} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)}\PY{o}{,} \PY{n}{s.X} \PY{n+nb+bp}{⟶} \PY{n}{t.X}\PY{o}{)}
  \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{s}\PY{o}{,} \PY{n}{G.map} \PY{o}{(}\PY{n}{lift} \PY{n}{s}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{ht.lift} \PY{o}{(}\PY{n}{G.map\PYZus{}cone} \PY{n}{s}\PY{o}{)}\PY{o}{)} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{t} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{lift} \PY{o}{:=} \PY{n}{lift}\PY{o}{,}
  \PY{n}{fac\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{j}\PY{o}{,} \PY{k+kd}{by} \PY{n}{apply} \PY{n}{G.injectivity}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{h}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{ht.fac}\PY{o}{,}
  \PY{n}{uniq\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{m} \PY{n}{w}\PY{o}{,} \PY{k+kd}{begin}
    \PY{n}{apply} \PY{n}{G.injectivity}\PY{o}{,} \PY{n}{rw} \PY{n}{h}\PY{o}{,}
    \PY{n}{refine} \PY{n}{ht.uniq} \PY{o}{(}\PY{n}{G.map\PYZus{}cone} \PY{n}{s}\PY{o}{)} \PY{n}{\PYZus{}} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{\PYZus{}}\PY{o}{)}\PY{o}{,}
    \PY{n}{convert} \PY{n+nb+bp}{←}\PY{n}{congr\PYZus{}arg} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{f}\PY{o}{,} \PY{n}{G.map} \PY{n}{f}\PY{o}{)} \PY{o}{(}\PY{n}{w} \PY{n}{j}\PY{o}{)}\PY{o}{,}
    \PY{n}{apply} \PY{n}{G.map\PYZus{}comp}
  \PY{k+kd}{end} \PY{o}{\PYZcb{}}

\PY{k+kd}{end} \PY{n}{is\PYZus{}limit}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{A}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{t}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{a}\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{d}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{i}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{e}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{r}\PY{l+s+sd}{o}\PY{l+s+sd}{m}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{t}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{structure} \PY{n}{is\PYZus{}colimit} \PY{o}{(}\PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{o}{(}\PY{n}{desc}  \PY{o}{:} \PY{n+nb+bp}{Π} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)}\PY{o}{,} \PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{s.X}\PY{o}{)}
\PY{o}{(}\PY{n}{fac\PYZsq{}}  \PY{o}{:} \PY{n+nb+bp}{∀} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)}\PY{o}{,} \PY{n}{t.ι.app} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{desc} \PY{n}{s} \PY{n+nb+bp}{=} \PY{n}{s.ι.app} \PY{n}{j} \PY{n+nb+bp}{.} \PY{n}{obviously}\PY{o}{)}
\PY{o}{(}\PY{n}{uniq\PYZsq{}} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{m} \PY{o}{:} \PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{s.X}\PY{o}{)} \PY{o}{(}\PY{n}{w} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{,} \PY{n}{t.ι.app} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{m} \PY{n+nb+bp}{=} \PY{n}{s.ι.app} \PY{n}{j}\PY{o}{)}\PY{o}{,}
  \PY{n}{m} \PY{n+nb+bp}{=} \PY{n}{desc} \PY{n}{s} \PY{n+nb+bp}{.} \PY{n}{obviously}\PY{o}{)}

\PY{n}{restate\PYZus{}axiom} \PY{n}{is\PYZus{}colimit.fac\PYZsq{}}
\PY{k+kn}{attribute} \PY{o}{[}\PY{n}{simp}\PY{o}{]} \PY{n}{is\PYZus{}colimit.fac}
\PY{n}{restate\PYZus{}axiom} \PY{n}{is\PYZus{}colimit.uniq\PYZsq{}}

\PY{k+kn}{namespace} \PY{n}{is\PYZus{}colimit}

\PY{k+kd}{instance} \PY{n}{subsingleton} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{:} \PY{n}{subsingleton} \PY{o}{(}\PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{:=}
\PY{o}{⟨}\PY{k+kd}{by} \PY{n}{intros} \PY{n}{P} \PY{n}{Q}\PY{n+nb+bp}{;} \PY{n}{cases} \PY{n}{P}\PY{n+nb+bp}{;} \PY{n}{cases} \PY{n}{Q}\PY{n+nb+bp}{;} \PY{n}{congr}\PY{n+nb+bp}{;} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{solve\PYZus{}by\PYZus{}elim}\PY{o}{⟩}

\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{R}\PY{c+cm}{e}\PY{c+cm}{p}\PY{c+cm}{a}\PY{c+cm}{c}\PY{c+cm}{k}\PY{c+cm}{a}\PY{c+cm}{g}\PY{c+cm}{i}\PY{c+cm}{n}\PY{c+cm}{g}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{h}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{d}\PY{c+cm}{e}\PY{c+cm}{f}\PY{c+cm}{i}\PY{c+cm}{n}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{i}\PY{c+cm}{o}\PY{c+cm}{n}\PY{c+cm}{ }\PY{c+cm}{i}\PY{c+cm}{n}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{e}\PY{c+cm}{r}\PY{c+cm}{m}\PY{c+cm}{s}\PY{c+cm}{ }\PY{c+cm}{o}\PY{c+cm}{f}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{n}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{m}\PY{c+cm}{o}\PY{c+cm}{r}\PY{c+cm}{p}\PY{c+cm}{h}\PY{c+cm}{i}\PY{c+cm}{s}\PY{c+cm}{m}\PY{c+cm}{s}\PY{c+cm}{.}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}

\PY{k+kd}{def} \PY{n}{desc\PYZus{}cocone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:} \PY{n}{t} \PY{n+nb+bp}{⟶} \PY{n}{s} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n}{h.desc} \PY{n}{s} \PY{o}{\PYZcb{}}

\PY{k+kd}{lemma} \PY{n}{uniq\PYZus{}cocone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{s} \PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{f} \PY{n}{f\PYZsq{}} \PY{o}{:} \PY{n}{t} \PY{n+nb+bp}{⟶} \PY{n}{s}\PY{o}{\PYZcb{}} \PY{o}{:}
  \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{o}{:=}
\PY{k}{have} \PY{n+nb+bp}{∀} \PY{o}{\PYZob{}}\PY{n}{g} \PY{o}{:} \PY{n}{t} \PY{n+nb+bp}{⟶} \PY{n}{s}\PY{o}{\PYZcb{}}\PY{o}{,} \PY{n}{g} \PY{n+nb+bp}{=} \PY{n}{h.desc\PYZus{}cocone\PYZus{}morphism} \PY{n}{s}\PY{o}{,} \PY{k+kd}{by} \PY{n}{intro} \PY{n}{g}\PY{n+nb+bp}{;} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{exact} \PY{n}{h.uniq} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}} \PY{n}{g.w}\PY{o}{,}
\PY{n}{this.trans} \PY{n}{this.symm}

\PY{k+kd}{def} \PY{n}{mk\PYZus{}cocone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}}
  \PY{o}{(}\PY{n}{desc} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)}\PY{o}{,} \PY{n}{t} \PY{n+nb+bp}{⟶} \PY{n}{s}\PY{o}{)}
  \PY{o}{(}\PY{n}{uniq\PYZsq{}} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{m} \PY{o}{:} \PY{n}{t} \PY{n+nb+bp}{⟶} \PY{n}{s}\PY{o}{)}\PY{o}{,} \PY{n}{m} \PY{n+nb+bp}{=} \PY{n}{desc} \PY{n}{s}\PY{o}{)} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{desc} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s}\PY{o}{,} \PY{o}{(}\PY{n}{desc} \PY{n}{s}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom}\PY{o}{,}
  \PY{n}{uniq\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{m} \PY{n}{w}\PY{o}{,}
    \PY{k}{have} \PY{n}{cocone\PYZus{}morphism.mk} \PY{n}{m} \PY{n}{w} \PY{n+nb+bp}{=} \PY{n}{desc} \PY{n}{s}\PY{o}{,} \PY{k+kd}{by} \PY{n}{apply} \PY{n}{uniq\PYZsq{}}\PY{o}{,}
    \PY{n}{congr\PYZus{}arg} \PY{n}{cocone\PYZus{}morphism.hom} \PY{n}{this} \PY{o}{\PYZcb{}}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{L}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{i}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{p}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{o}\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{unique} \PY{o}{\PYZob{}}\PY{n}{s} \PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{P} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{s}\PY{o}{)} \PY{o}{(}\PY{n}{Q} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{:} \PY{n}{s} \PY{n+nb+bp}{≅} \PY{n}{t} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n}{P.desc\PYZus{}cocone\PYZus{}morphism} \PY{n}{t}\PY{o}{,}
  \PY{n}{inv} \PY{o}{:=} \PY{n}{Q.desc\PYZus{}cocone\PYZus{}morphism} \PY{n}{s}\PY{o}{,}
  \PY{n}{hom\PYZus{}inv\PYZus{}id\PYZsq{}} \PY{o}{:=} \PY{n}{P.uniq\PYZus{}cocone\PYZus{}morphism}\PY{o}{,}
  \PY{n}{inv\PYZus{}hom\PYZus{}id\PYZsq{}} \PY{o}{:=} \PY{n}{Q.uniq\PYZus{}cocone\PYZus{}morphism} \PY{o}{\PYZcb{}}

\PY{k+kd}{def} \PY{n}{of\PYZus{}iso\PYZus{}colimit} \PY{o}{\PYZob{}}\PY{n}{r} \PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{P} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{r}\PY{o}{)} \PY{o}{(}\PY{n}{i} \PY{o}{:} \PY{n}{r} \PY{n+nb+bp}{≅} \PY{n}{t}\PY{o}{)} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t} \PY{o}{:=}
\PY{n}{is\PYZus{}colimit.mk\PYZus{}cocone\PYZus{}morphism}
  \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{s}\PY{o}{,} \PY{n}{i.inv} \PY{n+nb+bp}{≫} \PY{n}{P.desc\PYZus{}cocone\PYZus{}morphism} \PY{n}{s}\PY{o}{)}
  \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{m}\PY{o}{,} \PY{k+kd}{by} \PY{n}{rw} \PY{n}{i.eq\PYZus{}inv\PYZus{}comp}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{P.uniq\PYZus{}cocone\PYZus{}morphism}\PY{o}{)}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}}

\PY{k+kd}{lemma} \PY{n}{hom\PYZus{}desc} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{m} \PY{o}{:} \PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{)} \PY{o}{:}
  \PY{n}{m} \PY{n+nb+bp}{=} \PY{n}{h.desc} \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{W}\PY{o}{,} \PY{n}{ι} \PY{o}{:=} \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{b}\PY{o}{,} \PY{n}{t.ι.app} \PY{n}{b} \PY{n+nb+bp}{≫} \PY{n}{m}\PY{o}{,}
    \PY{n}{naturality\PYZsq{}} \PY{o}{:=} \PY{k+kd}{by} \PY{n}{intros}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{t.ι.naturality}\PY{o}{,} \PY{n}{comp\PYZus{}id}\PY{o}{,} \PY{n}{comp\PYZus{}id}\PY{o}{]} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}} \PY{o}{:=}
\PY{n}{h.uniq} \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{W}\PY{o}{,} \PY{n}{ι} \PY{o}{:=} \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{b}\PY{o}{,} \PY{n}{t.ι.app} \PY{n}{b} \PY{n+nb+bp}{≫} \PY{n}{m}\PY{o}{,} \PY{n}{naturality\PYZsq{}} \PY{o}{:=} \PY{n}{\PYZus{}} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}} \PY{n}{m} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{b}\PY{o}{,} \PY{n}{rfl}\PY{o}{)}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{T}\PY{l+s+sd}{w}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{u}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{i}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{m}\PY{l+s+sd}{p}\PY{l+s+sd}{o}\PY{l+s+sd}{s}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{i}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{a}\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{p}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{q}\PY{l+s+sd}{u}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{lemma} \PY{n}{hom\PYZus{}ext} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{f} \PY{n}{f\PYZsq{}} \PY{o}{:} \PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{\PYZcb{}}
  \PY{o}{(}\PY{n}{w} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{j}\PY{o}{,} \PY{n}{t.ι.app} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{t.ι.app} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{f\PYZsq{}}\PY{o}{)} \PY{o}{:} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{rw} \PY{o}{[}\PY{n}{h.hom\PYZus{}desc} \PY{n}{f}\PY{o}{,} \PY{n}{h.hom\PYZus{}desc} \PY{n}{f\PYZsq{}}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{congr}\PY{n+nb+bp}{;} \PY{n}{exact} \PY{n}{funext} \PY{n}{w}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{T}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{i}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{s}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{p}\PY{l+s+sd}{r}\PY{l+s+sd}{o}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{y}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{:}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{X}\PY{l+s+sd}{ }\PY{l+s+sd}{⟶}\PY{l+s+sd}{ }\PY{l+s+sd}{W}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{a}\PY{l+s+sd}{m}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{s}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{e}\PY{l+s+sd}{x}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{W}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{hom\PYZus{}iso} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:} \PY{o}{(}\PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⟹} \PY{o}{(}\PY{n}{const} \PY{n}{J}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{obj} \PY{n}{W}\PY{o}{)} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{f}\PY{o}{,} \PY{o}{(}\PY{n}{t.extend} \PY{n}{f}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{ι}\PY{o}{,}
  \PY{n}{inv} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{ι}\PY{o}{,} \PY{n}{h.desc} \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{W}\PY{o}{,} \PY{n}{ι} \PY{o}{:=} \PY{n}{ι} \PY{o}{\PYZcb{}}\PY{o}{,}
  \PY{n}{hom\PYZus{}inv\PYZus{}id\PYZsq{}} \PY{o}{:=} \PY{k+kd}{by} \PY{n}{ext} \PY{n}{f}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{h.hom\PYZus{}ext}\PY{n+nb+bp}{;} \PY{n}{intro} \PY{n}{j}\PY{n+nb+bp}{;} \PY{n}{simp}\PY{n+nb+bp}{;} \PY{n}{dsimp}\PY{n+nb+bp}{;} \PY{n}{refl} \PY{o}{\PYZcb{}}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{hom\PYZus{}iso\PYZus{}hom} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{is\PYZus{}colimit.hom\PYZus{}iso} \PY{n}{h} \PY{n}{W}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n}{f} \PY{n+nb+bp}{=} \PY{o}{(}\PY{n}{t.extend} \PY{n}{f}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{ι} \PY{o}{:=} \PY{n}{rfl}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{T}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{p}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{a}\PY{l+s+sd}{k}\PY{l+s+sd}{i}\PY{l+s+sd}{n}\PY{l+s+sd}{g}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{W}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{e}\PY{l+s+sd}{x}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{W}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{nat\PYZus{}iso} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{:} \PY{n}{coyoneda.obj} \PY{n}{t.X} \PY{n+nb+bp}{≅} \PY{n}{F.cocones} \PY{o}{:=}
\PY{n}{nat\PYZus{}iso.of\PYZus{}components} \PY{o}{(}\PY{n}{is\PYZus{}colimit.hom\PYZus{}iso} \PY{n}{h}\PY{o}{)} \PY{o}{(}\PY{k+kd}{by} \PY{n}{intros}\PY{n+nb+bp}{;} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{dsimp}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{n+nb+bp}{;} \PY{n}{refl}\PY{o}{)}

\PY{k+kd}{def} \PY{n}{hom\PYZus{}iso\PYZsq{}} \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t}\PY{o}{)} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{\PYZob{}} \PY{n}{p} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{n}{j}\PY{o}{,} \PY{n}{F.obj} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{W} \PY{n+nb+bp}{/}\PY{n+nb+bp}{/} \PY{n+nb+bp}{∀} \PY{o}{\PYZob{}}\PY{n}{j} \PY{n}{j\PYZsq{}} \PY{o}{:} \PY{n}{J}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{j\PYZsq{}}\PY{o}{)}\PY{o}{,} \PY{n}{F.map} \PY{n}{f} \PY{n+nb+bp}{≫} \PY{n}{p} \PY{n}{j\PYZsq{}} \PY{n+nb+bp}{=} \PY{n}{p} \PY{n}{j} \PY{o}{\PYZcb{}} \PY{o}{:=}
\PY{n}{h.hom\PYZus{}iso} \PY{n}{W} \PY{n+nb+bp}{≪}\PY{n+nb+bp}{≫}
\PY{o}{\PYZob{}} \PY{n}{hom} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{ι}\PY{o}{,}
  \PY{o}{⟨}\PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{ι.app} \PY{n}{j}\PY{o}{,} \PY{n+nb+bp}{λ} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{o}{,}
   \PY{k+kd}{by} \PY{n}{convert} \PY{n+nb+bp}{←}\PY{o}{(}\PY{n}{ι.naturality} \PY{n}{f}\PY{o}{)}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{comp\PYZus{}id}\PY{o}{⟩}\PY{o}{,}
  \PY{n}{inv} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{p}\PY{o}{,}
  \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{p.1} \PY{n}{j}\PY{o}{,}
    \PY{n}{naturality\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{o}{,} \PY{k+kd}{begin} \PY{n}{dsimp}\PY{o}{,} \PY{n}{rw} \PY{o}{[}\PY{n}{comp\PYZus{}id}\PY{o}{]}\PY{o}{,} \PY{n}{exact} \PY{o}{(}\PY{n}{p.2} \PY{n}{f}\PY{o}{)} \PY{k+kd}{end} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{I}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{G}\PY{l+s+sd}{ }\PY{l+s+sd}{:}\PY{l+s+sd}{ }\PY{l+s+sd}{C}\PY{l+s+sd}{ }\PY{l+s+sd}{→}\PY{l+s+sd}{ }\PY{l+s+sd}{D}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{a}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{h}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{d}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{n}\PY{l+s+sd}{e}\PY{l+s+sd}{,}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{u}\PY{l+s+sd}{f}\PY{l+s+sd}{f}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{c}\PY{l+s+sd}{k}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{n}\PY{l+s+sd}{d}\PY{l+s+sd}{u}\PY{l+s+sd}{c}\PY{l+s+sd}{e}\PY{l+s+sd}{d}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{g}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{t}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{a}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{b}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{t}\PY{l+s+sd}{e}\PY{l+s+sd}{d}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{ }\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{C}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{of\PYZus{}faithful} \PY{o}{\PYZob{}}\PY{n}{t} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]} \PY{o}{(}\PY{n}{G} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)} \PY{o}{[}\PY{n}{faithful} \PY{n}{G}\PY{o}{]}
  \PY{o}{(}\PY{n}{ht} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{o}{(}\PY{n}{G.map\PYZus{}cocone} \PY{n}{t}\PY{o}{)}\PY{o}{)} \PY{o}{(}\PY{n}{desc} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{o}{(}\PY{n}{s} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)}\PY{o}{,} \PY{n}{t.X} \PY{n+nb+bp}{⟶} \PY{n}{s.X}\PY{o}{)}
  \PY{o}{(}\PY{n}{h} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{s}\PY{o}{,} \PY{n}{G.map} \PY{o}{(}\PY{n}{desc} \PY{n}{s}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{ht.desc} \PY{o}{(}\PY{n}{G.map\PYZus{}cocone} \PY{n}{s}\PY{o}{)}\PY{o}{)} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{t} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{desc} \PY{o}{:=} \PY{n}{desc}\PY{o}{,}
  \PY{n}{fac\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{j}\PY{o}{,} \PY{k+kd}{by} \PY{n}{apply} \PY{n}{G.injectivity}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{h}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{apply} \PY{n}{ht.fac}\PY{o}{,}
  \PY{n}{uniq\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{s} \PY{n}{m} \PY{n}{w}\PY{o}{,} \PY{k+kd}{begin}
    \PY{n}{apply} \PY{n}{G.injectivity}\PY{o}{,} \PY{n}{rw} \PY{n}{h}\PY{o}{,}
    \PY{n}{refine} \PY{n}{ht.uniq} \PY{o}{(}\PY{n}{G.map\PYZus{}cocone} \PY{n}{s}\PY{o}{)} \PY{n}{\PYZus{}} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{\PYZus{}}\PY{o}{)}\PY{o}{,}
    \PY{n}{convert} \PY{n+nb+bp}{←}\PY{n}{congr\PYZus{}arg} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{f}\PY{o}{,} \PY{n}{G.map} \PY{n}{f}\PY{o}{)} \PY{o}{(}\PY{n}{w} \PY{n}{j}\PY{o}{)}\PY{o}{,}
    \PY{n}{apply} \PY{n}{G.map\PYZus{}comp}
  \PY{k+kd}{end} \PY{o}{\PYZcb{}}

\PY{k+kd}{end} \PY{n}{is\PYZus{}colimit}

\PY{k+kn}{section} \PY{n}{limit}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{\PYZus{}}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{p}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{p}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{u}\PY{l+s+sd}{l}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{o}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{d}\PY{l+s+sd}{i}\PY{l+s+sd}{a}\PY{l+s+sd}{g}\PY{l+s+sd}{r}\PY{l+s+sd}{a}\PY{l+s+sd}{m}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{class} \PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{:=}
\PY{o}{(}\PY{n}{cone} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)}
\PY{o}{(}\PY{n}{is\PYZus{}limit} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{n}{cone}\PY{o}{)}

\PY{k+kd}{variables} \PY{o}{(}\PY{n}{J} \PY{n}{C}\PY{o}{)}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{J}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{o}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{p}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{u}\PY{l+s+sd}{l}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{y}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{ }\PY{l+s+sd}{:}\PY{l+s+sd}{ }\PY{l+s+sd}{J}\PY{l+s+sd}{ }\PY{l+s+sd}{⥤}\PY{l+s+sd}{ }\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{@[class]} \PY{k+kd}{def} \PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape} \PY{o}{:=} \PY{n+nb+bp}{Π} \PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{,} \PY{n}{has\PYZus{}limit} \PY{n}{F}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{(}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{l}\PY{l+s+sd}{)}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{y}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{@[class]} \PY{k+kd}{def} \PY{n}{has\PYZus{}limits} \PY{o}{:=}
\PY{n+nb+bp}{Π} \PY{o}{\PYZob{}}\PY{n}{J} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n+nb+bp}{𝒥} \PY{o}{:} \PY{n}{small\PYZus{}category} \PY{n}{J}\PY{o}{\PYZcb{}}\PY{o}{,} \PY{k+kd}{by} \PY{n}{exactI} \PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{J} \PY{n}{C}\PY{o}{\PYZcb{}}

\PY{k+kd}{instance} \PY{n}{has\PYZus{}limit\PYZus{}of\PYZus{}has\PYZus{}limits\PYZus{}of\PYZus{}shape}
  \PY{o}{\PYZob{}}\PY{n}{J} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{J}\PY{o}{]} \PY{o}{[}\PY{n}{H} \PY{o}{:} \PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C}\PY{o}{]} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{:} \PY{n}{has\PYZus{}limit} \PY{n}{F} \PY{o}{:=}
\PY{n}{H} \PY{n}{F}

\PY{k+kd}{instance} \PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape\PYZus{}of\PYZus{}has\PYZus{}limits}
  \PY{o}{\PYZob{}}\PY{n}{J} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{J}\PY{o}{]} \PY{o}{[}\PY{n}{H} \PY{o}{:} \PY{n}{has\PYZus{}limits.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{C}\PY{o}{]} \PY{o}{:} \PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C} \PY{o}{:=}
\PY{n}{H}

\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{I}\PY{c+cm}{n}\PY{c+cm}{t}\PY{c+cm}{e}\PY{c+cm}{r}\PY{c+cm}{f}\PY{c+cm}{a}\PY{c+cm}{c}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{o}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{h}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{`}\PY{c+cm}{h}\PY{c+cm}{a}\PY{c+cm}{s}\PY{c+cm}{\PYZus{}}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{`}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{l}\PY{c+cm}{a}\PY{c+cm}{s}\PY{c+cm}{s}\PY{c+cm}{.}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}

\PY{k+kd}{def} \PY{n}{limit.cone} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{:} \PY{n}{cone} \PY{n}{F} \PY{o}{:=} \PY{n}{has\PYZus{}limit.cone} \PY{n}{F}

\PY{k+kd}{def} \PY{n}{limit} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{:=} \PY{o}{(}\PY{n}{limit.cone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{X}

\PY{k+kd}{def} \PY{n}{limit.π} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:} \PY{n}{limit} \PY{n}{F} \PY{n+nb+bp}{⟶} \PY{n}{F.obj} \PY{n}{j} \PY{o}{:=}
\PY{o}{(}\PY{n}{limit.cone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{π.app} \PY{n}{j}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.cone\PYZus{}π} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{limit.cone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{π.app} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{limit.π} \PY{n}{\PYZus{}} \PY{n}{j} \PY{o}{:=} \PY{n}{rfl}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.w} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{j} \PY{n}{j\PYZsq{}} \PY{o}{:} \PY{n}{J}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{j\PYZsq{}}\PY{o}{)} \PY{o}{:}
  \PY{n}{limit.π} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{F.map} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{limit.π} \PY{n}{F} \PY{n}{j\PYZsq{}} \PY{o}{:=} \PY{o}{(}\PY{n}{limit.cone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{w} \PY{n}{f}

\PY{k+kd}{def} \PY{n}{limit.is\PYZus{}limit} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{:} \PY{n}{is\PYZus{}limit} \PY{o}{(}\PY{n}{limit.cone} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{n}{has\PYZus{}limit.is\PYZus{}limit.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{F}

\PY{k+kd}{def} \PY{n}{limit.lift} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:} \PY{n}{c.X} \PY{n+nb+bp}{⟶} \PY{n}{limit} \PY{n}{F} \PY{o}{:=}
\PY{o}{(}\PY{n}{limit.is\PYZus{}limit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{lift} \PY{n}{c}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.is\PYZus{}limit\PYZus{}lift} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{limit.is\PYZus{}limit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{lift} \PY{n}{c} \PY{n+nb+bp}{=} \PY{n}{limit.lift} \PY{n}{F} \PY{n}{c} \PY{o}{:=} \PY{n}{rfl}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.lift\PYZus{}π} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{n}{limit.lift} \PY{n}{F} \PY{n}{c} \PY{n+nb+bp}{≫} \PY{n}{limit.π} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{c.π.app} \PY{n}{j} \PY{o}{:=}
\PY{n}{is\PYZus{}limit.fac} \PY{n}{\PYZus{}} \PY{n}{c} \PY{n}{j}

\PY{k+kd}{def} \PY{n}{limit.cone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{n}{cone\PYZus{}morphism} \PY{n}{c} \PY{o}{(}\PY{n}{limit.cone} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{o}{(}\PY{n}{limit.is\PYZus{}limit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{lift\PYZus{}cone\PYZus{}morphism} \PY{n}{c}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.cone\PYZus{}morphism\PYZus{}hom} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{limit.cone\PYZus{}morphism} \PY{n}{c}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n+nb+bp}{=} \PY{n}{limit.lift} \PY{n}{F} \PY{n}{c} \PY{o}{:=} \PY{n}{rfl}
\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.cone\PYZus{}morphism\PYZus{}π} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{limit.cone\PYZus{}morphism} \PY{n}{c}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n+nb+bp}{≫} \PY{n}{limit.π} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{c.π.app} \PY{n}{j} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{erw} \PY{n}{is\PYZus{}limit.fac}

\PY{k+kd}{@[extensionality]} \PY{k+kd}{lemma} \PY{n}{limit.hom\PYZus{}ext} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{X} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{f} \PY{n}{f\PYZsq{}} \PY{o}{:} \PY{n}{X} \PY{n+nb+bp}{⟶} \PY{n}{limit} \PY{n}{F}\PY{o}{\PYZcb{}}
  \PY{o}{(}\PY{n}{w} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{j}\PY{o}{,} \PY{n}{f} \PY{n+nb+bp}{≫} \PY{n}{limit.π} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{n+nb+bp}{≫} \PY{n}{limit.π} \PY{n}{F} \PY{n}{j}\PY{o}{)} \PY{o}{:} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{o}{:=}
\PY{o}{(}\PY{n}{limit.is\PYZus{}limit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}ext} \PY{n}{w}

\PY{k+kd}{def} \PY{n}{limit.hom\PYZus{}iso} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:} \PY{o}{(}\PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{limit} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{(}\PY{n}{F.cones.obj} \PY{n}{W}\PY{o}{)} \PY{o}{:=}
\PY{o}{(}\PY{n}{limit.is\PYZus{}limit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}iso} \PY{n}{W}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.hom\PYZus{}iso\PYZus{}hom} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{limit} \PY{n}{F}\PY{o}{)}\PY{o}{:}
  \PY{o}{(}\PY{n}{limit.hom\PYZus{}iso} \PY{n}{F} \PY{n}{W}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n}{f} \PY{n+nb+bp}{=} \PY{o}{(}\PY{n}{const} \PY{n}{J}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{map} \PY{n}{f} \PY{n+nb+bp}{≫} \PY{o}{(}\PY{n}{limit.cone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{π} \PY{o}{:=}
\PY{o}{(}\PY{n}{limit.is\PYZus{}limit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}iso\PYZus{}hom} \PY{n}{f}

\PY{k+kd}{def} \PY{n}{limit.hom\PYZus{}iso\PYZsq{}} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{limit} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{\PYZob{}} \PY{n}{p} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{n}{j}\PY{o}{,} \PY{n}{W} \PY{n+nb+bp}{⟶} \PY{n}{F.obj} \PY{n}{j} \PY{n+nb+bp}{/}\PY{n+nb+bp}{/} \PY{n+nb+bp}{∀} \PY{o}{\PYZob{}}\PY{n}{j} \PY{n}{j\PYZsq{}} \PY{o}{:} \PY{n}{J}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{j\PYZsq{}}\PY{o}{)}\PY{o}{,} \PY{n}{p} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{F.map} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{p} \PY{n}{j\PYZsq{}} \PY{o}{\PYZcb{}} \PY{o}{:=}
\PY{o}{(}\PY{n}{limit.is\PYZus{}limit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}iso\PYZsq{}} \PY{n}{W}

\PY{k+kd}{lemma} \PY{n}{limit.lift\PYZus{}extend} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{X} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{X} \PY{n+nb+bp}{⟶} \PY{n}{c.X}\PY{o}{)} \PY{o}{:}
  \PY{n}{limit.lift} \PY{n}{F} \PY{o}{(}\PY{n}{c.extend} \PY{n}{f}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{f} \PY{n+nb+bp}{≫} \PY{n}{limit.lift} \PY{n}{F} \PY{n}{c} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{obviously}

\PY{k+kn}{section} \PY{n}{pre}
\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]}
\PY{k+kd}{variables} \PY{o}{(}\PY{n}{F}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{E} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}\PY{o}{]}

\PY{k+kd}{def} \PY{n}{limit.pre} \PY{o}{:} \PY{n}{limit} \PY{n}{F} \PY{n+nb+bp}{⟶} \PY{n}{limit} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{n}{limit.lift} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}
  \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{limit} \PY{n}{F}\PY{o}{,}
    \PY{n}{π} \PY{o}{:=} \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{k}\PY{o}{,} \PY{n}{limit.π} \PY{n}{F} \PY{o}{(}\PY{n}{E.obj} \PY{n}{k}\PY{o}{)} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.pre\PYZus{}π} \PY{o}{(}\PY{n}{k} \PY{o}{:} \PY{n}{K}\PY{o}{)} \PY{o}{:} \PY{n}{limit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{≫} \PY{n}{limit.π} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n}{k} \PY{n+nb+bp}{=} \PY{n}{limit.π} \PY{n}{F} \PY{o}{(}\PY{n}{E.obj} \PY{n}{k}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{erw} \PY{n}{is\PYZus{}limit.fac}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.lift\PYZus{}pre} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{n}{limit.lift} \PY{n}{F} \PY{n}{c} \PY{n+nb+bp}{≫} \PY{n}{limit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{=} \PY{n}{limit.lift} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{c.whisker} \PY{n}{E}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{simp}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{L} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{L}\PY{o}{]}
\PY{k+kd}{variables} \PY{o}{(}\PY{n}{D} \PY{o}{:} \PY{n}{L} \PY{n+nb+bp}{⥤} \PY{n}{K}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{n}{D} \PY{n+nb+bp}{⋙} \PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}\PY{o}{]}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.pre\PYZus{}pre} \PY{o}{:} \PY{n}{limit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{≫} \PY{n}{limit.pre} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n}{D} \PY{n+nb+bp}{=} \PY{n}{limit.pre} \PY{n}{F} \PY{o}{(}\PY{n}{D} \PY{n+nb+bp}{⋙} \PY{n}{E}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext} \PY{n}{j}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.pre\PYZus{}π}\PY{o}{,} \PY{n}{limit.pre\PYZus{}π}\PY{o}{,} \PY{n}{limit.pre\PYZus{}π}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{end} \PY{n}{pre}

\PY{k+kn}{section} \PY{n}{post}
\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n+nb+bp}{𝒟} \PY{o}{:} \PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]}
\PY{k+kn}{include} \PY{n+nb+bp}{𝒟}

\PY{k+kd}{variables} \PY{o}{(}\PY{n}{F}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{G} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}\PY{o}{]}

\PY{k+kd}{def} \PY{n}{limit.post} \PY{o}{:} \PY{n}{G.obj} \PY{o}{(}\PY{n}{limit} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{⟶} \PY{n}{limit} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{o}{:=}
\PY{n}{limit.lift} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}
\PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{G.obj} \PY{o}{(}\PY{n}{limit} \PY{n}{F}\PY{o}{)}\PY{o}{,}
  \PY{n}{π} \PY{o}{:=}
  \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{G.map} \PY{o}{(}\PY{n}{limit.π} \PY{n}{F} \PY{n}{j}\PY{o}{)}\PY{o}{,}
    \PY{n}{naturality\PYZsq{}} \PY{o}{:=}
      \PY{k+kd}{by} \PY{n}{intros} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{limits.cone.w}\PY{o}{,} \PY{n}{id\PYZus{}comp}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.post\PYZus{}π} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:} \PY{n}{limit.post} \PY{n}{F} \PY{n}{G} \PY{n+nb+bp}{≫} \PY{n}{limit.π} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{G.map} \PY{o}{(}\PY{n}{limit.π} \PY{n}{F} \PY{n}{j}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{erw} \PY{n}{is\PYZus{}limit.fac}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.lift\PYZus{}post} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{n}{G.map} \PY{o}{(}\PY{n}{limit.lift} \PY{n}{F} \PY{n}{c}\PY{o}{)} \PY{n+nb+bp}{≫} \PY{n}{limit.post} \PY{n}{F} \PY{n}{G} \PY{n+nb+bp}{=} \PY{n}{limit.lift} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{o}{(}\PY{n}{G.map\PYZus{}cone} \PY{n}{c}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{limit.lift\PYZus{}π}\PY{o}{,} \PY{n}{limit.lift\PYZus{}π}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.post\PYZus{}post}
  \PY{o}{\PYZob{}}\PY{n}{E} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{E}\PY{o}{]} \PY{o}{(}\PY{n}{H} \PY{o}{:} \PY{n}{D} \PY{n+nb+bp}{⥤} \PY{n}{E}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n+nb+bp}{⋙} \PY{n}{H}\PY{o}{)}\PY{o}{]} \PY{o}{:}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{e}\PY{c+cm}{q}\PY{c+cm}{u}\PY{c+cm}{a}\PY{c+cm}{l}\PY{c+cm}{s}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
  \PY{n}{H.map} \PY{o}{(}\PY{n}{limit.post} \PY{n}{F} \PY{n}{G}\PY{o}{)} \PY{n+nb+bp}{≫} \PY{n}{limit.post} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n}{H} \PY{n+nb+bp}{=} \PY{n}{limit.post} \PY{n}{F} \PY{o}{(}\PY{n}{G} \PY{n+nb+bp}{⋙} \PY{n}{H}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{H.map\PYZus{}comp}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{end} \PY{n}{post}

\PY{k+kd}{lemma} \PY{n}{limit.pre\PYZus{}post} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]}
  \PY{o}{(}\PY{n}{E} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{)} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{(}\PY{n}{G} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)}
  \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{n}{F}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}limit} \PY{o}{(}\PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}\PY{o}{]} \PY{o}{:}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{E}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{(}\PY{c+cm}{E}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{v}\PY{c+cm}{s}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{E}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{o}\PY{c+cm}{r}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
  \PY{n}{G.map} \PY{o}{(}\PY{n}{limit.pre} \PY{n}{F} \PY{n}{E}\PY{o}{)} \PY{n+nb+bp}{≫} \PY{n}{limit.post} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n}{G} \PY{n+nb+bp}{=} \PY{n}{limit.post} \PY{n}{F} \PY{n}{G} \PY{n+nb+bp}{≫} \PY{n}{limit.pre} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n}{E} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{limit.pre\PYZus{}π}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n}{limit.pre\PYZus{}π}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kn}{section} \PY{n}{lim\PYZus{}functor}

\PY{k+kd}{variables} \PY{o}{[}\PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C}\PY{o}{]}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{i}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{,}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{J}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{lim} \PY{o}{:} \PY{o}{(}\PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{n+nb+bp}{⥤} \PY{n}{C} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{obj} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{F}\PY{o}{,} \PY{n}{limit} \PY{n}{F}\PY{o}{,}
  \PY{n}{map} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{F} \PY{n}{G} \PY{n}{α}\PY{o}{,} \PY{n}{limit.lift} \PY{n}{G}
    \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{limit} \PY{n}{F}\PY{o}{,}
      \PY{n}{π} \PY{o}{:=}
      \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{limit.π} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{α.app} \PY{n}{j}\PY{o}{,}
        \PY{n}{naturality\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{o}{,}
          \PY{k+kd}{by} \PY{n}{erw} \PY{o}{[}\PY{n}{id\PYZus{}comp}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{α.naturality}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.w}\PY{o}{]} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}\PY{o}{,}
  \PY{n}{map\PYZus{}comp\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{F} \PY{n}{G} \PY{n}{H} \PY{n}{α} \PY{n}{β}\PY{o}{,}
    \PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{is\PYZus{}limit.fac}\PY{o}{,} \PY{n}{is\PYZus{}limit.fac}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{is\PYZus{}limit.fac}\PY{o}{,} \PY{n}{assoc}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl} \PY{o}{\PYZcb{}}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{G} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{α} \PY{o}{:} \PY{n}{F} \PY{n+nb+bp}{⟹} \PY{n}{G}\PY{o}{)}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{lim.map\PYZus{}π} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:} \PY{n}{lim.map} \PY{n}{α} \PY{n+nb+bp}{≫} \PY{n}{limit.π} \PY{n}{G} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{limit.π} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{α.app} \PY{n}{j} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{apply} \PY{n}{is\PYZus{}limit.fac}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{limit.lift\PYZus{}map} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{n}{limit.lift} \PY{n}{F} \PY{n}{c} \PY{n+nb+bp}{≫} \PY{n}{lim.map} \PY{n}{α} \PY{n+nb+bp}{=} \PY{n}{limit.lift} \PY{n}{G} \PY{o}{(}\PY{n}{c.postcompose} \PY{n}{α}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{lim.map\PYZus{}π}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.lift\PYZus{}π}\PY{o}{,} \PY{n}{limit.lift\PYZus{}π}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{lemma} \PY{n}{limit.map\PYZus{}pre} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape} \PY{n}{K} \PY{n}{C}\PY{o}{]} \PY{o}{(}\PY{n}{E} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{n}{lim.map} \PY{n}{α} \PY{n+nb+bp}{≫} \PY{n}{limit.pre} \PY{n}{G} \PY{n}{E} \PY{n+nb+bp}{=} \PY{n}{limit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{≫} \PY{n}{lim.map} \PY{o}{(}\PY{n}{whisker\PYZus{}left} \PY{n}{E} \PY{n}{α}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.pre\PYZus{}π}\PY{o}{,} \PY{n}{lim.map\PYZus{}π}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n}{lim.map\PYZus{}π}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.pre\PYZus{}π}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{lemma} \PY{n}{limit.map\PYZus{}pre\PYZsq{}} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{K} \PY{n}{C}\PY{o}{]}
  \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{E₁} \PY{n}{E₂} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{α} \PY{o}{:} \PY{n}{E₁} \PY{n+nb+bp}{⟹} \PY{n}{E₂}\PY{o}{)} \PY{o}{:}
  \PY{n}{limit.pre} \PY{n}{F} \PY{n}{E₂} \PY{n+nb+bp}{=} \PY{n}{limit.pre} \PY{n}{F} \PY{n}{E₁} \PY{n+nb+bp}{≫} \PY{n}{lim.map} \PY{o}{(}\PY{n}{whisker\PYZus{}right} \PY{n}{α} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext1}\PY{n+nb+bp}{;} \PY{n}{simp} \PY{o}{[}\PY{o}{(}\PY{n}{category.assoc} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{symm}\PY{o}{]}

\PY{k+kd}{lemma} \PY{n}{limit.id\PYZus{}pre} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{:}
\PY{n}{limit.pre} \PY{n}{F} \PY{o}{(}\PY{n}{functor.id} \PY{n}{\PYZus{}}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{lim.map} \PY{o}{(}\PY{n}{functor.left\PYZus{}unitor} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{inv} \PY{o}{:=} \PY{k+kd}{by} \PY{n}{tidy}

\PY{k+kd}{lemma} \PY{n}{limit.map\PYZus{}post} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}limits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{D}\PY{o}{]} \PY{o}{(}\PY{n}{H} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)} \PY{o}{:}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{v}\PY{c+cm}{s}
\PY{c+cm}{ }\PY{c+cm}{ }\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
  \PY{n}{H.map} \PY{o}{(}\PY{n}{lim.map} \PY{n}{α}\PY{o}{)} \PY{n+nb+bp}{≫} \PY{n}{limit.post} \PY{n}{G} \PY{n}{H} \PY{n+nb+bp}{=} \PY{n}{limit.post} \PY{n}{F} \PY{n}{H} \PY{n+nb+bp}{≫} \PY{n}{lim.map} \PY{o}{(}\PY{n}{whisker\PYZus{}right} \PY{n}{α} \PY{n}{H}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{begin}
  \PY{n}{ext}\PY{o}{,}
  \PY{n}{rw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{H.map\PYZus{}comp}\PY{o}{,} \PY{n}{lim.map\PYZus{}π}\PY{o}{,} \PY{n}{H.map\PYZus{}comp}\PY{o}{]}\PY{o}{,}
  \PY{n}{rw} \PY{o}{[}\PY{n}{assoc}\PY{o}{,} \PY{n}{lim.map\PYZus{}π}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{limit.post\PYZus{}π}\PY{o}{]}\PY{o}{,}
  \PY{n}{refl}
\PY{k+kd}{end}

\PY{k+kd}{def} \PY{n}{lim\PYZus{}yoneda} \PY{o}{:} \PY{n}{lim} \PY{n+nb+bp}{⋙} \PY{n}{yoneda} \PY{n+nb+bp}{≅} \PY{n}{category\PYZus{}theory.cones} \PY{n}{J} \PY{n}{C} \PY{o}{:=}
\PY{n}{nat\PYZus{}iso.of\PYZus{}components} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{F}\PY{o}{,} \PY{n}{nat\PYZus{}iso.of\PYZus{}components} \PY{o}{(}\PY{n}{limit.hom\PYZus{}iso} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{k+kd}{by} \PY{n}{tidy}\PY{o}{)}\PY{o}{)} \PY{o}{(}\PY{k+kd}{by} \PY{n}{tidy}\PY{o}{)}

\PY{k+kd}{end} \PY{n}{lim\PYZus{}functor}

\PY{k+kd}{end} \PY{n}{limit}


\PY{k+kn}{section} \PY{n}{colimit}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{\PYZus{}}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{p}\PY{l+s+sd}{r}\PY{l+s+sd}{e}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{p}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{u}\PY{l+s+sd}{l}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{o}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{t}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{d}\PY{l+s+sd}{i}\PY{l+s+sd}{a}\PY{l+s+sd}{g}\PY{l+s+sd}{r}\PY{l+s+sd}{a}\PY{l+s+sd}{m}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{class} \PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{:=}
\PY{o}{(}\PY{n}{cocone} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)}
\PY{o}{(}\PY{n}{is\PYZus{}colimit} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{n}{cocone}\PY{o}{)}

\PY{k+kd}{variables} \PY{o}{(}\PY{n}{J} \PY{n}{C}\PY{o}{)}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{J}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{h}\PY{l+s+sd}{o}\PY{l+s+sd}{s}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{ }\PY{l+s+sd}{p}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{t}\PY{l+s+sd}{i}\PY{l+s+sd}{c}\PY{l+s+sd}{u}\PY{l+s+sd}{l}\PY{l+s+sd}{a}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}
\PY{l+s+sd}{ }\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{y}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{ }\PY{l+s+sd}{:}\PY{l+s+sd}{ }\PY{l+s+sd}{J}\PY{l+s+sd}{ }\PY{l+s+sd}{⥤}\PY{l+s+sd}{ }\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{@[class]} \PY{k+kd}{def} \PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape} \PY{o}{:=} \PY{n+nb+bp}{Π} \PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{,} \PY{n}{has\PYZus{}colimit} \PY{n}{F}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{(}\PY{l+s+sd}{s}\PY{l+s+sd}{m}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{l}\PY{l+s+sd}{)}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{e}\PY{l+s+sd}{v}\PY{l+s+sd}{e}\PY{l+s+sd}{r}\PY{l+s+sd}{y}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{@[class]} \PY{k+kd}{def} \PY{n}{has\PYZus{}colimits} \PY{o}{:=}
\PY{n+nb+bp}{Π} \PY{o}{\PYZob{}}\PY{n}{J} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n+nb+bp}{𝒥} \PY{o}{:} \PY{n}{small\PYZus{}category} \PY{n}{J}\PY{o}{\PYZcb{}}\PY{o}{,} \PY{k+kd}{by} \PY{n}{exactI} \PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{J} \PY{n}{C}\PY{o}{\PYZcb{}}

\PY{k+kd}{instance} \PY{n}{has\PYZus{}colimit\PYZus{}of\PYZus{}has\PYZus{}colimits\PYZus{}of\PYZus{}shape}
  \PY{o}{\PYZob{}}\PY{n}{J} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{J}\PY{o}{]} \PY{o}{[}\PY{n}{H} \PY{o}{:} \PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C}\PY{o}{]} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{:} \PY{n}{has\PYZus{}colimit} \PY{n}{F} \PY{o}{:=}
\PY{n}{H} \PY{n}{F}

\PY{k+kd}{instance} \PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape\PYZus{}of\PYZus{}has\PYZus{}colimits}
  \PY{o}{\PYZob{}}\PY{n}{J} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{J}\PY{o}{]} \PY{o}{[}\PY{n}{H} \PY{o}{:} \PY{n}{has\PYZus{}colimits.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{C}\PY{o}{]} \PY{o}{:} \PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C} \PY{o}{:=}
\PY{n}{H}

\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{I}\PY{c+cm}{n}\PY{c+cm}{t}\PY{c+cm}{e}\PY{c+cm}{r}\PY{c+cm}{f}\PY{c+cm}{a}\PY{c+cm}{c}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{o}\PY{c+cm}{ }\PY{c+cm}{t}\PY{c+cm}{h}\PY{c+cm}{e}\PY{c+cm}{ }\PY{c+cm}{`}\PY{c+cm}{h}\PY{c+cm}{a}\PY{c+cm}{s}\PY{c+cm}{\PYZus{}}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{`}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{l}\PY{c+cm}{a}\PY{c+cm}{s}\PY{c+cm}{s}\PY{c+cm}{.}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}

\PY{k+kd}{def} \PY{n}{colimit.cocone} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{:} \PY{n}{cocone} \PY{n}{F} \PY{o}{:=} \PY{n}{has\PYZus{}colimit.cocone} \PY{n}{F}

\PY{k+kd}{def} \PY{n}{colimit} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{:=} \PY{o}{(}\PY{n}{colimit.cocone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{X}

\PY{k+kd}{def} \PY{n}{colimit.ι} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:} \PY{n}{F.obj} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{colimit} \PY{n}{F} \PY{o}{:=}
\PY{o}{(}\PY{n}{colimit.cocone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{ι.app} \PY{n}{j}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.cocone\PYZus{}ι} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{colimit.cocone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{ι.app} \PY{n}{j} \PY{n+nb+bp}{=} \PY{n}{colimit.ι} \PY{n}{\PYZus{}} \PY{n}{j} \PY{o}{:=} \PY{n}{rfl}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.w} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{j} \PY{n}{j\PYZsq{}} \PY{o}{:} \PY{n}{J}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{j\PYZsq{}}\PY{o}{)} \PY{o}{:}
  \PY{n}{F.map} \PY{n}{f} \PY{n+nb+bp}{≫} \PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j\PYZsq{}} \PY{n+nb+bp}{=} \PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j} \PY{o}{:=} \PY{o}{(}\PY{n}{colimit.cocone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{w} \PY{n}{f}

\PY{k+kd}{def} \PY{n}{colimit.is\PYZus{}colimit} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{:} \PY{n}{is\PYZus{}colimit} \PY{o}{(}\PY{n}{colimit.cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{n}{has\PYZus{}colimit.is\PYZus{}colimit.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{F}

\PY{k+kd}{def} \PY{n}{colimit.desc} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:} \PY{n}{colimit} \PY{n}{F} \PY{n+nb+bp}{⟶} \PY{n}{c.X} \PY{o}{:=}
\PY{o}{(}\PY{n}{colimit.is\PYZus{}colimit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{desc} \PY{n}{c}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.is\PYZus{}colimit\PYZus{}desc} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{colimit.is\PYZus{}colimit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{desc} \PY{n}{c} \PY{n+nb+bp}{=} \PY{n}{colimit.desc} \PY{n}{F} \PY{n}{c} \PY{o}{:=} \PY{n}{rfl}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.ι\PYZus{}desc} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{colimit.desc} \PY{n}{F} \PY{n}{c} \PY{n+nb+bp}{=} \PY{n}{c.ι.app} \PY{n}{j} \PY{o}{:=}
\PY{n}{is\PYZus{}colimit.fac} \PY{n}{\PYZus{}} \PY{n}{c} \PY{n}{j}

\PY{k+kd}{def} \PY{n}{colimit.cocone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{n}{cocone\PYZus{}morphism} \PY{o}{(}\PY{n}{colimit.cocone} \PY{n}{F}\PY{o}{)} \PY{n}{c} \PY{o}{:=}
\PY{o}{(}\PY{n}{colimit.is\PYZus{}colimit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{desc\PYZus{}cocone\PYZus{}morphism} \PY{n}{c}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.cocone\PYZus{}morphism\PYZus{}hom} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{colimit.cocone\PYZus{}morphism} \PY{n}{c}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n+nb+bp}{=} \PY{n}{colimit.desc} \PY{n}{F} \PY{n}{c} \PY{o}{:=} \PY{n}{rfl}
\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.ι\PYZus{}cocone\PYZus{}morphism} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{o}{(}\PY{n}{colimit.cocone\PYZus{}morphism} \PY{n}{c}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n+nb+bp}{=} \PY{n}{c.ι.app} \PY{n}{j} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{erw} \PY{n}{is\PYZus{}colimit.fac}

\PY{k+kd}{@[extensionality]} \PY{k+kd}{lemma} \PY{n}{colimit.hom\PYZus{}ext} \PY{o}{\PYZob{}}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{X} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{f} \PY{n}{f\PYZsq{}} \PY{o}{:} \PY{n}{colimit} \PY{n}{F} \PY{n+nb+bp}{⟶} \PY{n}{X}\PY{o}{\PYZcb{}}
  \PY{o}{(}\PY{n}{w} \PY{o}{:} \PY{n+nb+bp}{∀} \PY{n}{j}\PY{o}{,} \PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{f\PYZsq{}}\PY{o}{)} \PY{o}{:} \PY{n}{f} \PY{n+nb+bp}{=} \PY{n}{f\PYZsq{}} \PY{o}{:=}
\PY{o}{(}\PY{n}{colimit.is\PYZus{}colimit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}ext} \PY{n}{w}

\PY{k+kd}{def} \PY{n}{colimit.hom\PYZus{}iso} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:} \PY{o}{(}\PY{n}{colimit} \PY{n}{F} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{(}\PY{n}{F.cocones.obj} \PY{n}{W}\PY{o}{)} \PY{o}{:=}
\PY{o}{(}\PY{n}{colimit.is\PYZus{}colimit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}iso} \PY{n}{W}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.hom\PYZus{}iso\PYZus{}hom} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{colimit} \PY{n}{F} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{)}\PY{o}{:}
  \PY{o}{(}\PY{n}{colimit.hom\PYZus{}iso} \PY{n}{F} \PY{n}{W}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{n}{f} \PY{n+nb+bp}{=} \PY{o}{(}\PY{n}{colimit.cocone} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{ι} \PY{n+nb+bp}{≫} \PY{o}{(}\PY{n}{const} \PY{n}{J}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{map} \PY{n}{f} \PY{o}{:=}
\PY{o}{(}\PY{n}{colimit.is\PYZus{}colimit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}iso\PYZus{}hom} \PY{n}{f}

\PY{k+kd}{def} \PY{n}{colimit.hom\PYZus{}iso\PYZsq{}} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{W} \PY{o}{:} \PY{n}{C}\PY{o}{)} \PY{o}{:}
  \PY{o}{(}\PY{n}{colimit} \PY{n}{F} \PY{n+nb+bp}{⟶} \PY{n}{W}\PY{o}{)} \PY{n+nb+bp}{≅} \PY{o}{\PYZob{}} \PY{n}{p} \PY{o}{:} \PY{n+nb+bp}{Π} \PY{n}{j}\PY{o}{,} \PY{n}{F.obj} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{W} \PY{n+nb+bp}{/}\PY{n+nb+bp}{/} \PY{n+nb+bp}{∀} \PY{o}{\PYZob{}}\PY{n}{j} \PY{n}{j\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{j} \PY{n+nb+bp}{⟶} \PY{n}{j\PYZsq{}}\PY{o}{)}\PY{o}{,} \PY{n}{F.map} \PY{n}{f} \PY{n+nb+bp}{≫} \PY{n}{p} \PY{n}{j\PYZsq{}} \PY{n+nb+bp}{=} \PY{n}{p} \PY{n}{j} \PY{o}{\PYZcb{}} \PY{o}{:=}
\PY{o}{(}\PY{n}{colimit.is\PYZus{}colimit} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom\PYZus{}iso\PYZsq{}} \PY{n}{W}

\PY{k+kd}{lemma} \PY{n}{colimit.desc\PYZus{}extend} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{X} \PY{o}{:} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{f} \PY{o}{:} \PY{n}{c.X} \PY{n+nb+bp}{⟶} \PY{n}{X}\PY{o}{)} \PY{o}{:}
  \PY{n}{colimit.desc} \PY{n}{F} \PY{o}{(}\PY{n}{c.extend} \PY{n}{f}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{colimit.desc} \PY{n}{F} \PY{n}{c} \PY{n+nb+bp}{≫} \PY{n}{f} \PY{o}{:=}
\PY{k+kd}{begin}
  \PY{n}{ext1}\PY{o}{,} \PY{n}{simp} \PY{o}{[}\PY{n}{category.assoc\PYZus{}symm}\PY{o}{]}\PY{o}{,} \PY{n}{refl}
\PY{k+kd}{end}

\PY{k+kn}{section} \PY{n}{pre}
\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]}
\PY{k+kd}{variables} \PY{o}{(}\PY{n}{F}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{E} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}\PY{o}{]}

\PY{k+kd}{def} \PY{n}{colimit.pre} \PY{o}{:} \PY{n}{colimit} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{⟶} \PY{n}{colimit} \PY{n}{F} \PY{o}{:=}
\PY{n}{colimit.desc} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}
  \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{colimit} \PY{n}{F}\PY{o}{,}
    \PY{n}{ι} \PY{o}{:=} \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{k}\PY{o}{,} \PY{n}{colimit.ι} \PY{n}{F} \PY{o}{(}\PY{n}{E.obj} \PY{n}{k}\PY{o}{)} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.ι\PYZus{}pre} \PY{o}{(}\PY{n}{k} \PY{o}{:} \PY{n}{K}\PY{o}{)} \PY{o}{:} \PY{n}{colimit.ι} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n}{k} \PY{n+nb+bp}{≫} \PY{n}{colimit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{=} \PY{n}{colimit.ι} \PY{n}{F} \PY{o}{(}\PY{n}{E.obj} \PY{n}{k}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{erw} \PY{n}{is\PYZus{}colimit.fac}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.pre\PYZus{}desc} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{n}{colimit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{≫} \PY{n}{colimit.desc} \PY{n}{F} \PY{n}{c} \PY{n+nb+bp}{=} \PY{n}{colimit.desc} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{o}{(}\PY{n}{c.whisker} \PY{n}{E}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}pre}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{simp}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{L} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{L}\PY{o}{]}
\PY{k+kd}{variables} \PY{o}{(}\PY{n}{D} \PY{o}{:} \PY{n}{L} \PY{n+nb+bp}{⥤} \PY{n}{K}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{D} \PY{n+nb+bp}{⋙} \PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}\PY{o}{]}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.pre\PYZus{}pre} \PY{o}{:} \PY{n}{colimit.pre} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n}{D} \PY{n+nb+bp}{≫} \PY{n}{colimit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{=} \PY{n}{colimit.pre} \PY{n}{F} \PY{o}{(}\PY{n}{D} \PY{n+nb+bp}{⋙} \PY{n}{E}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{begin}
  \PY{n}{ext} \PY{n}{j}\PY{o}{,}
  \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}pre}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}pre}\PY{o}{]}\PY{o}{,}
  \PY{n}{letI} \PY{o}{:} \PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{o}{(}\PY{n}{D} \PY{n+nb+bp}{⋙} \PY{n}{E}\PY{o}{)} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{o}{:=} \PY{k}{show} \PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{D} \PY{n+nb+bp}{⋙} \PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}\PY{o}{,} \PY{k+kd}{by} \PY{n}{apply\PYZus{}instance}\PY{o}{,}
  \PY{n}{exact} \PY{o}{(}\PY{n}{colimit.ι\PYZus{}pre} \PY{n}{F} \PY{o}{(}\PY{n}{D} \PY{n+nb+bp}{⋙} \PY{n}{E}\PY{o}{)} \PY{n}{j}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{symm}
\PY{k+kd}{end}

\PY{k+kd}{end} \PY{n}{pre}

\PY{k+kn}{section} \PY{n}{post}
\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n+nb+bp}{𝒟} \PY{o}{:} \PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]}
\PY{k+kn}{include} \PY{n+nb+bp}{𝒟}

\PY{k+kd}{variables} \PY{o}{(}\PY{n}{F}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{(}\PY{n}{G} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}\PY{o}{]}

\PY{k+kd}{def} \PY{n}{colimit.post} \PY{o}{:} \PY{n}{colimit} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n+nb+bp}{⟶} \PY{n}{G.obj} \PY{o}{(}\PY{n}{colimit} \PY{n}{F}\PY{o}{)} \PY{o}{:=}
\PY{n}{colimit.desc} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}
\PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{G.obj} \PY{o}{(}\PY{n}{colimit} \PY{n}{F}\PY{o}{)}\PY{o}{,}
  \PY{n}{ι} \PY{o}{:=}
  \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{G.map} \PY{o}{(}\PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j}\PY{o}{)}\PY{o}{,}
    \PY{n}{naturality\PYZsq{}} \PY{o}{:=}
      \PY{k+kd}{by} \PY{n}{intros} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{limits.cocone.w}\PY{o}{,} \PY{n}{comp\PYZus{}id}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.ι\PYZus{}post} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:} \PY{n}{colimit.ι} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{colimit.post} \PY{n}{F} \PY{n}{G}  \PY{n+nb+bp}{=} \PY{n}{G.map} \PY{o}{(}\PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{erw} \PY{n}{is\PYZus{}colimit.fac}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.post\PYZus{}desc} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{F}\PY{o}{)} \PY{o}{:}
  \PY{n}{colimit.post} \PY{n}{F} \PY{n}{G} \PY{n+nb+bp}{≫} \PY{n}{G.map} \PY{o}{(}\PY{n}{colimit.desc} \PY{n}{F} \PY{n}{c}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{colimit.desc} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{o}{(}\PY{n}{G.map\PYZus{}cocone} \PY{n}{c}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}post}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}desc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}desc}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.post\PYZus{}post}
  \PY{o}{\PYZob{}}\PY{n}{E} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{E}\PY{o}{]} \PY{o}{(}\PY{n}{H} \PY{o}{:} \PY{n}{D} \PY{n+nb+bp}{⥤} \PY{n}{E}\PY{o}{)} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n+nb+bp}{⋙} \PY{n}{H}\PY{o}{)}\PY{o}{]} \PY{o}{:}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{e}\PY{c+cm}{q}\PY{c+cm}{u}\PY{c+cm}{a}\PY{c+cm}{l}\PY{c+cm}{s}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
  \PY{n}{colimit.post} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n}{H} \PY{n+nb+bp}{≫} \PY{n}{H.map} \PY{o}{(}\PY{n}{colimit.post} \PY{n}{F} \PY{n}{G}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{colimit.post} \PY{n}{F} \PY{o}{(}\PY{n}{G} \PY{n+nb+bp}{⋙} \PY{n}{H}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{begin}
  \PY{n}{ext}\PY{o}{,}
  \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}post}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{H.map\PYZus{}comp}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}post}\PY{o}{]}\PY{o}{,}
  \PY{n}{exact} \PY{o}{(}\PY{n}{colimit.ι\PYZus{}post} \PY{n}{F} \PY{o}{(}\PY{n}{G} \PY{n+nb+bp}{⋙} \PY{n}{H}\PY{o}{)} \PY{n}{j}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{symm}
\PY{k+kd}{end}

\PY{k+kd}{end} \PY{n}{post}

\PY{k+kd}{lemma} \PY{n}{colimit.pre\PYZus{}post} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]}
  \PY{o}{(}\PY{n}{E} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{)} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{(}\PY{n}{G} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)}
  \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{n}{F}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}\PY{o}{]} \PY{o}{:}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{E}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{(}\PY{c+cm}{E}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{v}\PY{c+cm}{s}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{E}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{o}\PY{c+cm}{r}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
  \PY{n}{colimit.post} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n}{G} \PY{n+nb+bp}{≫} \PY{n}{G.map} \PY{o}{(}\PY{n}{colimit.pre} \PY{n}{F} \PY{n}{E}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{colimit.pre} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n}{E} \PY{n+nb+bp}{≫} \PY{n}{colimit.post} \PY{n}{F} \PY{n}{G} \PY{o}{:=}
\PY{k+kd}{begin}
  \PY{n}{ext}\PY{o}{,}
  \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}post}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{G.map\PYZus{}comp}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}pre}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{]}\PY{o}{,}
  \PY{n}{letI} \PY{o}{:} \PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{o}{:=} \PY{k}{show} \PY{n}{has\PYZus{}colimit} \PY{o}{(}\PY{o}{(}\PY{n}{E} \PY{n+nb+bp}{⋙} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)}\PY{o}{,} \PY{k+kd}{by} \PY{n}{apply\PYZus{}instance}\PY{o}{,}
  \PY{n}{erw} \PY{o}{[}\PY{n}{colimit.ι\PYZus{}pre} \PY{o}{(}\PY{n}{F} \PY{n+nb+bp}{⋙} \PY{n}{G}\PY{o}{)} \PY{n}{E} \PY{n}{j}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}post}\PY{o}{]}
\PY{k+kd}{end}

\PY{k+kn}{section} \PY{n}{colim\PYZus{}functor}

\PY{k+kd}{variables} \PY{o}{[}\PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{C}\PY{o}{]}

\PY{l+s+sd}{/\PYZhy{}\PYZhy{}}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{ }\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{f}\PY{l+s+sd}{u}\PY{l+s+sd}{n}\PY{l+s+sd}{c}\PY{l+s+sd}{t}\PY{l+s+sd}{o}\PY{l+s+sd}{r}\PY{l+s+sd}{i}\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{i}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{F}\PY{l+s+sd}{`}\PY{l+s+sd}{,}\PY{l+s+sd}{ }\PY{l+s+sd}{w}\PY{l+s+sd}{h}\PY{l+s+sd}{e}\PY{l+s+sd}{n}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{C}\PY{l+s+sd}{`}\PY{l+s+sd}{ }\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{a}\PY{l+s+sd}{l}\PY{l+s+sd}{l}\PY{l+s+sd}{ }\PY{l+s+sd}{c}\PY{l+s+sd}{o}\PY{l+s+sd}{l}\PY{l+s+sd}{i}\PY{l+s+sd}{m}\PY{l+s+sd}{i}\PY{l+s+sd}{t}\PY{l+s+sd}{s}\PY{l+s+sd}{ }\PY{l+s+sd}{o}\PY{l+s+sd}{f}\PY{l+s+sd}{ }\PY{l+s+sd}{s}\PY{l+s+sd}{h}\PY{l+s+sd}{a}\PY{l+s+sd}{p}\PY{l+s+sd}{e}\PY{l+s+sd}{ }\PY{l+s+sd}{`}\PY{l+s+sd}{J}\PY{l+s+sd}{`}\PY{l+s+sd}{.}\PY{l+s+sd}{ }\PY{l+s+sd}{\PYZhy{}/}
\PY{k+kd}{def} \PY{n}{colim} \PY{o}{:} \PY{o}{(}\PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{n+nb+bp}{⥤} \PY{n}{C} \PY{o}{:=}
\PY{o}{\PYZob{}} \PY{n}{obj} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{F}\PY{o}{,} \PY{n}{colimit} \PY{n}{F}\PY{o}{,}
  \PY{n}{map} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{F} \PY{n}{G} \PY{n}{α}\PY{o}{,} \PY{n}{colimit.desc} \PY{n}{F}
    \PY{o}{\PYZob{}} \PY{n}{X} \PY{o}{:=} \PY{n}{colimit} \PY{n}{G}\PY{o}{,}
      \PY{n}{ι} \PY{o}{:=}
      \PY{o}{\PYZob{}} \PY{n}{app} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j}\PY{o}{,} \PY{n}{α.app} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{colimit.ι} \PY{n}{G} \PY{n}{j}\PY{o}{,}
        \PY{n}{naturality\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{j} \PY{n}{j\PYZsq{}} \PY{n}{f}\PY{o}{,}
          \PY{k+kd}{by} \PY{n}{erw} \PY{o}{[}\PY{n}{comp\PYZus{}id}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{α.naturality}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.w}\PY{o}{]} \PY{o}{\PYZcb{}} \PY{o}{\PYZcb{}}\PY{o}{,}
  \PY{n}{map\PYZus{}comp\PYZsq{}} \PY{o}{:=} \PY{n+nb+bp}{λ} \PY{n}{F} \PY{n}{G} \PY{n}{H} \PY{n}{α} \PY{n}{β}\PY{o}{,}
    \PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{erw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{is\PYZus{}colimit.fac}\PY{o}{,} \PY{n}{is\PYZus{}colimit.fac}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n}{is\PYZus{}colimit.fac}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl} \PY{o}{\PYZcb{}}

\PY{k+kd}{variables} \PY{o}{\PYZob{}}\PY{n}{F}\PY{o}{\PYZcb{}} \PY{o}{\PYZob{}}\PY{n}{G} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{α} \PY{o}{:} \PY{n}{F} \PY{n+nb+bp}{⟹} \PY{n}{G}\PY{o}{)}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colim.ι\PYZus{}map} \PY{o}{(}\PY{n}{j} \PY{o}{:} \PY{n}{J}\PY{o}{)} \PY{o}{:} \PY{n}{colimit.ι} \PY{n}{F} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{colim.map} \PY{n}{α} \PY{n+nb+bp}{=} \PY{n}{α.app} \PY{n}{j} \PY{n+nb+bp}{≫} \PY{n}{colimit.ι} \PY{n}{G} \PY{n}{j} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{apply} \PY{n}{is\PYZus{}colimit.fac}

\PY{k+kd}{@[simp]} \PY{k+kd}{lemma} \PY{n}{colimit.map\PYZus{}desc} \PY{o}{(}\PY{n}{c} \PY{o}{:} \PY{n}{cocone} \PY{n}{G}\PY{o}{)} \PY{o}{:}
  \PY{n}{colim.map} \PY{n}{α} \PY{n+nb+bp}{≫} \PY{n}{colimit.desc} \PY{n}{G} \PY{n}{c} \PY{n+nb+bp}{=} \PY{n}{colimit.desc} \PY{n}{F} \PY{o}{(}\PY{n}{c.precompose} \PY{n}{α}\PY{o}{)} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colim.ι\PYZus{}map}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}desc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}desc}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{lemma} \PY{n}{colimit.pre\PYZus{}map} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape} \PY{n}{K} \PY{n}{C}\PY{o}{]} \PY{o}{(}\PY{n}{E} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{)} \PY{o}{:}
  \PY{n}{colimit.pre} \PY{n}{F} \PY{n}{E} \PY{n+nb+bp}{≫} \PY{n}{colim.map} \PY{n}{α} \PY{n+nb+bp}{=} \PY{n}{colim.map} \PY{o}{(}\PY{n}{whisker\PYZus{}left} \PY{n}{E} \PY{n}{α}\PY{o}{)} \PY{n+nb+bp}{≫} \PY{n}{colimit.pre} \PY{n}{G} \PY{n}{E} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext}\PY{n+nb+bp}{;} \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}pre}\PY{o}{,} \PY{n}{colim.ι\PYZus{}map}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colim.ι\PYZus{}map}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}pre}\PY{o}{]}\PY{n+nb+bp}{;} \PY{n}{refl}

\PY{k+kd}{lemma} \PY{n}{colimit.pre\PYZus{}map\PYZsq{}} \PY{o}{\PYZob{}}\PY{n}{K} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{v}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{small\PYZus{}category} \PY{n}{K}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{K} \PY{n}{C}\PY{o}{]}
  \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{\PYZob{}}\PY{n}{E₁} \PY{n}{E₂} \PY{o}{:} \PY{n}{K} \PY{n+nb+bp}{⥤} \PY{n}{J}\PY{o}{\PYZcb{}} \PY{o}{(}\PY{n}{α} \PY{o}{:} \PY{n}{E₁} \PY{n+nb+bp}{⟹} \PY{n}{E₂}\PY{o}{)} \PY{o}{:}
  \PY{n}{colimit.pre} \PY{n}{F} \PY{n}{E₁} \PY{n+nb+bp}{=} \PY{n}{colim.map} \PY{o}{(}\PY{n}{whisker\PYZus{}right} \PY{n}{α} \PY{n}{F}\PY{o}{)} \PY{n+nb+bp}{≫} \PY{n}{colimit.pre} \PY{n}{F} \PY{n}{E₂} \PY{o}{:=}
\PY{k+kd}{by} \PY{n}{ext1}\PY{n+nb+bp}{;} \PY{n}{simp} \PY{o}{[}\PY{o}{(}\PY{n}{category.assoc} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}} \PY{n}{\PYZus{}}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{symm}\PY{o}{]}

\PY{k+kd}{lemma} \PY{n}{colimit.pre\PYZus{}id} \PY{o}{(}\PY{n}{F} \PY{o}{:} \PY{n}{J} \PY{n+nb+bp}{⥤} \PY{n}{C}\PY{o}{)} \PY{o}{:}
\PY{n}{colimit.pre} \PY{n}{F} \PY{o}{(}\PY{n}{functor.id} \PY{n}{\PYZus{}}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{colim.map} \PY{o}{(}\PY{n}{functor.left\PYZus{}unitor} \PY{n}{F}\PY{o}{)}\PY{n+nb+bp}{.}\PY{n}{hom} \PY{o}{:=} \PY{k+kd}{by} \PY{n}{tidy}

\PY{k+kd}{lemma} \PY{n}{colimit.map\PYZus{}post} \PY{o}{\PYZob{}}\PY{n}{D} \PY{o}{:} \PY{k+kt}{Type} \PY{n}{u\PYZsq{}}\PY{o}{\PYZcb{}} \PY{o}{[}\PY{n}{category.}\PY{o}{\PYZob{}}\PY{n}{v}\PY{o}{\PYZcb{}} \PY{n}{D}\PY{o}{]} \PY{o}{[}\PY{n}{has\PYZus{}colimits\PYZus{}of\PYZus{}shape} \PY{n}{J} \PY{n}{D}\PY{o}{]} \PY{o}{(}\PY{n}{H} \PY{o}{:} \PY{n}{C} \PY{n+nb+bp}{⥤} \PY{n}{D}\PY{o}{)} \PY{o}{:}
\PY{c}{/\PYZhy{}}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{G}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{v}\PY{c+cm}{s}
\PY{c+cm}{ }\PY{c+cm}{ }\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{F}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{F}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{⟶}\PY{c+cm}{ }\PY{c+cm}{c}\PY{c+cm}{o}\PY{c+cm}{l}\PY{c+cm}{i}\PY{c+cm}{m}\PY{c+cm}{i}\PY{c+cm}{t}\PY{c+cm}{ }\PY{c+cm}{(}\PY{c+cm}{G}\PY{c+cm}{ }\PY{c+cm}{⋙}\PY{c+cm}{ }\PY{c+cm}{H}\PY{c+cm}{)}\PY{c+cm}{ }\PY{c+cm}{\PYZhy{}/}
  \PY{n}{colimit.post} \PY{n}{F} \PY{n}{H} \PY{n+nb+bp}{≫} \PY{n}{H.map} \PY{o}{(}\PY{n}{colim.map} \PY{n}{α}\PY{o}{)} \PY{n+nb+bp}{=} \PY{n}{colim.map} \PY{o}{(}\PY{n}{whisker\PYZus{}right} \PY{n}{α} \PY{n}{H}\PY{o}{)} \PY{n+nb+bp}{≫} \PY{n}{colimit.post} \PY{n}{G} \PY{n}{H}\PY{o}{:=}
\PY{k+kd}{begin}
  \PY{n}{ext}\PY{o}{,}
  \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}post}\PY{o}{,} \PY{n+nb+bp}{←}\PY{n}{H.map\PYZus{}comp}\PY{o}{,} \PY{n}{colim.ι\PYZus{}map}\PY{o}{,} \PY{n}{H.map\PYZus{}comp}\PY{o}{]}\PY{o}{,}
  \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←}\PY{n}{assoc}\PY{o}{,} \PY{n}{colim.ι\PYZus{}map}\PY{o}{,} \PY{n}{assoc}\PY{o}{,} \PY{n}{colimit.ι\PYZus{}post}\PY{o}{]}\PY{o}{,}
  \PY{n}{refl}
\PY{k+kd}{end}

\PY{k+kd}{def} \PY{n}{colim\PYZus{}coyoneda} \PY{o}{:} \PY{n}{colim.op} \PY{n+nb+bp}{⋙} \PY{n}{coyoneda} \PY{n+nb+bp}{≅} \PY{n}{category\PYZus{}theory.cocones} \PY{n}{J} \PY{n}{C} \PY{o}{:=}
\PY{n}{nat\PYZus{}iso.of\PYZus{}components} \PY{o}{(}\PY{n+nb+bp}{λ} \PY{n}{F}\PY{o}{,} \PY{n}{nat\PYZus{}iso.of\PYZus{}components} \PY{o}{(}\PY{n}{colimit.hom\PYZus{}iso} \PY{n}{F}\PY{o}{)}
  \PY{o}{(}\PY{k+kd}{by} \PY{o}{\PYZob{}}\PY{n}{tidy}\PY{o}{,} \PY{n}{dsimp} \PY{o}{[}\PY{n}{functor.cocones}\PY{o}{]}\PY{o}{,} \PY{n}{rw} \PY{n}{category.assoc} \PY{o}{\PYZcb{}}\PY{o}{)}\PY{o}{)}
  \PY{o}{(}\PY{k+kd}{by} \PY{o}{\PYZob{}}\PY{n}{tidy}\PY{o}{,} \PY{n}{rw} \PY{o}{[}\PY{n+nb+bp}{←} \PY{n}{category.assoc}\PY{o}{,}\PY{n+nb+bp}{←} \PY{n}{category.assoc}\PY{o}{]}\PY{o}{,} \PY{n}{tidy} \PY{o}{\PYZcb{}}\PY{o}{)}

\PY{k+kd}{end} \PY{n}{colim\PYZus{}functor}

\PY{k+kd}{end} \PY{n}{colimit}

\PY{k+kd}{end} \PY{n}{category\PYZus{}theory.limits}
\end{Verbatim}

\end{frame}

\end{document}