The category of arrows
The category of arrows, with morphisms commutative squares.
We set this up as a specialization of the comma category
comma L R,
R are both the identity functor.
We also define the typeclass
has_lift, representing a choice of a lift
of a commutative square (that is, a diagonal morphism making the two triangles commute).
A morphism in the arrow category is a commutative square connecting two objects of the arrow category.
We can also build a morphism in the arrow category out of any commutative square in
A lift of a commutative square is a diagonal morphism making the two triangles commute.
has_lift sq says that there is some
lift_struct sq, i.e., that it is possible to find a
diagonal morphism making the two triangles commute.
has_lift sq, obtain a lift.
C ⥤ D induces a functor between the corresponding arrow categories.