move Categories from gist to deprecated

Author: martinescardo

source/Lifting/IdentityViaSIP.lagda

@@ -23,7 +23,7 @@ open import UF.EquivalenceExamples
 open import UF.FunExt
 open import UF.Univalence
 open import UF.UA-FunExt
-open import UF.StructureIdentityPrinciple
+open import deprecated.StructureIdentityPrinciple
 
 open import Lifting.Construction 𝓣
 

source/Slice/IdentityViaSIP.lagda

@@ -20,7 +20,7 @@ open import UF.EquivalenceExamples
 open import UF.FunExt
 open import UF.Univalence
 open import UF.UA-FunExt
-open import UF.StructureIdentityPrinciple
+open import deprecated.StructureIdentityPrinciple
 
 open import Slice.Construction 𝓣
 

source/UF/index.lagda

@@ -69,7 +69,6 @@ import UF.Singleton-Properties       -- by [2]
 import UF.Size
 import UF.Size-TruncatedConnected    -- by [2]
 import UF.SmallnessProperties
-import UF.StructureIdentityPrinciple -- Obsolete but keep. Use UF.SIP instead
 import UF.Subsingletons
 import UF.Subsingletons-FunExt
 import UF.Subsingletons-Properties

…urce/UF/StructureIdentityPrinciple.lagda …recated/StructureIdentityPrinciple.lagdasource/UF/StructureIdentityPrinciple.lagda renamed to source/deprecated/StructureIdentityPrinciple.lagda source/UF/StructureIdentityPrinciple.lagda renamed to source/deprecated/StructureIdentityPrinciple.lagda

@@ -42,7 +42,7 @@ open import UF.Sets-Properties
 open import UF.Univalence
 open import UF.Yoneda
 
-module UF.StructureIdentityPrinciple where
+module deprecated.StructureIdentityPrinciple where
 
 \end{code}
 

source/deprecated/index.lagda

@@ -0,0 +1,10 @@
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+module deprecated.index where
+
+import deprecated.Categories.index
+import deprecated.StructureIdentityPrinciple    -- Use UF.SIP instead
+
+\end{code}