## § Fibrational category theory, sec 1.1, sec 1.2

• 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'

• We want:

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

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

#### § Omega sets

• 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)).

#### § PERs

• 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 ...

#### § Cloven Fibrations

• 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)!
defn
u*(Y)-->Y
|
v
I -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:

#### § Split Fibrations

• 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.

#### § Pseudofunctors

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

#### § Lemma about pulling stuff back into the fiber

• E(X, Y) != disjoint union (u: πX -> πY) E_{πX} (X, u*(Y))