Pour Cubical.Categories.Constructions into Instances #765

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 ⟦_⟧)

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

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
 

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

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
 

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

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

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

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

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

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

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

Cubical/Categories/Constructions/BinProduct.agda → 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

Cubical/Categories/Constructions/DisplayOverTerminal.agda → 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

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

Cubical/Categories/Constructions/Elements.agda → Cubical/Categories/Instances/Elements.agda

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

Cubical/Categories/Constructions/Elements/Properties.agda → 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

Cubical/Categories/Constructions/EssentialImage.agda → Cubical/Categories/Instances/EssentialImage.agda

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

Cubical/Categories/Constructions/Free.agda → 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

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

Cubical/Categories/Constructions/Free/Category/Base.agda → 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

Cubical/Categories/Constructions/Free/Category/Quiver.agda → 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

Cubical/Categories/Constructions/Free/Functor.agda → 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

Cubical/Categories/Constructions/FullSubcategory.agda → 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

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

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 _∘→_)

Cubical/Categories/Constructions/Lift.agda → 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

Cubical/Categories/Constructions/Opposite.agda → 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

Cubical/Categories/Constructions/Power.agda → 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
 

Cubical/Categories/Constructions/Product.agda → 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

Cubical/Categories/Constructions/Quotient.agda → 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

Cubical/Categories/Constructions/Slice.agda → 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

Cubical/Categories/Constructions/Slice/Base.agda → 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 ℓ ℓ'))

Cubical/Categories/Constructions/Slice/Functor.agda → 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

Cubical/Categories/Constructions/Slice/Properties.agda → Cubical/Categories/Instances/Slice/Properties.agda

@@ -8,16 +8,16 @@ 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
 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)