Give the equational formulation in a 2-category or
bicategory ( cf Exercise 7.30)
of the notion of a fibration with lex fibres, and of the same with comprehension.
In this sense show that
tgt:C^{v}® C freely adds comprehension to P:C® S, where the
objects of C^{v} are the vertical morphisms of C;
type-theoretically, this inserts an arbitrary division in the propositional
part of contexts. [Hint: for uniqueness of the meditator between the
total categories, you need to know that
omitted diagram environment
is a pullback in C^{v}, where
G = TPF = TPY
.] Although having comprehension is a property of the fibration,
viz that an adjoint exists, this construction is not idempotent;
explain why this is. In Section 5.3 we wanted to use
fibrations and comprehension to add partial maps; does the construction
achieve this goal?