ora-0015
1.3 Size, categories of categories, and indexed hypotheses
The phrase “the category of all categories” requires a size convention. Choose Grothendieck universes \(\mathcal U\in \mathcal V\). The category \(\mathbf{Cat}_{\mathcal U}\) of \(\mathcal U\)-small categories is generally not \(\mathcal U\)-small, but it is an object of the larger \(\mathbf{Cat}_{\mathcal V}\). This prevents the ambient hypothesis space from being mistaken for one of its own small objects.
Categories, functors, and natural transformations form a 2-category. Hence a learner may compare candidate worlds by functors and compare those comparisons by natural transformations; equality of hypothesis codes is not the intended semantics.
For a functor \(H:\mathcal T^{\mathrm{op}}\to \mathbf{Cat}\), the Grothendieck construction \(\int _{\mathcal T}H\) has objects \((T,x)\) with \(x\in H(T)\). A morphism \((T,x)\to (T',x')\) consists of a map \(u:T\to T'\) and a morphism \(x\to H(u)(x')\) in \(H(T)\). The projection
is a fibration whose fiber over \(T\) is equivalent to \(H(T)\).
For ORACLE, \(\mathcal T\) is the category of interaction transcripts and \(H(T)\) is the category of hypotheses consistent with transcript \(T\). The construction turns a changing family of hypothesis categories into one typed total space.