From 7d6db415a1a8277df7841675aacf300e880fa4ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 8 Jan 2018 22:48:59 +0100 Subject: [PATCH] Move modules around again. Henceforth all modules shall be placed under the top-level module-name `Cat` (at least until I've come up with a better name) Also fixes an issue caused by https://github.com/Saizan/cubical-demo/ redefining Sigma. --- src/{Category => Cat}/Categories/Cat.agda | 0 src/{Category => Cat/Categories}/Rel.agda | 15 +++++++++------ src/{Category => Cat/Categories}/Sets.agda | 0 src/{ => Cat}/Category.agda | 2 +- src/{ => Cat}/Category/Bij.agda | 0 src/{ => Cat}/Category/Free.agda | 0 src/{ => Cat}/Category/Pathy.agda | 0 src/{Category => Cat}/Cubical.agda | 5 +++-- 8 files changed, 13 insertions(+), 9 deletions(-) rename src/{Category => Cat}/Categories/Cat.agda (100%) rename src/{Category => Cat/Categories}/Rel.agda (94%) rename src/{Category => Cat/Categories}/Sets.agda (100%) rename src/{ => Cat}/Category.agda (99%) rename src/{ => Cat}/Category/Bij.agda (100%) rename src/{ => Cat}/Category/Free.agda (100%) rename src/{ => Cat}/Category/Pathy.agda (100%) rename src/{Category => Cat}/Cubical.agda (95%) diff --git a/src/Category/Categories/Cat.agda b/src/Cat/Categories/Cat.agda similarity index 100% rename from src/Category/Categories/Cat.agda rename to src/Cat/Categories/Cat.agda diff --git a/src/Category/Rel.agda b/src/Cat/Categories/Rel.agda similarity index 94% rename from src/Category/Rel.agda rename to src/Cat/Categories/Rel.agda index e9bbdc4..32e07f4 100644 --- a/src/Category/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -1,11 +1,14 @@ {-# OPTIONS --cubical #-} -module Category.Rel where +module Cat.Categories.Rel where -open import Data.Product open import Cubical.PathPrelude open import Cubical.GradLemma open import Agda.Primitive -open import Category +open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) +open import Function +import Cubical.FromStdLib + +open import Cat.Category -- Subsets are predicates over some type. Subset : {ℓ : Level} → ( A : Set ℓ ) → Set (ℓ ⊔ lsuc lzero) @@ -72,7 +75,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≃ (a , b) ∈ S - equi = backwards , isequiv + equi = backwards Cubical.FromStdLib., isequiv ident-l : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≡ (a , b) ∈ S @@ -106,7 +109,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≃ ab ∈ S - equi = backwards , isequiv + equi = backwards Cubical.FromStdLib., isequiv ident-r : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≡ ab ∈ S @@ -144,7 +147,7 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) - equi = fwd , isequiv + equi = fwd Cubical.FromStdLib., isequiv -- assocc : Q + (R + S) ≡ (Q + R) + S is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) diff --git a/src/Category/Sets.agda b/src/Cat/Categories/Sets.agda similarity index 100% rename from src/Category/Sets.agda rename to src/Cat/Categories/Sets.agda diff --git a/src/Category.agda b/src/Cat/Category.agda similarity index 99% rename from src/Category.agda rename to src/Cat/Category.agda index 568f93b..c3ce34f 100644 --- a/src/Category.agda +++ b/src/Cat/Category.agda @@ -1,6 +1,6 @@ {-# OPTIONS --cubical #-} -module Category where +module Cat.Category where open import Agda.Primitive open import Data.Unit.Base diff --git a/src/Category/Bij.agda b/src/Cat/Category/Bij.agda similarity index 100% rename from src/Category/Bij.agda rename to src/Cat/Category/Bij.agda diff --git a/src/Category/Free.agda b/src/Cat/Category/Free.agda similarity index 100% rename from src/Category/Free.agda rename to src/Cat/Category/Free.agda diff --git a/src/Category/Pathy.agda b/src/Cat/Category/Pathy.agda similarity index 100% rename from src/Category/Pathy.agda rename to src/Cat/Category/Pathy.agda diff --git a/src/Category/Cubical.agda b/src/Cat/Cubical.agda similarity index 95% rename from src/Category/Cubical.agda rename to src/Cat/Cubical.agda index 22709be..cba1c41 100644 --- a/src/Category/Cubical.agda +++ b/src/Cat/Cubical.agda @@ -1,13 +1,14 @@ -module Category.Cubical where +module Cat.Cubical where open import Agda.Primitive -open import Category open import Data.Bool open import Data.Product open import Data.Sum open import Data.Unit open import Data.Empty +open import Cat.Category + module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where -- Σ is the "namespace" ℓo = (lsuc lzero ⊔ ℓ)