From 500757e2e1109e46c704e1d4c5ff754d59dfa826 Mon Sep 17 00:00:00 2001
From: Andreas Nuyts <andreas.nuyts@kuleuven.be>
Date: Fri, 25 Oct 2024 20:02:25 +0200
Subject: [PATCH 1/3] Cubical.Categories: merge Constructions with Instances
 (issue #765).

---
 Cubical/Categories/Additive/Quotient.agda                   | 2 +-
 Cubical/Categories/Constructions/Free/Category.agda         | 5 -----
 Cubical/Categories/Constructions/TotalCategory.agda         | 5 -----
 Cubical/Categories/Displayed/BinProduct.agda                | 2 +-
 Cubical/Categories/Displayed/Cartesian.agda                 | 2 +-
 .../Displayed/Constructions/LeftAdjointToReindex.agda       | 2 +-
 .../Categories/Displayed/Constructions/Reindex/Base.agda    | 2 +-
 .../Displayed/Constructions/StructureOver/Properties.agda   | 2 +-
 .../Categories/Displayed/Constructions/TotalCategory.agda   | 2 +-
 Cubical/Categories/Displayed/Constructions/Weaken/Base.agda | 2 +-
 Cubical/Categories/Displayed/Instances/Path.agda            | 2 +-
 Cubical/Categories/Displayed/Reasoning.agda                 | 2 +-
 Cubical/Categories/Displayed/Weaken.agda                    | 2 +-
 Cubical/Categories/Functors/HomFunctor.agda                 | 2 +-
 .../Categories/{Constructions => Instances}/BinProduct.agda | 2 +-
 .../{Constructions => Instances}/DisplayOverTerminal.agda   | 2 +-
 Cubical/Categories/Instances/EilenbergMoore.agda            | 2 +-
 .../Categories/{Constructions => Instances}/Elements.agda   | 4 ++--
 .../{Constructions => Instances}/EssentialImage.agda        | 4 ++--
 Cubical/Categories/{Constructions => Instances}/Free.agda   | 2 +-
 Cubical/Categories/Instances/Free/Category.agda             | 5 +++++
 .../{Constructions => Instances}/Free/Category/Base.agda    | 2 +-
 .../{Constructions => Instances}/Free/Category/Quiver.agda  | 4 ++--
 .../{Constructions => Instances}/Free/Functor.agda          | 4 ++--
 .../{Constructions => Instances}/FullSubcategory.agda       | 2 +-
 Cubical/Categories/Instances/Functors.agda                  | 2 +-
 Cubical/Categories/Instances/Functors/Currying.agda         | 2 +-
 Cubical/Categories/{Constructions => Instances}/Lift.agda   | 2 +-
 .../Categories/{Constructions => Instances}/Opposite.agda   | 2 +-
 Cubical/Categories/{Constructions => Instances}/Power.agda  | 4 ++--
 .../Categories/{Constructions => Instances}/Product.agda    | 2 +-
 .../Categories/{Constructions => Instances}/Quotient.agda   | 2 +-
 Cubical/Categories/{Constructions => Instances}/Slice.agda  | 6 +++---
 .../Categories/{Constructions => Instances}/Slice/Base.agda | 2 +-
 .../{Constructions => Instances}/Slice/Functor.agda         | 4 ++--
 .../{Constructions => Instances}/Slice/Properties.agda      | 6 +++---
 .../Categories/{Constructions => Instances}/SubObject.agda  | 4 ++--
 Cubical/Categories/Instances/TotalCategory.agda             | 5 +++++
 .../{Constructions => Instances}/TotalCategory/Base.agda    | 2 +-
 .../TotalCategory/Properties.agda                           | 4 ++--
 .../{Constructions => Instances}/TwistedArrow.agda          | 6 +++---
 .../Categories/{Constructions => Instances}/Vertical.agda   | 4 ++--
 Cubical/Categories/Monad/Base.agda                          | 2 +-
 Cubical/Categories/Monoidal/Base.agda                       | 2 +-
 Cubical/Categories/Presheaf/Morphism.agda                   | 4 ++--
 Cubical/Categories/Presheaf/NonPresheaf/Forget.agda         | 2 +-
 Cubical/Categories/Presheaf/Properties.agda                 | 6 +++---
 Cubical/Categories/Presheaf/Representable.agda              | 4 ++--
 Cubical/Categories/Profunctor/Base.agda                     | 2 +-
 Cubical/Categories/RezkCompletion/Construction.agda         | 2 +-
 Cubical/Categories/Site/Cover.agda                          | 2 +-
 Cubical/Categories/Site/Instances/ZariskiCommRing.agda      | 2 +-
 Cubical/Categories/Site/Sheaf.agda                          | 2 +-
 .../Categories/Site/Sheafification/UniversalProperty.agda   | 2 +-
 Cubical/Categories/Yoneda.agda                              | 2 +-
 Cubical/Tactics/CategorySolver/Reflection.agda              | 2 +-
 Cubical/Tactics/CategorySolver/Solver.agda                  | 4 ++--
 Cubical/Tactics/FunctorSolver/Reflection.agda               | 4 ++--
 Cubical/Tactics/FunctorSolver/Solver.agda                   | 4 ++--
 59 files changed, 87 insertions(+), 87 deletions(-)
 delete mode 100644 Cubical/Categories/Constructions/Free/Category.agda
 delete mode 100644 Cubical/Categories/Constructions/TotalCategory.agda
 rename Cubical/Categories/{Constructions => Instances}/BinProduct.agda (98%)
 rename Cubical/Categories/{Constructions => Instances}/DisplayOverTerminal.agda (93%)
 rename Cubical/Categories/{Constructions => Instances}/Elements.agda (97%)
 rename Cubical/Categories/{Constructions => Instances}/EssentialImage.agda (94%)
 rename Cubical/Categories/{Constructions => Instances}/Free.agda (93%)
 create mode 100644 Cubical/Categories/Instances/Free/Category.agda
 rename Cubical/Categories/{Constructions => Instances}/Free/Category/Base.agda (99%)
 rename Cubical/Categories/{Constructions => Instances}/Free/Category/Quiver.agda (97%)
 rename Cubical/Categories/{Constructions => Instances}/Free/Functor.agda (99%)
 rename Cubical/Categories/{Constructions => Instances}/FullSubcategory.agda (98%)
 rename Cubical/Categories/{Constructions => Instances}/Lift.agda (95%)
 rename Cubical/Categories/{Constructions => Instances}/Opposite.agda (96%)
 rename Cubical/Categories/{Constructions => Instances}/Power.agda (88%)
 rename Cubical/Categories/{Constructions => Instances}/Product.agda (96%)
 rename Cubical/Categories/{Constructions => Instances}/Quotient.agda (98%)
 rename Cubical/Categories/{Constructions => Instances}/Slice.agda (50%)
 rename Cubical/Categories/{Constructions => Instances}/Slice/Base.agda (99%)
 rename Cubical/Categories/{Constructions => Instances}/Slice/Functor.agda (98%)
 rename Cubical/Categories/{Constructions => Instances}/Slice/Properties.agda (92%)
 rename Cubical/Categories/{Constructions => Instances}/SubObject.agda (96%)
 create mode 100644 Cubical/Categories/Instances/TotalCategory.agda
 rename Cubical/Categories/{Constructions => Instances}/TotalCategory/Base.agda (96%)
 rename Cubical/Categories/{Constructions => Instances}/TotalCategory/Properties.agda (95%)
 rename Cubical/Categories/{Constructions => Instances}/TwistedArrow.agda (83%)
 rename Cubical/Categories/{Constructions => Instances}/Vertical.agda (86%)

diff --git a/Cubical/Categories/Additive/Quotient.agda b/Cubical/Categories/Additive/Quotient.agda
index 16e13ec179..e843940f83 100644
--- a/Cubical/Categories/Additive/Quotient.agda
+++ b/Cubical/Categories/Additive/Quotient.agda
@@ -7,7 +7,7 @@ open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Categories.Additive.Base
 open import Cubical.Categories.Additive.Properties
 open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Constructions.Quotient
+open import Cubical.Categories.Instances.Quotient
 open import Cubical.Categories.Limits.Terminal
 open import Cubical.Foundations.Prelude
 open import Cubical.HITs.SetQuotients renaming ([_] to ⟦_⟧)
diff --git a/Cubical/Categories/Constructions/Free/Category.agda b/Cubical/Categories/Constructions/Free/Category.agda
deleted file mode 100644
index 1b1cda7c79..0000000000
--- a/Cubical/Categories/Constructions/Free/Category.agda
+++ /dev/null
@@ -1,5 +0,0 @@
-{-# OPTIONS --safe #-}
-
-module Cubical.Categories.Constructions.Free.Category where
-
-open import Cubical.Categories.Constructions.Free.Category.Base public
diff --git a/Cubical/Categories/Constructions/TotalCategory.agda b/Cubical/Categories/Constructions/TotalCategory.agda
deleted file mode 100644
index 6ffd24c31d..0000000000
--- a/Cubical/Categories/Constructions/TotalCategory.agda
+++ /dev/null
@@ -1,5 +0,0 @@
-{-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.TotalCategory where
-
-open import Cubical.Categories.Constructions.TotalCategory.Base public
-open import Cubical.Categories.Constructions.TotalCategory.Properties public
diff --git a/Cubical/Categories/Displayed/BinProduct.agda b/Cubical/Categories/Displayed/BinProduct.agda
index 1f883beff7..abd7070ca2 100644
--- a/Cubical/Categories/Displayed/BinProduct.agda
+++ b/Cubical/Categories/Displayed/BinProduct.agda
@@ -5,7 +5,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
 open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 open import Cubical.Categories.Displayed.Base
 
 private
diff --git a/Cubical/Categories/Displayed/Cartesian.agda b/Cubical/Categories/Displayed/Cartesian.agda
index 6dedcb8f00..b2ce2b7473 100644
--- a/Cubical/Categories/Displayed/Cartesian.agda
+++ b/Cubical/Categories/Displayed/Cartesian.agda
@@ -15,7 +15,7 @@ import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.NaturalTransformation
-open import Cubical.Categories.Constructions.Vertical
+open import Cubical.Categories.Instances.Vertical
 
 module Cubical.Categories.Displayed.Cartesian where
 
diff --git a/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda b/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda
index bf150c4887..22f2f478e2 100644
--- a/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda
+++ b/Cubical/Categories/Displayed/Constructions/LeftAdjointToReindex.agda
@@ -14,7 +14,7 @@ open import Cubical.Categories.Functor
 
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Constructions.Weaken.Base
-open import Cubical.Categories.Constructions.TotalCategory
+open import Cubical.Categories.Instances.TotalCategory
 
 private
   variable
diff --git a/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda b/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
index 466d7cc677..4770e19eb1 100644
--- a/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
+++ b/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
@@ -66,7 +66,7 @@ open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Functor
 import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 open import Cubical.Categories.Displayed.Section.Base
-open import Cubical.Categories.Constructions.TotalCategory as TotalCat
+open import Cubical.Categories.Instances.TotalCategory as TotalCat
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Terminal
 
diff --git a/Cubical/Categories/Displayed/Constructions/StructureOver/Properties.agda b/Cubical/Categories/Displayed/Constructions/StructureOver/Properties.agda
index 4d0948030a..11aba56578 100644
--- a/Cubical/Categories/Displayed/Constructions/StructureOver/Properties.agda
+++ b/Cubical/Categories/Displayed/Constructions/StructureOver/Properties.agda
@@ -13,7 +13,7 @@ open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Displayed.HLevels
 open import Cubical.Categories.Displayed.Constructions.StructureOver.Base
-open import Cubical.Categories.Constructions.TotalCategory
+open import Cubical.Categories.Instances.TotalCategory
 
 private
   variable
diff --git a/Cubical/Categories/Displayed/Constructions/TotalCategory.agda b/Cubical/Categories/Displayed/Constructions/TotalCategory.agda
index 24393f58ec..171e73a01f 100644
--- a/Cubical/Categories/Displayed/Constructions/TotalCategory.agda
+++ b/Cubical/Categories/Displayed/Constructions/TotalCategory.agda
@@ -14,7 +14,7 @@ open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Displayed.HLevels
 open import Cubical.Categories.Displayed.Section.Base
 open import Cubical.Categories.Displayed.Instances.Terminal hiding (introF)
-open import Cubical.Categories.Constructions.TotalCategory as TC hiding (intro)
+open import Cubical.Categories.Instances.TotalCategory as TC hiding (intro)
 
 private
   variable
diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
index e795f4b873..1b7a0dd39c 100644
--- a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
+++ b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
@@ -15,7 +15,7 @@ open import Cubical.Categories.Functor
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Section.Base
 open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Constructions.TotalCategory as TC
+open import Cubical.Categories.Instances.TotalCategory as TC
   hiding (intro)
 
 private
diff --git a/Cubical/Categories/Displayed/Instances/Path.agda b/Cubical/Categories/Displayed/Instances/Path.agda
index dc1f1ffb38..e6696b5be0 100644
--- a/Cubical/Categories/Displayed/Instances/Path.agda
+++ b/Cubical/Categories/Displayed/Instances/Path.agda
@@ -16,7 +16,7 @@ open import Cubical.Data.Unit
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.HLevels
 open import Cubical.Categories.Displayed.Functor
diff --git a/Cubical/Categories/Displayed/Reasoning.agda b/Cubical/Categories/Displayed/Reasoning.agda
index 223d4ef8c1..5ef8986846 100644
--- a/Cubical/Categories/Displayed/Reasoning.agda
+++ b/Cubical/Categories/Displayed/Reasoning.agda
@@ -24,7 +24,7 @@ open import Cubical.Foundations.Transport
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Constructions.TotalCategory.Base
+open import Cubical.Categories.Instances.TotalCategory.Base
 open import Cubical.Categories.Displayed.Base
 
 module Cubical.Categories.Displayed.Reasoning
diff --git a/Cubical/Categories/Displayed/Weaken.agda b/Cubical/Categories/Displayed/Weaken.agda
index 41d645d32c..567092cb8a 100644
--- a/Cubical/Categories/Displayed/Weaken.agda
+++ b/Cubical/Categories/Displayed/Weaken.agda
@@ -5,7 +5,7 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Constructions.TotalCategory
+open import Cubical.Categories.Instances.TotalCategory
 
 private
   variable
diff --git a/Cubical/Categories/Functors/HomFunctor.agda b/Cubical/Categories/Functors/HomFunctor.agda
index ec0bfd5bbb..59e7832950 100644
--- a/Cubical/Categories/Functors/HomFunctor.agda
+++ b/Cubical/Categories/Functors/HomFunctor.agda
@@ -6,7 +6,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Instances.Sets
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 
 private
   variable
diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Instances/BinProduct.agda
similarity index 98%
rename from Cubical/Categories/Constructions/BinProduct.agda
rename to Cubical/Categories/Instances/BinProduct.agda
index da80ea1b07..e10d98d83e 100644
--- a/Cubical/Categories/Constructions/BinProduct.agda
+++ b/Cubical/Categories/Instances/BinProduct.agda
@@ -1,7 +1,7 @@
 -- Product of two categories
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.BinProduct where
+module Cubical.Categories.Instances.BinProduct where
 
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Categories/Constructions/DisplayOverTerminal.agda b/Cubical/Categories/Instances/DisplayOverTerminal.agda
similarity index 93%
rename from Cubical/Categories/Constructions/DisplayOverTerminal.agda
rename to Cubical/Categories/Instances/DisplayOverTerminal.agda
index 4c16306266..74050b154e 100644
--- a/Cubical/Categories/Constructions/DisplayOverTerminal.agda
+++ b/Cubical/Categories/Instances/DisplayOverTerminal.agda
@@ -4,7 +4,7 @@
 -}
 
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.DisplayOverTerminal where
+module Cubical.Categories.Instances.DisplayOverTerminal where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Data.Unit
diff --git a/Cubical/Categories/Instances/EilenbergMoore.agda b/Cubical/Categories/Instances/EilenbergMoore.agda
index 0996d0fe2b..5c9ebae7b4 100644
--- a/Cubical/Categories/Instances/EilenbergMoore.agda
+++ b/Cubical/Categories/Instances/EilenbergMoore.agda
@@ -12,7 +12,7 @@ open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)
 open import Cubical.Categories.NaturalTransformation.Base
 open import Cubical.Categories.Monad.Base
 open import Cubical.Categories.Instances.FunctorAlgebras
-open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Instances.FullSubcategory
 open import Cubical.Categories.Adjoint
 
 private
diff --git a/Cubical/Categories/Constructions/Elements.agda b/Cubical/Categories/Instances/Elements.agda
similarity index 97%
rename from Cubical/Categories/Constructions/Elements.agda
rename to Cubical/Categories/Instances/Elements.agda
index c5e1c27c3c..38ee666615 100644
--- a/Cubical/Categories/Constructions/Elements.agda
+++ b/Cubical/Categories/Instances/Elements.agda
@@ -12,7 +12,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category
-import      Cubical.Categories.Constructions.Slice.Base as Slice
+import      Cubical.Categories.Instances.Slice.Base as Slice
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Isomorphism
@@ -20,7 +20,7 @@ import      Cubical.Categories.Morphism as Morphism
 
 
 
-module Cubical.Categories.Constructions.Elements where
+module Cubical.Categories.Instances.Elements where
 
 -- some issues
 -- * always need to specify objects during composition because can't infer isSet
diff --git a/Cubical/Categories/Constructions/EssentialImage.agda b/Cubical/Categories/Instances/EssentialImage.agda
similarity index 94%
rename from Cubical/Categories/Constructions/EssentialImage.agda
rename to Cubical/Categories/Instances/EssentialImage.agda
index cd4eaae49f..607253cf59 100644
--- a/Cubical/Categories/Constructions/EssentialImage.agda
+++ b/Cubical/Categories/Instances/EssentialImage.agda
@@ -4,7 +4,7 @@ The Essential Image of Functor
 
 -}
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.EssentialImage where
+module Cubical.Categories.Instances.EssentialImage where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
@@ -12,7 +12,7 @@ open import Cubical.HITs.PropositionalTruncation as PropTrunc
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
-open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Instances.FullSubcategory
 
 private
   variable
