I can't belive I made it

J'ai pris le bus S2. Oxford est magnifique.


No country for old man

Tomorrow morning, I will be heading to Oxford to attend a seminar on "2 dimensional Kripke Semantics". I will be taking a bus which stops in every village of Cotswold, which is a blessing in disguise. I am a wannabe category theorist. I have some clues about Krikpe Semantics but the main goal is to see Alex Kavvos in person and ask if he would be willing to supervise me at somepoint. I have met him before in his office. I must have came across as a crackpot. I am certainly older but am I still a crackpot? If there be an opportunity, I am going to say hi and bring up linear logic. Stoics say the goal of life is not to keep hold of sanity. On the posetive side, no body cares about me and so I shall overcome the imposter syndrom. No need to mention, today was cold. I need change. I need fire. I need noon. "Oh Shamash, by your light you scan the totality of lands as if they were cuniforms."


General Nonsense 1- Yoneda Lemmma

This i A fibration is a functor $F:\mathcal{E}\rightarrow \mathcal{B}$ such that $\forall u: B' \rightarrow FE$ in $\mathcal{B}$ there is a unique $t: E'\rightarrow E$ such that $Ft = u$ and moreover $Fs=uu' \implies s= tt'$ with $Ft' = s'$. A morphism in $t \in \mathcal{E}$ is in the fiber over $B \in \mathcal{B}$ of a fibration $F:\mathcal{E}\rightarrow\mathcal{B}$ denoted by $t \in F^{-1}\left(B\right)$ if $Ft = id_B$. A fibration is discrete if the fiber over any object is a set. We shall denote $\mbox{DiscFib}\left(\mathcal{B}\right)$ for the category of discrete fibrations over $B$. Define a presheaf to be a contravariant set valued functor over a locally small category and denote $\mathcal{B}^{\wedge}$ for the category of presheaves and their natural transformations. In this post we recollect some generalities conerning the topos of presheaves, begining by showing that $\mbox{DiscFib}\left(\mathcal{B}\right) \simeq \mathcal{B}^{\wedge}$. There is a discrete fibration $\rho_X$ associated to any presheaf $X \in \mathcal{B}^{\wedge}$ given by a forgetful functor $\left(x,B\right)\mapsto B: \mathcal{B}_X \rightarrow \mathcal{B}$, where $\mathcal{B}_X$ is the category of elements of $X: \mathcal{B}^{o}\rightarrow Set$ with $u \in \mathcal{B}_X\left(\left(x',B'\right),\left(x,B\right)\right)$ if $u \in \mathcal{B}\left(B',B\right)$ and $Xux=x'$. A section $x \in XB$ of a presheaf $X$ gives a presheaf morphism $x:B \rightarrow X$ whose component at $B' \in \mathcal{B}$ is given by $u \mapsto Xux:\mathcal{B}: \mathcal{B}\left(B',B\right)\rightarrow XB'$. Here, $B \in \mathcal{B}^{\wedge}$ is an abuse of notation for a presheaf representable by $B \in \mathcal{B}$, that is -in anticipation of the uses of Yoneda lemma- we write $B$ instead of $\mathcal{B}\left(-,B\right):\mathcal{B}^{o}\rightarrow Set$ and $x:B \rightarrow X$, for the presheaf over $X$ determined by sending the generic element $id_B$ of $B$ to $x \in XB$. Moreover, there is a quasi-equivalance of big categories of the category of presheaves over $X$ denoted $\mathcal{B}^{\wedge}/X$ and the category $\left(\mathcal{B}_X\right)^{\wedge}$ of presheaves over the category of elements of $X$. Recall that the Yoned embedding $\mathscr{Y}:\mathcal{B}\rightarrow \mathcal{B}^{\wedge}$ sends $B\in \mathcal{B}$ to $\mathcal{B}\left(-,B\right)\in \mathcal{B}^{\wedge}$. But, besides the Yoneda embedding $\mathscr{Y}''\left(x,B\right)= \mathcal{B}_X\left(-,\left(x,B\right)\right):\left(\mathcal{B}_{X}\right)^{o}\rightarrow Set$ of the category of elements of $X$ into the category of presheaves over the category of elements of $X$, there is also $\mathscr{Y}':\mathcal{B}_X \rightarrow \mathcal{B}^{\wedge}/X$ where $\left(\phi,Z\right) \in \mathcal{B}^{\wedge}/X$ if $\phi \in \mathcal{B}^{\wedge}\left(Z,X\right)$ and $\mathscr{Y}'\left(x,B\right) = \left(x,B\right)$ where $x:B \rightarrow X$ is determined by $id_B \mapsto x$. Its easy to see $\mathcal{B}^{\wedge}/X \simeq \left(\mathcal{B}_X\right)^{\wedge}$ as any presheaf $F: \left(\mathcal{B}_X\right)^{\wedge}\rightarrow Set$ can be sent to $\pi: \lambda\left(F\right) \rightarrow X$ where $\lambda\left(F\right): \mathcal{B}^{o}\rightarrow Set$ sends $B \in \mathcal{B}$ to the set $\left\{\left(x,s\right)| x \in XB, s \in F\left(x,B\right)\right\}$ and $\pi_B\left(x,s\right):=x$ gives the component at $B \in \mathcal{B}$. On the other hand, any $\alpha: Z \rightarrow X$ gives a presheaf $\gamma\left(\alpha\right) \in \left(\mathcal{B}_X\right)^{\wedge}$ which maps $\left(x,B\right)$ to $\left\{z \in ZB|\alpha z = x\right\}$ and we have: $\gamma \circ \lambda \simeq id_{\left(\mathcal{B}_X\right)^{\wedge}}$ and $\lambda \circ \gamma \simeq id_{\mathcal{B}^{\wedge}/X}$. Seeing that $\rho_X: \mathcal{B}_{X} \rightarrow \mathcal{B}$ defined by $\left(x,B\right) \mapsto B$ associated to any presheaf $X:\mathcal{B}^{o}\rightarrow Set$ is a discrete fibration is the matter of unpacking $X$ being a presheaf. We show in detail how any discrete fibration $F: \mathcal{E}\rightarrow \mathcal{B}$ gives a presheaf, namely the presheaf $B \mapsto F^{-1}\left(B\right):\mathcal{B}\rightarrow Set$. To this end, suppose $r:E \rightarrow E_0$$ \in F^{-1}\left(B\right)$ is in the fiber over $B$ and $u:B' \rightarrow FE$ in the base category $\mathcal{B}$ are given. By definition, there must be $t:E'\rightarrow E$ with $Ft = u$ and moreover $Fs=uu' \implies s=tt'$ with $Ft'=u'$. In particular, letting $s=rt$ we see $Fs = FrFt = id_{B}u = u id_{B'}$ and therefore $rt = tt'$ for some unique $t' \in F^{-1}\left(B'\right)$. For a functor $\alpha:I \rightarrow \mathcal{B}$ we define the ind-limit of $\alpha$ to be the colimit of $\mathscr{Y} \circ \alpha: I \rightarrow \mathcal{B}^{\wedge}$ where $\mathscr{Y}:\mathcal{B}\rightarrow \mathcal{B}^{\wedge}$ is the Yoneda embedding $B \mapsto \mathcal{B}\left(-,B\right)$. The category $\mathcal{B}^{\wedge}$ of presheaves over $B$ has colimits (of small diagrams) as $Set$ has such colimits as we know: Let $\psi: J \rightarrow \left[\mathcal{C},\mathcal{D}\right]$ be a diagram in the functor category $\left[\mathcal{C},\mathcal{D}\right]$ and suppose $\mathcal{D}$ has $J$-shaped colimits. Then the colimit of $\psi$ exists and is given by $C \mapsto \varinjlim \beta_ C: \mathcal{C}\rightarrow \mathcal{D}$ where $\beta_C: J \rightarrow \mathcal{D}$ for $C \in \mathcal{C}$ is given by $j \mapsto \psi \left(j\right)\left(C\right)$. In other word, colimits (and similalry limits) are computed objectwise. So a presheaf $"\varinjlim \alpha ": \mathcal{B}^{o} \rightarrow Set$ called the ind-limit of $\alpha$ must exists when $I$ is small and $$\mathcal{B}^{\wedge}\left("\varinjlim" \alpha, Z\right)\simeq \varprojlim \mathcal{B}^{\wedge}\left(\mathscr{Y}\alpha,Z\right) \simeq I^{\wedge}\left(1, \mathcal{B}^{\wedge}\left(\mathscr{Y}\alpha,Z\right)\right)$$.