§ 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'
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 J
to 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 welldefined 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 nonsplit fibration: Setarrow, 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 nonsplit.
§ Pseudofunctors
 A functor where all the equalities are isos.
f(a . b) ~= f a . f b
. f(id) ~= id
.
§ Split Indexed Category
§ Lemma about pulling stuff back into the fiber

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