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