module Cubical.Categories.LocallySmall.Displayed.Instances.Weaken where open import Cubical.Categories.LocallySmall.Displayed.Instances.Weaken.Base public