open import Cat.Diagram.Everything
open import Cat.Functor.Everything
open import Cat.Prelude

module wip.giraud
    {o ℓ o′ ℓ′} {C : Precategory o ℓ}
    (fc : Finitely-complete C)
    (cocomp : is-cocomplete o′ ℓ′ C)
  where