The cograph of a function
is a quotient of the coproduct
by the equivalence relation generated from
.
We can also describe the cograph as a category, using the
following (strict) pullback:
In displayed
land, this would be the pullback of pointed sets along the functor
that picks out the domain and codomain of
, along with the map between them. Therefore, the resulting
category would have objects
,
, and a proofs that
over
.
Cograph of a functor
We can also form the cograph of a functor
; this yields a fibration over the interval category, where
,
, and
Cograph of a profunctor
More generally, the cograph of a profunctor
is a fibration over the interval category, where
,
, and