Lifting as a KZ-doctrine

                        Marcelo P. Fiore
                        <mf@dcs.ed.ac.uk>

                  Department of Computer Science 
           Laboratory for Foundations of Computer Science 
            University of Edinburgh, The King's Buildings 
                   Edinburgh EH9 3JZ, Scotland


                            Synopsis 

In a cartesian closed category with an initial object and a dominance 
that classifies it, an intensional notion of approximation between maps
---the path relation (c.f. link relation)--- is defined. It is shown 
that if such a category admits strict/upper-closed factorisations then 
it preorder-enriches (as a cartesian closed category) with respect to 
the path relation. By imposing further axioms we can, on the one hand, 
endow maps and proofs of their approximations (viz. paths) with the 
2-dimensional algebraic structure of a sesqui-category and, on the 
other, characterise lifting as a preorder-enriched lax colimit. As a 
consequence of the latter the lifting (or partial map classifier) monad
becomes a KZ-doctrine.