module Chapter8.Container.Morphism.Cartesian.Main where open import Chapter8.Container.Morphism.Cartesian open import Chapter8.Container.Morphism.Cartesian.Identity open import Chapter8.Container.Morphism.Cartesian.Composition.Vertical