Rename Categories.(Displayed.)Constructions to Instances (#1296)

* rename Categories.Constructions to Categories.Instances

* rename Categories.Displayed.Constructions to Categories.Displayed.Instances

Author: maxsnew

Cubical/Categories/Additive/Quotient.agda

@@ -6,7 +6,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 ⟦_⟧)

Cubical/Categories/Constructions/Free/Category.agda

@@ -5,7 +5,7 @@ open import Cubical.Data.Sigma
 
 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.Morphism
 
 open import Cubical.Categories.Dagger.Base

Cubical/Categories/Constructions/Slice.agda

@@ -6,7 +6,7 @@ open import Cubical.Data.Sigma
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.NaturalTransformation
-open import Cubical.Categories.Constructions.FullSubcategory
+open import Cubical.Categories.Instances.FullSubcategory
 open import Cubical.Categories.Instances.Functors
 
 open import Cubical.Categories.Dagger.Base

Cubical/Categories/Constructions/TotalCategory.agda

@@ -4,7 +4,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

Cubical/Categories/Dagger/Instances/BinProduct.agda

@@ -14,7 +14,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
 

Cubical/Categories/Dagger/Instances/Functors.agda

@@ -1,5 +1,5 @@
 --
-module Cubical.Categories.Displayed.Constructions.LeftAdjointToReindex where
+module Cubical.Categories.Displayed.Instances.LeftAdjointToReindex where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Path
@@ -12,8 +12,8 @@ open import Cubical.Categories.Instances.Terminal
 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.Displayed.Instances.Weaken.Base
+open import Cubical.Categories.Instances.TotalCategory
 
 private
   variable