Discrete opfibration (source code)

= Discrete opfibration
{title2=$F:\mathcal C\to\mathcal D$}

A <functor> with a unique lift, from each specified object $c$, of every arrow $Fc\to d$. The lifted arrow's target is part of the uniqueness requirement. This is dual to a <discrete fibration>. Lifting a <cocone> of a finite <connected category> gives a cocone upstairs: lifts of its legs have a common target because uniqueness identifies targets along every diagram arrow. Thus a discrete opfibration over a <weakly filtered category> has weakly filtered domain, including the possibility of an empty domain.