Clean up: Remove Foundation/Everything and outdated stuff

.gitignore

@@ -3,6 +3,4 @@
 \.*#*
 \#*
 Cubical/*/Everything.agda
-!Cubical/Core/Everything.agda
-!Cubical/Foundations/Everything.agda
 !Cubical/Codata/Everything.agda

Cubical/Codata/Conat.agda

@@ -1,7 +1,5 @@
-{-# OPTIONS --guardedness #-}
-
+{-# OPTIONS --safe --guardedness #-}
 module Cubical.Codata.Conat where
 
 open import Cubical.Codata.Conat.Base public
-
 open import Cubical.Codata.Conat.Properties public

Cubical/Codata/Conat/Base.agda

@@ -21,11 +21,11 @@ of Sized Types.
 {-# OPTIONS --safe --guardedness #-}
 module Cubical.Codata.Conat.Base where
 
+open import Cubical.Foundations.Prelude
+
 open import Cubical.Data.Unit
 open import Cubical.Data.Sum
 
-open import Cubical.Core.Everything
-
 record Conat : Type₀
 Conat′ = Unit ⊎ Conat
 record Conat where

Cubical/Codata/Conat/Properties.agda

@@ -33,8 +33,6 @@ open import Cubical.Data.Bool
 import Cubical.Data.Nat as Nat
 import Cubical.Data.Nat.Order.Recursive as Nat
 
-open import Cubical.Core.Everything
-
 open import Cubical.Functions.Embedding
 
 open import Cubical.Foundations.Prelude

Cubical/Codata/Everything.agda

@@ -1,33 +1,15 @@
-{-# OPTIONS --guardedness #-}
-
+{-# OPTIONS --safe --guardedness #-}
 module Cubical.Codata.Everything where
 
-open import Cubical.Codata.EverythingSafe public
-
---- Modules making assumptions that might be incompatible with other
---  flags or make use of potentially unsafe features.
-
--- Assumes --guardedness
-open import Cubical.Codata.Stream public
-
-open import Cubical.Codata.Conat public
-open import Cubical.Codata.Conat.Bounded
-
-open import Cubical.Codata.M public
-
--- Also uses {-# TERMINATING #-}.
-open import Cubical.Codata.M.Bisimilarity public
-
-{-
--- Alternative M type implemetation, based on
--- https://arxiv.org/pdf/1504.02949.pdf
--- "Non-wellfounded trees in Homotopy Type Theory"
--- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
--}
-
-open import Cubical.Codata.M.AsLimit.M
-open import Cubical.Codata.M.AsLimit.Coalg
-open import Cubical.Codata.M.AsLimit.helper
-open import Cubical.Codata.M.AsLimit.Container
-open import Cubical.Codata.M.AsLimit.itree
-open import Cubical.Codata.M.AsLimit.stream
+import Cubical.Codata.Conat
+import Cubical.Codata.Conat.Bounded
+import Cubical.Codata.M.Coalg
+import Cubical.Codata.M.Coalg.Base
+import Cubical.Codata.M.Container
+import Cubical.Codata.M.M
+import Cubical.Codata.M.M.Base
+import Cubical.Codata.M.M.Properties
+import Cubical.Codata.M.helper
+import Cubical.Codata.M.itree
+import Cubical.Codata.M.stream
+import Cubical.Codata.Stream

Cubical/Codata/M/Coalg.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --guardedness --safe #-}
+
+module Cubical.Codata.M.Coalg where
+
+open import Cubical.Codata.M.Coalg.Base public

Cubical/Codata/M/AsLimit/Coalg/Base.agda → Cubical/Codata/M/Coalg/Base.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS --guardedness --safe #-}
 
-module Cubical.Codata.M.AsLimit.Coalg.Base where
+module Cubical.Codata.M.Coalg.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function using ( _∘_ )
@@ -15,8 +15,8 @@ open import Cubical.Data.Nat
 open import Cubical.Data.Prod
 open import Cubical.Data.Sigma
 
-open import Cubical.Codata.M.AsLimit.Container
-open import Cubical.Codata.M.AsLimit.helper
+open import Cubical.Codata.M.Container
+open import Cubical.Codata.M.helper
 
 -------------------------------
 -- Definition of a Coalgebra --

Cubical/Codata/M/AsLimit/Container.agda → Cubical/Codata/M/Container.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS --guardedness --safe #-}
 
-module Cubical.Codata.M.AsLimit.Container where
+module Cubical.Codata.M.Container where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv using (_≃_)
@@ -20,7 +20,7 @@ open import Cubical.Data.Sum
 
 open import Cubical.Foundations.Structure
 
-open import Cubical.Codata.M.AsLimit.helper
+open import Cubical.Codata.M.helper
 
 -------------------------------------
 -- Container and Container Functor --