A Universe of Sorts

Key idea: can define a notion of a bundle p: E → B
The idea is that we want to generalize pullbacks into fibres.
A functor p: E \to B is called as a fibration if for each morphism f: b → b'downstairs, and an element e' ∈ E such that π(e') = b', then we have a lift of the morphism f into f♮, such that this morphism has a property called cartesianity .
Given:

        e'        |b ----> b'

e===f♮=>e'|       ||π      |πv       vb --f-->b'

Furthermore, to ensure that this is really a pullback, we ask for the condition that TODO

A set with some sort of "denotation by natural numbers" for each element of the set.
More formally, an omega set is a tuple (S, E: S → 2^N) such that E(s) ≠ ∅. The numbers E(s) are to be thought of as the denotation for the element s.
A morphism of omega sets (S, E) → (S', E') is a function f: S → S', and a partial function realiser(f): N → N such that for all s ∈ S, realiser(f)(E(s)) ⊂ E'(f(s)). That is, for every denotation d ∈ E(s), we have that the realiser realiser(f) maps d into the denotation of f(s), so we must have that d' = realiser(f(d)) lives in E'(f(s)).

This is a partial equivalence relation, so we only need symmetry and transitivity.
We consider partial equivalence relations (PERs) over N.
Let R be a PER. We think of those elements that are reflexively related (ie, xRx) as "in the domain" of the PER.
Thus we define domain(R) = { x | xRx }.
In this way, R is a real equivalence relation on domain(R).
We write N/R or domain(R)/R for the equivalence classes induced by R on N.
The category of PERs has as objects these PERs.
Intuitively, these give us subsets of the naturals ...

A fibration is cloven if for every arrow downstairs, there is a chosen cartesian arrow upstairs. So we have a function that computes the cartesian arrow upstairs for an arrow downstairs. This is different from the regular definition where we just know that there exists something upstairs.
Note that given a fibration, we can always cleave the fibration using choice.
Recall the definition of cartesian. For a functor p: E → B, for every arrow downstairs u: I → J ∈ B and every object Y ∈ E lying above J (ie, p(Y) = J), there is a cartesian lift of u given by X → Y for some X lying above I. ( p(X) = I).
Having made such a choice, every map u: I → J in B gives a functor u*: E_J → E_I from the the fiber E_J over Jto the fiber E_I over I. (Direction changes, pullback)
Recall that E_J is a subcategory of E where the objects are p^{-1}(J), and the morphisms are p^{-1}(id_J).
Implement the map u* as u*(y) as that object given by lifting the map u: I → J along Y. This is well-defined since we have a clevage to pick a unique u*(Y)!

defnu*(Y)-->Y        |        vI -u--->J

For morphisms, suppose we are given an arrow f: Y → Y' in E_J. Then we use the cartesianity of the lifted morphism to give us the lift. Mediatate on the below diagram:

A fibration is split if the cartesian lift of identity is identity, and the cartesian lift of compositions is the composition of the lifs (ie, the lifting is functorial).
In a cloven fibration, this is going to only be equal upto iso.
Example of a non-split fibration: Set-arrow, because pullbacks in set are not associative. Thus, the (A x B) x C != A x (B x C).
Being split has mathemaitcal content, because it's not possible to globally fix a functor being non-split.

A functor where all the equalities are isos. f(a . b) ~= f a . f b. f(id) ~= id.

§ Fibrational Category Theory, Sec 1.1, Sec 1.2