Post #2093347

I'm quite fond of the proof that π : U• → U is an object classifier - i.e. that is terminal in the category with objects (small) maps and morphisms cartesian squares. We show that a cartesian square from f to π is equivalent to the proposition that f is a small map (a concept which - amongst many other things - @FredrikBakke has recently formalised for agda-synthetic-categories). First we can straighten a cartesian map of arrows into a cartesian map of families. Explicitly this is a map (X : A → U) and a fibrewise equivalence Πₐ fib_f(a) ≃ 𝑋(𝑎). Then by a [rather choice theorem](https://samtoth.github.io/agda-synthetic-categories/Foundations.TheoremOfChoice), this is exactly the proposition that f is a small map. Now it's also easy to show that for any subclass of maps that has a classifier (such as the small left fibrations!) we have a factorisation of cartesian squares through this classifying map. Formalisation coming soon hopefully...