Interpolant in a Fibration
Let
be a Cartesian
Fibration, and let
be a commuting square in
, as in the following diagram:
Now, let
, and
, and
be a vertical morphism in
. An interpolant of
over the square
consists of:
- An object
- A morphism
- A morphism
Such that
, where
is the canonical iso
induced by the square
.