diff --git a/Cubical/Categories/Constructions/Free.agda b/Cubical/Categories/Instances/Free.agda
similarity index 93%
rename from Cubical/Categories/Constructions/Free.agda
rename to Cubical/Categories/Instances/Free.agda
index 73a5925bba..fbc8c21d2c 100644
--- a/Cubical/Categories/Constructions/Free.agda
+++ b/Cubical/Categories/Instances/Free.agda
@@ -1,7 +1,7 @@
 -- Free category over a directed graph/quiver
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.Free where
+module Cubical.Categories.Instances.Free where
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Data.Graph.Base
diff --git a/Cubical/Categories/Instances/Free/Category.agda b/Cubical/Categories/Instances/Free/Category.agda
new file mode 100644
index 0000000000..ca4254555e
--- /dev/null
+++ b/Cubical/Categories/Instances/Free/Category.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Instances.Free.Category where
+
+open import Cubical.Categories.Instances.Free.Category.Base public
diff --git a/Cubical/Categories/Constructions/Free/Category/Base.agda b/Cubical/Categories/Instances/Free/Category/Base.agda
similarity index 99%
rename from Cubical/Categories/Constructions/Free/Category/Base.agda
rename to Cubical/Categories/Instances/Free/Category/Base.agda
index ccd734ce7e..9abe4fe628 100644
--- a/Cubical/Categories/Constructions/Free/Category/Base.agda
+++ b/Cubical/Categories/Instances/Free/Category/Base.agda
@@ -5,7 +5,7 @@
 -- assumes the vertices of the input graph form a Set.
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.Free.Category.Base where
+module Cubical.Categories.Instances.Free.Category.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
diff --git a/Cubical/Categories/Constructions/Free/Category/Quiver.agda b/Cubical/Categories/Instances/Free/Category/Quiver.agda
similarity index 97%
rename from Cubical/Categories/Constructions/Free/Category/Quiver.agda
rename to Cubical/Categories/Instances/Free/Category/Quiver.agda
index cdb3801b20..982e724b60 100644
--- a/Cubical/Categories/Constructions/Free/Category/Quiver.agda
+++ b/Cubical/Categories/Instances/Free/Category/Quiver.agda
@@ -4,7 +4,7 @@
 -- which is better in some applications
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.Free.Category.Quiver where
+module Cubical.Categories.Instances.Free.Category.Quiver where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Path
@@ -19,7 +19,7 @@ open import Cubical.Data.Graph.Displayed as Graph hiding (Section)
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.NaturalTransformation
-open import Cubical.Categories.Constructions.BinProduct as BP
+open import Cubical.Categories.Instances.BinProduct as BP
 open import Cubical.Categories.UnderlyingGraph hiding (Interp)
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Instances.Path
diff --git a/Cubical/Categories/Constructions/Free/Functor.agda b/Cubical/Categories/Instances/Free/Functor.agda
similarity index 99%
rename from Cubical/Categories/Constructions/Free/Functor.agda
rename to Cubical/Categories/Instances/Free/Functor.agda
index 79023cdb1e..d18af9859e 100644
--- a/Cubical/Categories/Constructions/Free/Functor.agda
+++ b/Cubical/Categories/Instances/Free/Functor.agda
@@ -1,7 +1,7 @@
 -- Free functor between categories generated from two graphs and a
 -- function on nodes between them
 {-# OPTIONS --safe --lossy-unification #-}
-module Cubical.Categories.Constructions.Free.Functor where
+module Cubical.Categories.Instances.Free.Functor where
 
 open import Cubical.Foundations.Prelude hiding (J)
 open import Cubical.Foundations.Function renaming (_∘_ to _∘f_)
@@ -18,7 +18,7 @@ open import Cubical.Data.Graph.Base
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Constructions.Free.Category
+open import Cubical.Categories.Instances.Free.Category
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.NaturalTransformation.Base
 open import Cubical.Categories.UnderlyingGraph
diff --git a/Cubical/Categories/Constructions/FullSubcategory.agda b/Cubical/Categories/Instances/FullSubcategory.agda
similarity index 98%
rename from Cubical/Categories/Constructions/FullSubcategory.agda
rename to Cubical/Categories/Instances/FullSubcategory.agda
index f05b966ea7..46ad26c4d8 100644
--- a/Cubical/Categories/Constructions/FullSubcategory.agda
+++ b/Cubical/Categories/Instances/FullSubcategory.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.FullSubcategory where
+module Cubical.Categories.Instances.FullSubcategory where
 -- Full subcategory (not necessarily injective on objects)
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda
index 789994b00e..be669f81ef 100644
--- a/Cubical/Categories/Instances/Functors.agda
+++ b/Cubical/Categories/Instances/Functors.agda
@@ -18,7 +18,7 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Morphism
 open import Cubical.Categories.NaturalTransformation.Base
diff --git a/Cubical/Categories/Instances/Functors/Currying.agda b/Cubical/Categories/Instances/Functors/Currying.agda
index 9a34731e10..7d7b61bed8 100644
--- a/Cubical/Categories/Instances/Functors/Currying.agda
+++ b/Cubical/Categories/Instances/Functors/Currying.agda
@@ -7,7 +7,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Transport
 
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.NaturalTransformation.Base
 open import Cubical.Foundations.Function renaming (_∘_ to _∘→_)
diff --git a/Cubical/Categories/Constructions/Lift.agda b/Cubical/Categories/Instances/Lift.agda
similarity index 95%
rename from Cubical/Categories/Constructions/Lift.agda
rename to Cubical/Categories/Instances/Lift.agda
index 2ed45fa913..5ddd4bf9c5 100644
--- a/Cubical/Categories/Constructions/Lift.agda
+++ b/Cubical/Categories/Instances/Lift.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.Lift where
+module Cubical.Categories.Instances.Lift where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
diff --git a/Cubical/Categories/Constructions/Opposite.agda b/Cubical/Categories/Instances/Opposite.agda
similarity index 96%
rename from Cubical/Categories/Constructions/Opposite.agda
rename to Cubical/Categories/Instances/Opposite.agda
index 4afa7e971c..f1fbebe235 100644
--- a/Cubical/Categories/Constructions/Opposite.agda
+++ b/Cubical/Categories/Instances/Opposite.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.Opposite where
+module Cubical.Categories.Instances.Opposite where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
diff --git a/Cubical/Categories/Constructions/Power.agda b/Cubical/Categories/Instances/Power.agda
similarity index 88%
rename from Cubical/Categories/Constructions/Power.agda
rename to Cubical/Categories/Instances/Power.agda
index 6c0359bad8..e6c6d5a856 100644
--- a/Cubical/Categories/Constructions/Power.agda
+++ b/Cubical/Categories/Instances/Power.agda
@@ -1,10 +1,10 @@
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.Power where
+module Cubical.Categories.Instances.Power where
 
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Product
+open import Cubical.Categories.Instances.Product
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 
diff --git a/Cubical/Categories/Constructions/Product.agda b/Cubical/Categories/Instances/Product.agda
similarity index 96%
rename from Cubical/Categories/Constructions/Product.agda
rename to Cubical/Categories/Instances/Product.agda
index 45a3bb10b3..22ab925c12 100644
--- a/Cubical/Categories/Constructions/Product.agda
+++ b/Cubical/Categories/Instances/Product.agda
@@ -1,7 +1,7 @@
 -- Product of type-many categories
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.Product where
+module Cubical.Categories.Instances.Product where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
diff --git a/Cubical/Categories/Constructions/Quotient.agda b/Cubical/Categories/Instances/Quotient.agda
similarity index 98%
rename from Cubical/Categories/Constructions/Quotient.agda
rename to Cubical/Categories/Instances/Quotient.agda
index 7082bd9c0d..718933eb26 100644
--- a/Cubical/Categories/Constructions/Quotient.agda
+++ b/Cubical/Categories/Instances/Quotient.agda
@@ -1,7 +1,7 @@
 -- Quotient category
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.Quotient where
+module Cubical.Categories.Instances.Quotient where
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor.Base
diff --git a/Cubical/Categories/Constructions/Slice.agda b/Cubical/Categories/Instances/Slice.agda
similarity index 50%
rename from Cubical/Categories/Constructions/Slice.agda
rename to Cubical/Categories/Instances/Slice.agda
index bd82f7c307..48ea11cac8 100644
--- a/Cubical/Categories/Constructions/Slice.agda
+++ b/Cubical/Categories/Instances/Slice.agda
@@ -6,11 +6,11 @@ open import Cubical.Categories.Category
 
 open Category
 
-module Cubical.Categories.Constructions.Slice
+module Cubical.Categories.Instances.Slice
   {ℓ ℓ' : Level}
   (C : Category ℓ ℓ')
   (c : C .ob)
   where
 
-open import Cubical.Categories.Constructions.Slice.Base C c public
-open import Cubical.Categories.Constructions.Slice.Properties C c public
+open import Cubical.Categories.Instances.Slice.Base C c public
+open import Cubical.Categories.Instances.Slice.Properties C c public
diff --git a/Cubical/Categories/Constructions/Slice/Base.agda b/Cubical/Categories/Instances/Slice/Base.agda
similarity index 99%
rename from Cubical/Categories/Constructions/Slice/Base.agda
rename to Cubical/Categories/Instances/Slice/Base.agda
index c11652b7cf..49a8746d5c 100644
--- a/Cubical/Categories/Constructions/Slice/Base.agda
+++ b/Cubical/Categories/Instances/Slice/Base.agda
@@ -17,7 +17,7 @@ open Category
 open isUnivalent
 open Iso
 
-module Cubical.Categories.Constructions.Slice.Base {ℓ ℓ' : Level} (C : Category ℓ ℓ') (c : C .ob) where
+module Cubical.Categories.Instances.Slice.Base {ℓ ℓ' : Level} (C : Category ℓ ℓ') (c : C .ob) where
 
 -- just a helper to prevent redundency
 TypeC : Type (ℓ-suc (ℓ-max ℓ ℓ'))
diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Instances/Slice/Functor.agda
similarity index 98%
rename from Cubical/Categories/Constructions/Slice/Functor.agda
rename to Cubical/Categories/Instances/Slice/Functor.agda
index 424fa85052..491af68a86 100644
--- a/Cubical/Categories/Constructions/Slice/Functor.agda
+++ b/Cubical/Categories/Instances/Slice/Functor.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.Slice.Functor where
+module Cubical.Categories.Instances.Slice.Functor where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
@@ -9,7 +9,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Categories.Category
 open import Cubical.Categories.Category.Properties
 
-open import Cubical.Categories.Constructions.Slice.Base
+open import Cubical.Categories.Instances.Slice.Base
 
 open import Cubical.Categories.Limits.Pullback
 open import Cubical.Categories.Functor
diff --git a/Cubical/Categories/Constructions/Slice/Properties.agda b/Cubical/Categories/Instances/Slice/Properties.agda
similarity index 92%
rename from Cubical/Categories/Constructions/Slice/Properties.agda
rename to Cubical/Categories/Instances/Slice/Properties.agda
index 747bc1ec3c..377c249dc7 100644
--- a/Cubical/Categories/Constructions/Slice/Properties.agda
+++ b/Cubical/Categories/Instances/Slice/Properties.agda
@@ -8,8 +8,8 @@ open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation using (∣_∣₁)
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Slice.Base
-import Cubical.Categories.Constructions.Elements as Elements
+open import Cubical.Categories.Instances.Slice.Base
+import Cubical.Categories.Instances.Elements as Elements
 open import Cubical.Categories.Equivalence
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
@@ -17,7 +17,7 @@ open import Cubical.Categories.NaturalTransformation
 
 open Category
 
-module Cubical.Categories.Constructions.Slice.Properties
+module Cubical.Categories.Instances.Slice.Properties
   {ℓC ℓ'C : Level}
   (C : Category ℓC ℓ'C)
   (c : C .ob)
diff --git a/Cubical/Categories/Constructions/SubObject.agda b/Cubical/Categories/Instances/SubObject.agda
similarity index 96%
rename from Cubical/Categories/Constructions/SubObject.agda
rename to Cubical/Categories/Instances/SubObject.agda
index 2a5040bd49..ba6f2edf6c 100644
--- a/Cubical/Categories/Constructions/SubObject.agda
+++ b/Cubical/Categories/Instances/SubObject.agda
@@ -15,13 +15,13 @@ open import Cubical.Relation.Binary.Order.Preorder
 
 open Category
 
-module Cubical.Categories.Constructions.SubObject
+module Cubical.Categories.Instances.SubObject
   {ℓ ℓ' : Level}
   (C : Category ℓ ℓ')
   (c : C .ob)
   where
 
-open import Cubical.Categories.Constructions.Slice C c
+open import Cubical.Categories.Instances.Slice C c
 
 isSubObj : ℙ (SliceCat .ob)
 isSubObj (sliceob arr) = isMonic C arr , isPropIsMonic C arr
diff --git a/Cubical/Categories/Instances/TotalCategory.agda b/Cubical/Categories/Instances/TotalCategory.agda
new file mode 100644
index 0000000000..7a8905f01f
--- /dev/null
+++ b/Cubical/Categories/Instances/TotalCategory.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Instances.TotalCategory where
+
+open import Cubical.Categories.Instances.TotalCategory.Base public
+open import Cubical.Categories.Instances.TotalCategory.Properties public
diff --git a/Cubical/Categories/Constructions/TotalCategory/Base.agda b/Cubical/Categories/Instances/TotalCategory/Base.agda
similarity index 96%
rename from Cubical/Categories/Constructions/TotalCategory/Base.agda
rename to Cubical/Categories/Instances/TotalCategory/Base.agda
index 10a8aaf141..351ef5c169 100644
--- a/Cubical/Categories/Constructions/TotalCategory/Base.agda
+++ b/Cubical/Categories/Instances/TotalCategory/Base.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.TotalCategory.Base where
+module Cubical.Categories.Instances.TotalCategory.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
diff --git a/Cubical/Categories/Constructions/TotalCategory/Properties.agda b/Cubical/Categories/Instances/TotalCategory/Properties.agda
similarity index 95%
rename from Cubical/Categories/Constructions/TotalCategory/Properties.agda
rename to Cubical/Categories/Instances/TotalCategory/Properties.agda
index c00d1550e6..d1d293cffc 100644
--- a/Cubical/Categories/Constructions/TotalCategory/Properties.agda
+++ b/Cubical/Categories/Instances/TotalCategory/Properties.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.TotalCategory.Properties where
+module Cubical.Categories.Instances.TotalCategory.Properties where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
@@ -11,7 +11,7 @@ open import Cubical.Categories.Functor
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Displayed.Section.Base
-open import Cubical.Categories.Constructions.TotalCategory.Base
+open import Cubical.Categories.Instances.TotalCategory.Base
 open import Cubical.Categories.Displayed.Instances.Terminal.Base
 import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 
diff --git a/Cubical/Categories/Constructions/TwistedArrow.agda b/Cubical/Categories/Instances/TwistedArrow.agda
similarity index 83%
rename from Cubical/Categories/Constructions/TwistedArrow.agda
rename to Cubical/Categories/Instances/TwistedArrow.agda
index 7b8ccdfc9b..be16a29927 100644
--- a/Cubical/Categories/Constructions/TwistedArrow.agda
+++ b/Cubical/Categories/Instances/TwistedArrow.agda
@@ -1,17 +1,17 @@
 
 {-# OPTIONS --safe #-}
 
-module Cubical.Categories.Constructions.TwistedArrow where
+module Cubical.Categories.Instances.TwistedArrow where
 
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor.Base
-open import Cubical.Categories.Constructions.Elements
+open import Cubical.Categories.Instances.Elements
 open Covariant
 open import Cubical.Categories.Functors.HomFunctor
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 
 private
   variable
diff --git a/Cubical/Categories/Constructions/Vertical.agda b/Cubical/Categories/Instances/Vertical.agda
similarity index 86%
rename from Cubical/Categories/Constructions/Vertical.agda
rename to Cubical/Categories/Instances/Vertical.agda
index 5b189349cc..a7e36b126c 100644
--- a/Cubical/Categories/Constructions/Vertical.agda
+++ b/Cubical/Categories/Instances/Vertical.agda
@@ -3,13 +3,13 @@
   category. Also sometimes called the "fiber"
 -}
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Constructions.Vertical where
+module Cubical.Categories.Instances.Vertical where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Categories.Category
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Constructions.Reindex.Base
-open import Cubical.Categories.Constructions.DisplayOverTerminal
+open import Cubical.Categories.Instances.DisplayOverTerminal
 open import Cubical.Categories.Instances.Terminal
 
 private
diff --git a/Cubical/Categories/Monad/Base.agda b/Cubical/Categories/Monad/Base.agda
index 90190b2d4e..e6866bfc6f 100644
--- a/Cubical/Categories/Monad/Base.agda
+++ b/Cubical/Categories/Monad/Base.agda
@@ -7,7 +7,7 @@ open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)
 open import Cubical.Categories.NaturalTransformation.Base
 open import Cubical.Categories.NaturalTransformation.Properties
 open import Cubical.Categories.Functors.HomFunctor
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 
 private
   variable
diff --git a/Cubical/Categories/Monoidal/Base.agda b/Cubical/Categories/Monoidal/Base.agda
index 17904ffa8d..caae57a4b4 100644
--- a/Cubical/Categories/Monoidal/Base.agda
+++ b/Cubical/Categories/Monoidal/Base.agda
@@ -4,7 +4,7 @@
 module Cubical.Categories.Monoidal.Base where
 
 open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Morphism
 open import Cubical.Categories.NaturalTransformation.Base
diff --git a/Cubical/Categories/Presheaf/Morphism.agda b/Cubical/Categories/Presheaf/Morphism.agda
index 5a2adf17c9..9925df016d 100644
--- a/Cubical/Categories/Presheaf/Morphism.agda
+++ b/Cubical/Categories/Presheaf/Morphism.agda
@@ -6,8 +6,8 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Elements
-open import Cubical.Categories.Constructions.Lift
+open import Cubical.Categories.Instances.Elements
+open import Cubical.Categories.Instances.Lift
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Isomorphism
diff --git a/Cubical/Categories/Presheaf/NonPresheaf/Forget.agda b/Cubical/Categories/Presheaf/NonPresheaf/Forget.agda
index 9a0f03c5e6..d9b4d83190 100644
--- a/Cubical/Categories/Presheaf/NonPresheaf/Forget.agda
+++ b/Cubical/Categories/Presheaf/NonPresheaf/Forget.agda
@@ -6,7 +6,7 @@ open import Cubical.Foundations.HLevels
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Instances.Sets
-open import Cubical.Categories.Constructions.Product
+open import Cubical.Categories.Instances.Product
 open import Cubical.Categories.Functor
 open import Cubical.Categories.NaturalTransformation
 
diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda
index 1f79eb4c42..ca612ca4de 100644
--- a/Cubical/Categories/Presheaf/Properties.agda
+++ b/Cubical/Categories/Presheaf/Properties.agda
@@ -3,7 +3,7 @@
 module Cubical.Categories.Presheaf.Properties where
 
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
-open import Cubical.Categories.Constructions.Lift
+open import Cubical.Categories.Instances.Lift
 open import Cubical.Categories.NaturalTransformation
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Instances.Functors
@@ -19,8 +19,8 @@ open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation using (∣_∣₁)
 
 import Cubical.Categories.Morphism as Morphism
-import Cubical.Categories.Constructions.Slice as Slice
-import Cubical.Categories.Constructions.Elements as Elements
+import Cubical.Categories.Instances.Slice as Slice
+import Cubical.Categories.Instances.Elements as Elements
 import Cubical.Functions.Fibration as Fibration
 
 private
diff --git a/Cubical/Categories/Presheaf/Representable.agda b/Cubical/Categories/Presheaf/Representable.agda
index 350b05cbb6..aa2171d788 100644
--- a/Cubical/Categories/Presheaf/Representable.agda
+++ b/Cubical/Categories/Presheaf/Representable.agda
@@ -32,8 +32,8 @@ open import Cubical.HITs.PropositionalTruncation.Base
 open import Cubical.Reflection.RecordEquiv
 
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
-open import Cubical.Categories.Constructions.Elements
-open import Cubical.Categories.Constructions.Opposite
+open import Cubical.Categories.Instances.Elements
+open import Cubical.Categories.Instances.Opposite
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.Instances.Sets
diff --git a/Cubical/Categories/Profunctor/Base.agda b/Cubical/Categories/Profunctor/Base.agda
index 070391b37a..e2e9b8eadd 100644
--- a/Cubical/Categories/Profunctor/Base.agda
+++ b/Cubical/Categories/Profunctor/Base.agda
@@ -34,7 +34,7 @@ open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.NaturalTransformation
-open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.BinProduct
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Functors.HomFunctor
 
diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda
index 029948031f..5803195b5b 100644
--- a/Cubical/Categories/RezkCompletion/Construction.agda
+++ b/Cubical/Categories/RezkCompletion/Construction.agda
@@ -12,7 +12,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Equivalence.WeakEquivalence
-open import Cubical.Categories.Constructions.EssentialImage
+open import Cubical.Categories.Instances.EssentialImage
 open import Cubical.Categories.Presheaf.Base
 open import Cubical.Categories.Yoneda
 
diff --git a/Cubical/Categories/Site/Cover.agda b/Cubical/Categories/Site/Cover.agda
index ae6c7ea719..ee0d305fed 100644
--- a/Cubical/Categories/Site/Cover.agda
+++ b/Cubical/Categories/Site/Cover.agda
@@ -9,7 +9,7 @@ open import Cubical.Foundations.Structure
 open import Cubical.HITs.PropositionalTruncation
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Slice
+open import Cubical.Categories.Instances.Slice
 
 
 module _
diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
index 9d86d30c23..20660fe75a 100644
--- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
+++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda
@@ -23,7 +23,7 @@ open import Cubical.Categories.Category
 open import Cubical.Categories.Instances.CommRings
 open import Cubical.Categories.Site.Coverage
 open import Cubical.Categories.Site.Sheaf
-open import Cubical.Categories.Constructions.Slice
+open import Cubical.Categories.Instances.Slice
 open import Cubical.Categories.Yoneda
 
 open import Cubical.HITs.PropositionalTruncation as PT
diff --git a/Cubical/Categories/Site/Sheaf.agda b/Cubical/Categories/Site/Sheaf.agda
index d910db5d43..0a98f3e7da 100644
--- a/Cubical/Categories/Site/Sheaf.agda
+++ b/Cubical/Categories/Site/Sheaf.agda
@@ -19,7 +19,7 @@ open import Cubical.Categories.Site.Sieve
 open import Cubical.Categories.Site.Coverage
 open import Cubical.Categories.Presheaf
 open import Cubical.Categories.Functor
-open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Instances.FullSubcategory
 open import Cubical.Categories.Yoneda
 
 module _
diff --git a/Cubical/Categories/Site/Sheafification/UniversalProperty.agda b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
index 8fd6714028..48e66802dc 100644
--- a/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
+++ b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
@@ -16,7 +16,7 @@ open import Cubical.Categories.Presheaf
 open import Cubical.Categories.Functor
 open import Cubical.Categories.NaturalTransformation
 open import Cubical.Categories.Instances.Sets
-open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Instances.FullSubcategory
 
 open import Cubical.Categories.Site.Cover
 open import Cubical.Categories.Site.Coverage
diff --git a/Cubical/Categories/Yoneda.agda b/Cubical/Categories/Yoneda.agda
index f845c072b6..3fc082b19b 100644
--- a/Cubical/Categories/Yoneda.agda
+++ b/Cubical/Categories/Yoneda.agda
@@ -11,7 +11,7 @@ open import Cubical.Foundations.Equiv
 open import Cubical.HITs.PropositionalTruncation
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Lift
+open import Cubical.Categories.Instances.Lift
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.NaturalTransformation
diff --git a/Cubical/Tactics/CategorySolver/Reflection.agda b/Cubical/Tactics/CategorySolver/Reflection.agda
index e3ba3ac761..981921b909 100644
--- a/Cubical/Tactics/CategorySolver/Reflection.agda
+++ b/Cubical/Tactics/CategorySolver/Reflection.agda
@@ -18,7 +18,7 @@ open import Cubical.Tactics.CategorySolver.Solver
 open import Cubical.Tactics.Reflection
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Free.Category.Quiver as FC
+open import Cubical.Categories.Instances.Free.Category.Quiver as FC
 
 private
   variable
diff --git a/Cubical/Tactics/CategorySolver/Solver.agda b/Cubical/Tactics/CategorySolver/Solver.agda
index 0748789418..b7d14a2980 100644
--- a/Cubical/Tactics/CategorySolver/Solver.agda
+++ b/Cubical/Tactics/CategorySolver/Solver.agda
@@ -5,8 +5,8 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Data.Quiver.Base
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Free.Category.Quiver as FreeCat
-open import Cubical.Categories.Constructions.Power
+open import Cubical.Categories.Instances.Free.Category.Quiver as FreeCat
+open import Cubical.Categories.Instances.Power
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.UnderlyingGraph
diff --git a/Cubical/Tactics/FunctorSolver/Reflection.agda b/Cubical/Tactics/FunctorSolver/Reflection.agda
index 9faaca98e6..c892d94460 100644
--- a/Cubical/Tactics/FunctorSolver/Reflection.agda
+++ b/Cubical/Tactics/FunctorSolver/Reflection.agda
@@ -18,8 +18,8 @@ open import Cubical.Tactics.FunctorSolver.Solver
 open import Cubical.Tactics.Reflection
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Free.Category
-open import Cubical.Categories.Constructions.Free.Functor
+open import Cubical.Categories.Instances.Free.Category
+open import Cubical.Categories.Instances.Free.Functor
 open import Cubical.Categories.Functor
 
 private
diff --git a/Cubical/Tactics/FunctorSolver/Solver.agda b/Cubical/Tactics/FunctorSolver/Solver.agda
index aee48d7fe7..c569d88fa2 100644
--- a/Cubical/Tactics/FunctorSolver/Solver.agda
+++ b/Cubical/Tactics/FunctorSolver/Solver.agda
@@ -12,8 +12,8 @@ open import Cubical.Data.Equality renaming (refl to reflEq)
   hiding (_∙_; sym; transport)
 
 open import Cubical.Categories.Category
-open import Cubical.Categories.Constructions.Free.Functor
-open import Cubical.Categories.Constructions.Power
+open import Cubical.Categories.Instances.Free.Functor
+open import Cubical.Categories.Instances.Power
 open import Cubical.Categories.Functor renaming (Id to IdF)
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.NaturalTransformation

From 3c832d6ff8178f00d79d161ec00c29d4e0215e48 Mon Sep 17 00:00:00 2001
From: Andreas Nuyts <andreas.nuyts@kuleuven.be>
Date: Mon, 28 Oct 2024 12:18:23 +0100
Subject: [PATCH 2/3] Incorporate last merge.

---
 Cubical/Categories/Instances/Elements.agda                    | 2 +-
 .../{Constructions => Instances}/Elements/Properties.agda     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)
 rename Cubical/Categories/{Constructions => Instances}/Elements/Properties.agda (94%)

diff --git a/Cubical/Categories/Instances/Elements.agda b/Cubical/Categories/Instances/Elements.agda
index 74bd29500d..db953d9d6e 100644
--- a/Cubical/Categories/Instances/Elements.agda
+++ b/Cubical/Categories/Instances/Elements.agda
@@ -12,7 +12,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category
-import      Cubical.Categories.Constructions.Slice.Base as Slice
+import      Cubical.Categories.Instances.Slice.Base as Slice
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Isomorphism
diff --git a/Cubical/Categories/Constructions/Elements/Properties.agda b/Cubical/Categories/Instances/Elements/Properties.agda
similarity index 94%
rename from Cubical/Categories/Constructions/Elements/Properties.agda
rename to Cubical/Categories/Instances/Elements/Properties.agda
index 9506ff5a37..8de75475d2 100644
--- a/Cubical/Categories/Constructions/Elements/Properties.agda
+++ b/Cubical/Categories/Instances/Elements/Properties.agda
@@ -11,14 +11,14 @@ open import Cubical.Categories.NaturalTransformation
 open NatTrans
 open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.Instances.Sets
-open import Cubical.Categories.Constructions.Elements
+open import Cubical.Categories.Instances.Elements
 open Covariant
 
 open import Cubical.WildCat.Functor
 open import Cubical.WildCat.Instances.Categories
 open import Cubical.WildCat.Instances.NonWild
 
-module Cubical.Categories.Constructions.Elements.Properties where
+module Cubical.Categories.Instances.Elements.Properties where
 
 variable
   ℓC ℓC' ℓD ℓD' ℓS : Level

From e6d7fc6759fbcfaf5d693da41b312706de2d7efa Mon Sep 17 00:00:00 2001
From: Andreas Nuyts <andreas.nuyts@kuleuven.be>
Date: Mon, 28 Oct 2024 12:56:25 +0100
Subject: [PATCH 3/3] =?UTF-8?q?Recover=20ElementHom=E2=89=A1.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Cubical/Categories/Instances/Elements.agda | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Cubical/Categories/Instances/Elements.agda b/Cubical/Categories/Instances/Elements.agda
index db953d9d6e..96115bb961 100644
--- a/Cubical/Categories/Instances/Elements.agda
+++ b/Cubical/Categories/Instances/Elements.agda
@@ -80,6 +80,11 @@ module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
           p2 = snd ((∫ F) ._⋆_ f' ((∫ F) ._⋆_ {o1} {o2} {o3} g' h'))
     (∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _
 
+    ElementHom≡ : ∀ {ℓS} (F : Functor C (SET ℓS)) → {c,f c',f' : Element F}
+      → {χ1,ef1 χ2,ef2 : (∫ F) [ c,f , c',f' ]} → (fst χ1,ef1 ≡ fst χ2,ef2) → (χ1,ef1 ≡ χ2,ef2)
+    ElementHom≡ F {c1 , f1} {c2 , f2} {χ1 , ef1} {χ2 , ef2} eχ = cong₂ _,_ eχ
+      (fst (isOfHLevelPathP' 0 (snd (F ⟅ c2 ⟆) _ _) ef1 ef2))
+
     ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C
     F-ob (ForgetElements F) = fst
     F-hom (ForgetElements F) = fst