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.
This commit is contained in:
Frederik Hanghøj Iversen 2018-01-08 22:48:59 +01:00
parent e3d2c0d39e
commit 7d6db415a1
8 changed files with 13 additions and 9 deletions

View file

@ -1,11 +1,14 @@
{-# OPTIONS --cubical #-} {-# OPTIONS --cubical #-}
module Category.Rel where module Cat.Categories.Rel where
open import Data.Product
open import Cubical.PathPrelude open import Cubical.PathPrelude
open import Cubical.GradLemma open import Cubical.GradLemma
open import Agda.Primitive 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. -- Subsets are predicates over some type.
Subset : { : Level} ( A : Set ) Set ( lsuc lzero) 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) equi : (Σ[ a' A ] (a , a') Diag A × (a' , b) S)
(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) ident-l : (Σ[ a' A ] (a , a') Diag A × (a' , b) S)
(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) equi : (Σ[ b' B ] (a , b') S × (b' , b) Diag B)
ab S ab S
equi = backwards , isequiv equi = backwards Cubical.FromStdLib., isequiv
ident-r : (Σ[ b' B ] (a , b') S × (b' , b) Diag B) ident-r : (Σ[ b' B ] (a , b') S × (b' , b) Diag B)
ab S 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) 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)) (Σ[ 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 -- assocc : Q + (R + S) ≡ (Q + R) + S
is-assoc : (Σ[ c C ] (Σ[ b B ] (a , b) S × (b , c) R) × (c , d) Q) is-assoc : (Σ[ c C ] (Σ[ b B ] (a , b) S × (b , c) R) × (c , d) Q)

View file

@ -1,6 +1,6 @@
{-# OPTIONS --cubical #-} {-# OPTIONS --cubical #-}
module Category where module Cat.Category where
open import Agda.Primitive open import Agda.Primitive
open import Data.Unit.Base open import Data.Unit.Base

View file

@ -1,13 +1,14 @@
module Category.Cubical where module Cat.Cubical where
open import Agda.Primitive open import Agda.Primitive
open import Category
open import Data.Bool open import Data.Bool
open import Data.Product open import Data.Product
open import Data.Sum open import Data.Sum
open import Data.Unit open import Data.Unit
open import Data.Empty open import Data.Empty
open import Cat.Category
module _ { ' : Level} (Ns : Set ) where module _ { ' : Level} (Ns : Set ) where
-- Σ is the "namespace" -- Σ is the "namespace"
o = (lsuc lzero ) o = (lsuc lzero )