Skip to content

Commit 78c5277

Browse files
martinescardomartinescardo
committed
move Categories from gist to deprecated
1 parent 59309af commit 78c5277

File tree

12 files changed

+33
-33
lines changed

12 files changed

+33
-33
lines changed

‎source/Duploids/DeductiveSystem.lagda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ open import MLTT.Spartan
2222
open import UF.Subsingletons
2323
open import UF.Subsingletons-FunExt
2424

25-
open import gist.Categories.Category fe
25+
open import deprecated.Categories.Category fe
2626

2727
deductive-system-structure : (𝓤 𝓥 : Universe) → (𝓤 ⊔ 𝓥)⁺ ̇
2828
deductive-system-structure 𝓤 𝓥 = category-structure 𝓤 𝓥

‎source/Duploids/Depolarization.lagda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ open import UF.PropTrunc
2323
open import UF.Subsingletons
2424
open import UF.Subsingletons-FunExt
2525

26-
open import gist.Categories.Category fe
26+
open import deprecated.Categories.Category fe
2727
open import Duploids.DeductiveSystem fe
2828

2929
module _ (𝓓 : deductive-system 𝓤 𝓥) where

‎source/Duploids/Duploid.lagda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,8 @@ open import MLTT.Spartan
4343
open import UF.Base
4444
open import UF.Subsingletons
4545

46-
open import gist.Categories.Category fe
47-
open import gist.Categories.Functor fe
46+
open import deprecated.Categories.Category fe
47+
open import deprecated.Categories.Functor fe
4848
open import Duploids.DeductiveSystem fe
4949
open import Duploids.Preduploid fe pt
5050

‎source/Duploids/Preduploid.lagda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ open import UF.Subsingletons
2626
open import UF.Subsingletons-FunExt
2727
open import UF.Subsingletons-Properties
2828

29-
open import gist.Categories.Category fe
29+
open import deprecated.Categories.Category fe
3030
open import Duploids.DeductiveSystem fe
3131

3232
module _ (𝓓 : deductive-system 𝓤 𝓥) where

source/gist/Categories/Adjunction.lagda renamed to source/deprecated/Categories/Adjunction.lagda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@ Jon Sterling, started 18th Dec 2022
66

77
open import UF.FunExt
88

9-
module gist.Categories.Adjunction (fe : Fun-Ext) where
9+
module deprecated.Categories.Adjunction (fe : Fun-Ext) where
1010

1111
open import MLTT.Spartan
1212
open import UF.Subsingletons
1313

14-
open import gist.Categories.Category fe
15-
open import gist.Categories.Functor fe
16-
open import gist.Categories.NaturalTransformation fe
14+
open import deprecated.Categories.Category fe
15+
open import deprecated.Categories.Functor fe
16+
open import deprecated.Categories.NaturalTransformation fe
1717

1818
module adjunction-of-precategories (𝓒 : precategory 𝓤 𝓥) (𝓓 : precategory 𝓤' 𝓥') where
1919
open functor-of-precategories

source/gist/Categories/Category.lagda renamed to source/deprecated/Categories/Category.lagda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Jon Sterling, started 16th Dec 2022
66

77
open import UF.FunExt
88

9-
module gist.Categories.Category (fe : Fun-Ext) where
9+
module deprecated.Categories.Category (fe : Fun-Ext) where
1010

1111
open import MLTT.Spartan
1212
open import UF.Base

source/gist/Categories/Functor.lagda renamed to source/deprecated/Categories/Functor.lagda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@ Jon Sterling, started 16th Dec 2022
66

77
open import UF.FunExt
88

9-
module gist.Categories.Functor (fe : Fun-Ext) where
9+
module deprecated.Categories.Functor (fe : Fun-Ext) where
1010

1111
open import MLTT.Spartan
1212
open import UF.Equiv
1313
open import UF.Subsingletons
1414
open import UF.Subsingletons-FunExt
1515

16-
open import gist.Categories.Category fe
16+
open import deprecated.Categories.Category fe
1717

1818
module functor-of-precategories (𝓒 : precategory 𝓤 𝓥) (𝓓 : precategory 𝓤' 𝓥') where
1919
private

source/gist/Categories/NaturalTransformation.lagda renamed to source/deprecated/Categories/NaturalTransformation.lagda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ Jon Sterling, started 16th Dec 2022
66

77
open import UF.FunExt
88

9-
module gist.Categories.NaturalTransformation (fe : Fun-Ext) where
9+
module deprecated.Categories.NaturalTransformation (fe : Fun-Ext) where
1010

11-
open import gist.Categories.Category fe
12-
open import gist.Categories.Functor fe
11+
open import deprecated.Categories.Category fe
12+
open import deprecated.Categories.Functor fe
1313
open import MLTT.Spartan
1414
open import UF.Base
1515
open import UF.Equiv

‎source/deprecated/Categories/index.lagda‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
Jon Sterling, 16 Dec 2022
2+
3+
This is a nascent development of some basic 1-category theory from the univalent
4+
point of view.
5+
6+
\begin{code}
7+
8+
{-# OPTIONS --safe --without-K #-}
9+
10+
module deprecated.Categories.index where
11+
12+
import deprecated.Categories.Category
13+
import deprecated.Categories.Functor
14+
import deprecated.Categories.NaturalTransformation
15+
import deprecated.Categories.Adjunction
16+
17+
\end{code}

‎source/gist/Categories/index.lagda‎

Lines changed: 0 additions & 17 deletions
This file was deleted.

0 commit comments

Comments
 (0)