§ Fibrational category theory, sec 1.1, sec 1.2

        e'
        |

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

§ Omega sets

§ PERs

§ Cloven Fibrations

defn
u*(Y)-->Y
        |
        v
I -u--->J

§ Split Fibrations

§ Pseudofunctors

§ Split Indexed Category

§ Lemma about pulling stuff back into the fiber