I started reading Bart Jacob’s Categorical Logic and Type Theory
book today after seeing it mentioned on the Category Theory Zulip
because I’ve been seriously itching to get back into some mathy /
formalish stuff—life in hardware/software land just hasn’t been
cutting it. I have heard a dozen times, I once even tried to slog
through the CwF paper, about the categorical semantics for type theory
being presheaf based as the presheaf apparently captures the notion of
type families. However, after reading through Chapter 0: Prospectus in
Jacobs’ book, it sounds like he’s going to use fibrations to talk
about indexing rather than presheafs, so I wanted to update my
understanding, precisely, on what a fibration actually was. After
having moderate success recently in asking it for help to remember how
to do Either-based error returning rather than exception
throwing in Haskell, I thought I’d chat with ChatGPT viz-a-viz
categorical fibrations. Here’s the first thing it told me, which makes
sense:
[A] functor \(F: C \to D\) between categories is called a fibration if for every morphism \(f: X \to Y\) in the codomain category D and for every object \(X\) in the domain category \(C\), there exists:
- An object \(\text{fib}(f)\) in \(C\), called the “fiber” or “preimage” of \(f\) under \(F\), and
- A morphism \(p(f): \text{fib}(f) \to X\) in \(C\), called the “lifting” or “pullback” of \(f\) along \(F\), such that \(F(p(f)) = f\).
Ok GPT, I’m with you so far. So next I asked it if it could give me a diagram. “Certainly!” it replied, followed with an example using the category \(C\), a category with two objects \(0\) and \(1\), and only identity morphisms, and a functor \(F : C \to D\) where \(D\) was the category given by \(\langle\mathbb{N},\ \le\rangle\). It then gave an example of a \(p\) that depended on a morphism in \(C\) from \(0\) to \(1\). Which, in its own example did not exist.
I corrected it, telling that there was no morphism \(f : 0 \to 1\) in \(C\), so it gave me another example with \(C\) being the two object category with \(A\) and \(B\) and again only identity morphisms, and \(D\) being \(\textbf{Set}\). And then proceeded to, three different times, give me examples where the lifting morphism depended on a morphism \(A \to B\) in \(C\).
Finally, it gave me an example that makes sense after I told it, “That’s the same example! You’re still saying that id_A is A -> B, but this is only the case if A and B are isomorphic, leaving C to be a category with one object rather than two.”
This time it told me that \(f\) was \(\text{Id}_X\) then \(p(f)\) was \(\text{Id}_a\), but if \(f = \text{I}_Y\), then there was no morphism that lifts \(f\) in \(C\). Finally I asked it if the lifting \(p\) could be
\[ p(f) = \left\{\begin{array}{lr} f = \text{Id}_X & \text{Id}_A \\ f = \text{Id}_Y & \text{Id}_B \end{array}\right\} \]
To which it said, ah, yes, that should work too:
Apologies for the confusion caused by my previous incorrect statement. You are correct. In the given example, if f is the identity morphism on Y (f = id_Y), then the fiber fib(f) is the object B in C, and the lifting p(f) is the identity morphism id_B: B -> B.
Concluding with:
The fiber \(\text{fib}(f)\) for \(f\) in \(C\) is defined as follows:
- If \(f\) is the identity morphism on \(X\ (f\ =\ id_X)\), then the fiber \(\text{fib}(f)\) is the object \(A\) in \(C\).
- If \(f\) is the identity morphism on \(Y\ (f\ =\ id_Y)\), then the fiber \(\text{fib}(f)\) is the object \(B\) in \(C\).
To define the lifting \(p(f)\) for \(f: X \to Y\):
- If \(f\) is the identity morphism on \(X (f = id_X)\), then the lifting \(p(f)\) is the identity morphism \(id_A: A \to A\) in \(C\).
- If \(f\) is the identity morphism on \(Y (f = id_Y)\), then the lifting \(p(f)\) is the identity morphism \(id_B: B \to B\) in \(C\).
So if you’re following along this far you may have noticed that, because of ChatGPT’s bad examples, I missed an important detail: \(f\) is supposed to be \(X \to Y\) in \(D\)—it can’t be identities in \(D\)! The only way this works is if in \(F\)’s domain category, there is at least one morphism between \(A\) and \(B\). Here’s the last example that we arrived at together:
Consider the category \(C = \{A, B\}\) with two objects \(A\) and \(B\) and two non-identity morphisms \(f: A \to B\) and \(g: A \to B\). Let \(D\) be the category of sets.
Define a functor \(F: C \to D\) as follows:
- \(F(A) = X\), where \(X\) is a set,
- \(F(B) = Y\), where \(Y\) is another set,
- \(F(f) = h: X \to Y\), a function from \(X\) to \(Y\),
- \(F(g) = k: X \to Y\), another function from \(X\) to \(Y\).
In this case, the functor \(F\) maps objects \(A\) and \(B\) in \(C\) to sets \(X\) and \(Y\) in \(D\), respectively, and it maps the non-identity morphisms \(f\) and \(g\) in \(C\) to the functions \(h\) and \(k\) in \(D\).
To show that \(F\) is a fibration, let’s consider a morphism \(f: X \to Y\) in \(D\).
The fiber \(\text{fib}(f)\) for \(f\) in \(C\) is defined as the object \(A\) in \(C\).
To define the lifting \(p(f)\) for \(f: X \to Y\):
- If \(f\) is the function \(h: X \to Y\), the lifting \(p(f)\) is the morphism \(f: A \to B\) in \(C\).
- If \(f\) is the function \(k: X \to Y\), the lifting \(p(f)\) is the morphism \(g: A \to B\) in \(C\).
In both cases, applying \(F\) to the lifting \(p(f)\) yields the original morphism \(f: X \to Y\).
Therefore, the functor \(F: C \to D\) is a fibration since, for every morphism \(f: X \to Y\) in \(D\), the fiber \(\text{fib}(f) = A\) in \(C\), and the lifting \(p(f)\) satisfies \(F(p(f)) = f\).
Which, as it states, satisfies \(F(p(f)) = f\). I love that everything ChatGPT does is in the format that written standardized tests in middle school were required to be… “In conclusion, …”
Anyway, we got there eventually, and now I feel like I actually know what the hell a fibration is, and although it was an oblique route, ChatGPT was yet again helpful.