Kan extensions

Draft of just one, but key, diagram concerning the pointwise right Kan extension at (one object $\leftcat{ \boxed{1} \;  l\in\calL}$).

$$\leftcat{      \boxed{     \begin{array} {}    &&  \calI & \xrightarrow[\smash{\kern4em}]{\textstyle \boxed{1} \; l}  &  \calL  \\ &&  \rightadj{  \llap{ \boxed{11} \; ! } {\Bigg\uparrow}  }  &  \leftcat{  \llap{ \boxed{11} \; \lambda }   {\Bigg\Downarrow} }   &  \rightadj{  \llap{ \boxed{0} R } {\Bigg\uparrow}   }  &  \kern2em \llap{  \llap{ \rightcat{\boxed{31} \, \alpha} \kern-.2em } \Downarrow \kern1em  }  \leftcat{  \searrow \rlap {S \; \boxed{30} }  }     \\    \leftcat\calI  &  \xrightarrow[  \smash{ \textstyle \leftcat{\boxed{12}} \; \rightcat r \leftcat{[\lambda]} }  ]{  \smash{ \textstyle \text{right lax fiber} }  }  &  \leftcat{     ( l \downarrow {\rightadj R} ) \smash{    \rlap{  \lower2.7ex{   \kern-2.1em \boxed{10}  }  }   }    }  &    \rightcat{   \xrightarrow[ \smash{\textstyle \boxed{11}  \; Q=r}  ]{}   }    &  \rightcat\calR  &  \xrightarrow[  \smash{ \textstyle \boxed{0} \;  G \; (\text{e.g., }\rightadj R) }  ]{\kern8em}  &  \calC       \\   \leftcat\Vert  &&&&  \rightcat\Vert  \\  \leftcat\calI \rlap{ \xrightarrow[ \textstyle \rightcat r ]{\kern24em} }  &&&&  \rightcat\calR    \\ \end{array}     }      }$$

Given the initial data, the span $\Big( \rightadj{  \boxed{0} \; R  : {\leftcat\calL} \leftarrow {} } {\rightcat\calR}  \to \calC :  { G \; \boxed{0} } \Big)$, 

we wish to form 

(the right Kan extension $\rightadj{ \boxed{20} \; { \Ran_R {\black G} } : {\leftcat\calL} \to {\black\calC} }$) 

of $G$ over $\rightadj R$.

We do this "pointwise".

Given (an object $\leftcat{ \boxed{1} \;  l\in\calL }$),

form (its right lax fiber $\leftcat{  \boxed{10} \; ( l \downarrow {\rightadj R} )   }$) as shown in the diagram above.

Then form 

(the limit ${\rightadj{  \boxed{20} \; \rightcat{\big( (Q=r) \black G\big)} \lim_{\black\calC}  }}$ in $\calC$), 

an arrow running from the top left in the above diagram southeast to the somewhat lower right,

together with 

(its universal cone $\rightadj{ \boxed{21} \; \pi : \rightcat{\big( (Q=r) \black G\big)}   {\rightadj\lim}_{\black\calC} \Rightarrow \rightcat{(Q=r) \black G}  }$), 

a 2-cell just below the just-mentioned arrow.

$$\leftcat{ \boxed{ \begin{array} {} && \calI & \xrightarrow[\smash{\kern4em}]{\textstyle \boxed{1} \; l} & \calL \\ && \rightadj{ \llap{ \boxed{11} \; ! } {\Bigg\uparrow} } & \leftcat{ \llap{ \boxed{11} \; \lambda } {\Bigg\Downarrow} } & \rightadj{ \llap{ \boxed{0} R } {\Bigg\uparrow} } & \kern2em \rightadj{     \llap{  \llap{ \boxed{31} \, 1_R  \kern-.3em  } \Downarrow \kern1em  }   }  \leftcat{ \searrow \rlap {1_\calL \; \boxed{30} } } \\ \leftcat\calI & \xrightarrow[ \smash{ \textstyle \leftcat{\boxed{12}} \; \rightcat r \leftcat{[\lambda]} } ]{ \smash{ \textstyle \text{right lax fiber} } } & \leftcat{ ( l \downarrow {\rightadj R} ) \smash{ \rlap{ \lower2.7ex{ \kern-2.1em \boxed{10} } } } } & \rightcat{ \xrightarrow[ \smash{\textstyle \boxed{11} \; Q=r} ]{} } & \rightcat\calR &   \rightadj{    \xrightarrow[ \smash{ \textstyle R \; \boxed{0} } ]{\kern8em}    }   & \calL \\ \leftcat\Vert &&&& \rightcat\Vert \\ \leftcat\calI \rlap{ \xrightarrow[ \textstyle \rightcat r ]{\kern24em} } &&&& \rightcat\calR \\ \end{array} } }$$

Algebraic set theory versus ETCS

Very much a preliminary draft, with errors!

This is a first cut at lining up and comparing various set theories and their models.

$$\boxed{  \begin{array} {l|c|c|ccc}   \text{reference}  &  \text{Awodey}  &  \text{Leinster}  &  \text{SGL VI.10}    \\   \hline    \text{theories}  &  \text{BIST: Basic Intuitionistic Set Theory}  & \text{ETCS: Elementary Theory of the Category of Sets}   &  \text{RZC}  \\   \hline    \text{models}   &  \text{categories of classes}  &  &  \text{WPTNNC}   \\    \end{array}    }$$

Awodey-Butz-Simpson-Streicher 2014 BIST APAL

https://www.sciencedirect.com/science/article/pii/S0168007213000730

Spaces, frames, locales

Here are some of the key concepts from Mac Lane and Moerdijk's SGL related to the above.

$\mathbf{(Spaces)}$ (arrows go in geometric direction), 

$\mathbf{(Frames)}$ (arrows go in algebraic direction), 

$\mathbf{(Locales)} = {\mathbf{(Frames)}}\op$ (arrows go in geometric direction),

Quoting Mac Lane-Moerdijk, Section IX.1,

For a map $f : S \to T$ of spaces, the locale-map $\Loc(f) : \Loc(S) \to \Loc(T)$ is given by the frame morphism $f\inv : \calO(T) \to \calO(S)$, 

i.e.

$\Big(f :S \to T\Big) \in \mathbf{(Spaces)} \xrightarrow{\textstyle \Loc} \mathbf{(Locales)} \ni \Big( \Loc(f) : \Loc(S) \to \Loc(T) \Big) = \Big( { \big( f\inv: \mathcal{O}(T) \to \calO(S) \big) }\op \Big) \in { \mathbf{(Frames)} }\op$.