module Cubical.Categories.Instances.TotalCategory where open import Cubical.Categories.Instances.TotalCategory.Base public open import Cubical.Categories.Instances.TotalCategory.Properties public