module Cubical.Categories.LocallySmall.Instances.Functor.IntoFiberCategory where open import Cubical.Categories.LocallySmall.Instances.Functor.IntoFiberCategory.Base public open import Cubical.Categories.LocallySmall.Instances.Functor.IntoFiberCategory.Properties public