other kinds of fibrations (#29)

* [racket] switch to string-ci<? [don't know if this is what was causing the weird sorting??]

* Right fibrations.

* rename nodes + garbage collect

* qualify fibration with "cartesian" as needed

* choose better notation

* typo

Co-authored-by: Jon Sterling <jon@jonmsterling.com>

_lectures/categorical-foundations.md

@@ -21,4 +21,5 @@ We will draw on the following materials:
 @include{0008}
 @include{0009}
 @include{000E}
+@include{0012}
 @include{000N}

_nodes/0000.md

@@ -15,7 +15,7 @@ following data {%cite ahrens-lumsdaine:2019%}:
     \\[
       E\Sub{f}(\bar{x},\bar{y}) \times E\Sub{g}(\bar{y},\bar{z}) \to E\Sub{f;g}(\bar{x},\bar{z})
     \\]
-   that we will denote like ordinary (digrammatic) function composition,
+   that we will denote like ordinary (diagrammatic) function composition,
 5. such that the following equations hold:
   \\[
       \Idn{\bar{x}};\bar{h} = \bar{h}\qquad

_nodes/0002.md

@@ -7,7 +7,7 @@ A displayed category $E$ over $B$ is said to be a *cartesian fibration*, when
 for each morphism $f : x \to y$ and displayed object $\bar{y}\in E\Sub{y}$, there
 exists a displayed object $\bar{x}\in E\Sub{x}$ and a *cartesian* morphism
 $\bar{f} : \bar{x}\to\Sub{f} \bar{y}$. Note that the pair $(\bar{x},\bar{f})$ is unique up to
-unique isomorphism, so being fibered is a *property* of a displayed category.
+unique isomorphism, so being a cartesian fibration is a *property* of a displayed category.
 
 There are other variations of fibration. For instance, $E$ is said to be an
 *isofibration* when the condition above holds just for isomorphisms $f : x

_nodes/000C.md

@@ -3,19 +3,19 @@ title: Relationship to Street's fibrations
 macrolib: topos
 ---
 
-In classical category theory, fibrations are defined by
+In classical category theory, cartesian fibrations are defined by
 Grothendieck {%cite sga:1 -A%} to be certain functors $E\to B$ such that any morphism $f:x\to Pv$
 in $B$ lies strictly underneath a cartesian morphism in $E$. As we have
 discussed, this condition cannot be formulated unless equality is meaningful
 for the collection of objects of $B$.
 
-There is an alternative definition of fibration {%cite street:1980%} that avoids
+There is an alternative definition of cartesian fibration {%cite street:1980%} that avoids
 equality of objects; here we require for each $f:x\to Pv$ a cartesian morphism
 $h:\InvImg{f}v \to v$ together with an isomorphism $\phi : P(\InvImg{f}v)\cong x$
 such that $\phi^{-1};Ph = f$.
 
 By unrolling definitions, it is not difficult to see that the displayed
-category $P\Sub{\bullet}$ is a fibration in our sense if and only if the functor
+category $P\Sub{\bullet}$ is a cartesian fibration in our sense if and only if the functor
 $P:E\to B$ was a fibration in Street's sense. Moreover, it can be seen that the
 Grothendieck construction yields a *Grothendieck* fibration
 $\TotCat{P\Sub{\bullet}}\to B$; hence we have introduced by accident a convenient

_nodes/000H.md

@@ -4,7 +4,7 @@ macrolib: topos
 ---
 
 We will reformulate the above in a way that uses only the language that makes
-sense for an arbitrary fibration, though for now we stick with $\FAM{C}$. Given
+sense for an arbitrary cartesian fibration, though for now we stick with $\FAM{C}$. Given
 $u,v\in \FAM{C}[I]$, we have a "relative hom family" $[u,v]\in\Sl{\SET}{I}$,
 defined in {%ref 000G%}. The fact that each $[u,v]\Sub{i}$ is the set of all
 morphisms $u\Sub{i}\to v\Sub{i}$ can be rephrased more abstractly.

_nodes/000I.md

@@ -4,7 +4,7 @@ macrolib: topos
 ---
 
 Based on our explorations above, we are now prepared to write down (and
-understand) the proper definition of local smallness for an arbitrary fibration
+understand) the proper definition of local smallness for an arbitrary cartesian fibration
 $E$ over $B$, which should be thought of as a (potentially large) category
 relative to $B$.
 
@@ -66,7 +66,7 @@ This structure can be rephrased in terms of a displayed category $\CandHom{x}{u}
    \end{tikzpicture}
    »
 
-**Definition.** A fibration $E$ over $B$ is *locally small* if and only if for
+**Definition.** A cartesian fibration $E$ over $B$ is *locally small* if and only if for
 each $x\in B$ and $u,v\in E\Sub{x}$, the total category $\TotCat{\CandHom{x}{u}{v}}$
 has a terminal object.
 

_nodes/000K.md

@@ -5,6 +5,6 @@ macrolib: topos
 
 Up to equivalence of categories, we may detect global smallness of a category $C$ from the perspective of the family fibration $\FAM{C}$ {%ref 0006%}. In particular, a category is equivalent to a globally small category when its family fibration has a *generic object* in the following sense.
 
-**Definition.** Let $E$ be a fibration over $B$; a *generic object* for $E$ is defined to be an object $\bar{u}\in \TotCat{E}$  such that for any $\bar{z}\in \TotCat{E}$ there exists a cartesian map $\bar{z}\to \bar{u}$.
+**Definition.** Let $E$ be a cartesian fibration over $B$; a *generic object* for $E$ is defined to be an object $\bar{u}\in \TotCat{E}$  such that for any $\bar{z}\in \TotCat{E}$ there exists a cartesian map $\bar{z}\to \bar{u}$.
 
 @include{000L}

_nodes/000N.md

@@ -5,10 +5,10 @@ macrolib: topos
 
 The purpose of this section is to develop the relationship between *internal
 categories* (categories defined in the internal language of a category $B$) and
-fibrations over $B$, generalizing the relationship between categories internal
+cartesian fibrations over $B$, generalizing the relationship between categories internal
 to $\SET$ (i.e. small categories) and their family fibrations over $\SET$.
 
-**Definition.** A fibration is called *small* when it is both locally small
+**Definition.** A cartesian fibration is called *small* when it is both locally small
 {%ref 000I%} and globally small {%ref 000J%}.
 
 We have already seen in {%ref 000G%} and {%ref 000L%} that smallness in the

_nodes/000P.md

@@ -3,4 +3,4 @@ title: The definition of global smallness
 macrolib: topos
 ---
 
-**Definition.** A fibration $E$ over $B$ is called *globally small* when it has a generic object {%ref 000K%}.
+**Definition.** A cartesian fibration $E$ over $B$ is called *globally small* when it has a generic object {%ref 000K%}.

_nodes/000U.md

@@ -6,7 +6,7 @@ macrolib: topos
 The foregoing characterization {%ref 000T%} of cartesian maps in $\OpCat{E}$
 immediately implies that $\OpCat{E}$ is fibered over $B$.
 
-**Corollary.** The displayed category $\OpCat{E}$ is a fibration.
+**Corollary.** The displayed category $\OpCat{E}$ is a cartesian fibration.
 
 **Proof.**
 Fixing $\bar{y}\in \OpCat{E}\Sub{y}$ and $f:x\to y\in B$, we must

_nodes/000W.md

@@ -1,5 +1,5 @@
 ---
-title: The externalization is a fibration
+title: The externalization is a cartesian fibration
 macrolib: topos
 ---
 

_nodes/000Z.md

@@ -3,8 +3,8 @@ title: The internalization of a small fibration
 macrolib: topos
 ---
 
-Let $C$ be a small fibration {%ref 000N%} over $B$ a category with finite
-limits, i.e. a fibration that is both locally small {%ref 000I%} and globally
+Let $C$ be a small cartesian fibration {%ref 000N%} over $B$ a category with finite
+limits, i.e. a cartesian fibration that is both locally small {%ref 000I%} and globally
 small {%ref 000P%}. We will show that $C$ is equivalent to the externalization
 {%ref 000V%} of an internal category {%ref 000O%} $\underline{C}$ in $B$,
 namely the the full internal subcategory {%ref 0011%} associated to the generic

_nodes/0011.md

@@ -3,7 +3,7 @@ title: The full internal subcategory associated to a displayed object
 macrolib: topos
 ---
 
-This full internal subfibration {%ref 0010%} associated to a displayed object $\bar{u}$ of a locally small fibration $E$ over $B$ can be seen to be equivalent to the externalization
+This full internal subfibration {%ref 0010%} associated to a displayed object $\bar{u}$ of a locally small cartesian fibration $E$ over $B$ can be seen to be equivalent to the externalization
 of an internal category $\gl{\bar{u}}$ in $B$. In particular, we let the object of objects $\gl{\bar{u}}\Sub{0}$ be $u$ itself; defining the object of arrows $\gl{\bar{u}}\Sub{1}$ is more complex, making critical use of the local smalness of $E$ over $B$.
 
 We will think of the fiber $E\Sub{u\times u}$ as the category of

_nodes/0012.md

@@ -0,0 +1,6 @@
+---
+title: Other kinds of fibrations
+macrolib: topos
+---
+
+@include{0013}

_nodes/0013.md

@@ -0,0 +1,98 @@
+---
+title: Right fibrations
+macrolib: topos
+---
+
+**Definition.** A cartesian fibration $E$ over $B$ is said to be a *right fibration*
+when all displayed morphisms in $E$ are cartesian.
+
+Recall from {%ref 0005 %} that for every $b\in B$, the collection of displayed
+objects $E\Sub{b}$ and vertical maps $E\Sub{1\Sub{b}}$ forms a category. When $E$ is
+a right fibration over $B$, this category is in fact a *groupoid*.
+
+**Theorem.** A cartesian fibration $E$ over $B$ is a right fibration if and only if
+all its vertical maps are isomorphisms.
+
+**Proof.** Suppose that $E$ is a right fibration over $B$, and fix $b\in B$,
+$\bar{b}\in E\Sub{b}$, and a vertical map $f:\bar{b}\to\Sub{1\Sub{b}} \bar{b}$.
+Using the hypothesis that $f$ is cartesian, it has a unique section
+$g:\bar{b}\to\Sub{1\Sub{b}} \bar{b}$ as follows:
+«
+  \begin{tikzpicture}[diagram]
+    \SpliceDiagramSquare{
+      west/style = lies over,
+      east/style = lies over,
+      north/node/style = upright desc,
+      height = 1.5cm,
+      nw = \bar{b},
+      ne = \bar{b},
+      north = f,
+      sw = b,
+      se = b,
+      south/style = double,
+      nw/style = pullback,
+    }
+    \node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{b}$};
+    \node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$b$};
+    \draw[lies over] (u') to (u);
+    \draw[double,bend left=30] (u') to (ne);
+    \draw[double] (u) to (sw);
+    \draw[->,exists] (u') to node [desc] {$g$} (nw);
+  \end{tikzpicture}
+»
+Likewise, because $g$ is cartesian, $f$ is the unique section of $g$; thus $f$ is an
+isomorphism in $E\Sub{b}$.
+
+Conversely, suppose that $E$ is a cartesian fibration whose vertical maps are
+isomorphisms. Fix $f:x\to y \in B$ and an arbitrary displayed morphism
+$\bar{g}:\bar{x}\to\Sub{f}\bar{y}$. Then $\bar{g}$ is the precomposition of a
+cartesian lift $\bar{f}:\bar{x}\Sup{\prime}\to\Sub{f}\bar{y}$ with a vertical map:
+«
+  \begin{tikzpicture}[diagram]
+    \SpliceDiagramSquare{
+      west/style = lies over,
+      east/style = lies over,
+      north/node/style = upright desc,
+      height = 1.5cm,
+      nw = \bar{x}',
+      ne = \bar{y},
+      sw = x,
+      north = \bar{f},
+      south = f,
+      se = y,
+      nw/style = pullback,
+    }
+    \node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{x}$};
+    \node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$x$};
+    \draw[lies over] (u') to (u);
+    \draw[->,bend left=30] (u') to node [sloped,above] {$\bar{g}$} (ne);
+    \draw[double] (u) to (sw);
+    \draw[->,exists] (u') to node [desc] {$i$} (nw);
+  \end{tikzpicture}
+»
+Because vertical maps are isomorphisms and $\bar{f}$ is cartesian, we can observe
+that $\bar{g}$ is cartesian as follows, writing $\bar{m} : \bar{u}\to\Sub{m}
+\bar{x}\Sup{\prime}$ for the unique factorization of $\bar{h}$ through $\bar{f}$ over $m$:
+«
+  \begin{tikzpicture}[diagram]
+    \SpliceDiagramSquare{
+      west/style = lies over,
+      east/style = lies over,
+      north/node/style = upright desc,
+      height = 1.5cm,
+      nw = \bar{x},
+      ne = \bar{y},
+      sw = x,
+      north = \bar{g},
+      south = f,
+      se = y,
+      nw/style = pullback,
+    }
+    \node (u') [above left = 1.5cm of nw,xshift=-1cm] {$\bar{u}$};
+    \node (u) [above left = 1.5cm of sw,xshift=-1cm] {$u$};
+    \draw[lies over] (u') to (u);
+    \draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
+    \draw[->] (u) to node [sloped,below] {$m$} (sw);
+    \draw[->,exists] (u') to node [desc] {$\bar{m};i\Sup{-1}$} (nw);
+  \end{tikzpicture}
+»

macros/macro-kit.rkt

@@ -41,7 +41,7 @@
 
 (define (macro-list)
   (define (lt? repr1 repr2)
-    (string<? (macro-repr-name repr1) (macro-repr-name repr2)))
+    (string-ci<? (macro-repr-name repr1) (macro-repr-name repr2)))
 
   (sort (set->list (macro-set)) lt?))