From 22410e5cb1609c63a66ce140dcbcfed1da97a85c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Mon, 13 May 2024 15:22:48 +0200
Subject: [PATCH 01/11] Clean Codata folder and make it --safe

---
 Cubical/Codata/Conat.agda          |   4 +-
 Cubical/Codata/Everything.agda     |  33 -------
 Cubical/Codata/EverythingSafe.agda |   2 -
 Cubical/Codata/M/AsLimit/M.agda    |   7 +-
 Cubical/Codata/M/Bisimilarity.agda | 153 -----------------------------
 Cubical/Codata/Stream.agda         |   2 +-
 GNUmakefile                        |   6 +-
 7 files changed, 11 insertions(+), 196 deletions(-)
 delete mode 100644 Cubical/Codata/Everything.agda
 delete mode 100644 Cubical/Codata/EverythingSafe.agda
 delete mode 100644 Cubical/Codata/M/Bisimilarity.agda

diff --git a/Cubical/Codata/Conat.agda b/Cubical/Codata/Conat.agda
index f35a316c92..b695c1d03b 100644
--- a/Cubical/Codata/Conat.agda
+++ b/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
diff --git a/Cubical/Codata/Everything.agda b/Cubical/Codata/Everything.agda
deleted file mode 100644
index 52c952d486..0000000000
--- a/Cubical/Codata/Everything.agda
+++ /dev/null
@@ -1,33 +0,0 @@
-{-# OPTIONS --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
diff --git a/Cubical/Codata/EverythingSafe.agda b/Cubical/Codata/EverythingSafe.agda
deleted file mode 100644
index 0f7a364688..0000000000
--- a/Cubical/Codata/EverythingSafe.agda
+++ /dev/null
@@ -1,2 +0,0 @@
-{-# OPTIONS --safe #-}
-module Cubical.Codata.EverythingSafe where
diff --git a/Cubical/Codata/M/AsLimit/M.agda b/Cubical/Codata/M/AsLimit/M.agda
index 22c3b9e654..238b294064 100644
--- a/Cubical/Codata/M/AsLimit/M.agda
+++ b/Cubical/Codata/M/AsLimit/M.agda
@@ -1,5 +1,10 @@
+{-
+-- 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
+-}
 {-# OPTIONS --guardedness --safe #-}
-
 module Cubical.Codata.M.AsLimit.M where
 
 open import Cubical.Codata.M.AsLimit.M.Base public
diff --git a/Cubical/Codata/M/Bisimilarity.agda b/Cubical/Codata/M/Bisimilarity.agda
deleted file mode 100644
index 602d2f8989..0000000000
--- a/Cubical/Codata/M/Bisimilarity.agda
+++ /dev/null
@@ -1,153 +0,0 @@
-{-# OPTIONS --postfix-projections --guardedness #-}
-module Cubical.Codata.M.Bisimilarity where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Equiv.Fiberwise
-open import Cubical.Foundations.Transport
-open import Cubical.Foundations.HLevels
-
-
-open import Cubical.Codata.M
-
-
-open Helpers using (J')
-
--- Bisimilarity as a coinductive record type.
-record _≈_ {X : Type₀} {C : IxCont X} {x : X} (a b : M C x) : Type₀ where
-  coinductive
-  constructor _,_
-  field
-    head≈ : a .head ≡ b .head
-    tails≈ : ∀ y → (pa : C .snd x (a .head) y) (pb : C .snd x (b .head) y)
-             → (\ i → C .snd x (head≈ i) y) [ pa ≡ pb ]
-             → a .tails y pa ≈ b .tails y pb
-
-open _≈_ public
-
-
-
-module _ {X : Type₀} {C : IxCont X} where
-
-  -- Here we show that `a ≡ b` and `a ≈ b` are equivalent.
-  --
-  -- A direct construction of an isomorphism, like we do for streams,
-  -- would be complicated by the type dependencies between the fields
-  -- of `M C x` and even more so between the fields of the bisimilarity relation itself.
-  --
-  -- Instead we rely on theorem 4.7.7 of the HoTT book (fiberwise equivalences) to show that `misib` is an equivalence.
-
-  misib : {x : X} (a b : M C x) → a ≡ b → a ≈ b
-  misib a b eq .head≈ i          = eq i .head
-  misib a b eq .tails≈ y pa pb q = misib (a .tails y pa) (b .tails y pb) (\ i → eq i .tails y (q i))
-
-
-  -- With `a` fixed, `misib` is a fiberwise transformation between (a ≡_) and (a ≈_).
-  --
-  -- We show that the induced map on the total spaces is an
-  -- equivalence because it is a map of contractible types.
-  --
-  -- The domain is the HoTT singleton type, so contractible, while the
-  -- codomain is shown to be contractible by `contr-T` below.
-
-  T : ∀ {x} → M C x → Type _
-  T a = Σ (M C _) \ b → a ≈ b
-
-  private
-    lemma : ∀ {A} (B : Type₀) (P : A ≡ B) (pa : P i0) (pb : P i1) (peq : PathP (\ i → P i) pa pb)
-          → PathP (\ i → PathP (\ j → P j) (transp (\ k → P (~ k ∧ i)) (~ i) (peq i)) pb)
-                  peq
-                  (\ j → transp (\ k → P (~ k ∨ j)) j pb)
-    lemma {A} = J' _ \ pa → J' _ \ { i j → transp (\ _ → A) (~ i ∨ j) pa }
-
-
-
-  -- We predefine `u'` so that Agda will agree that `contr-T-fst` is productive.
-  private
-    module Tails x a φ (u : Partial φ (T {x} a)) y (p : C .snd x (hcomp (λ i .o → u o .snd .head≈ i) (a .head)) y) where
-      q = transp (\ i → C .snd x (hfill (\ i o → u o .snd .head≈ i) (inS (a .head)) (~ i)) y) i0 p
-      a' = a .tails y q
-      u' : Partial φ (T a')
-      u' (φ = i1) = u 1=1 .fst .tails y p
-                  , u 1=1 .snd .tails≈ y q p \ j → transp (\ i → C .snd x (u 1=1 .snd .head≈ (~ i ∨ j)) y) j p
-
-
-  contr-T-fst : ∀ x a φ → Partial φ (T {x} a) → M C x
-  contr-T-fst x a φ u .head      = hcomp (\ i o → u o .snd .head≈ i) (a .head)
-  contr-T-fst x a φ u .tails y p = contr-T-fst y a' φ u'
-    where
-      open Tails x a φ u y p
-
-  -- `contr-T-snd` is productive as the corecursive call appears as
-  -- the main argument of transport, which is guardedness-preserving.
-  {-# TERMINATING #-}
-  contr-T-snd : ∀ x a φ → (u : Partial φ (T {x} a)) → a ≈ contr-T-fst x a φ u
-  contr-T-snd x a φ u .head≈ i = hfill (λ { i (φ = i1) → u 1=1 .snd .head≈ i }) (inS (a .head)) i
-  contr-T-snd x a φ u .tails≈ y pa pb peq =
-    let r = contr-T-snd y (a .tails y pa) φ (\ { (φ = i1) → u 1=1 .fst .tails y pb , u 1=1 .snd .tails≈ y pa pb peq }) in
-      transport (\ i → a .tails y pa
-                ≈ contr-T-fst y (a .tails y (sym (fromPathP (\ i → peq (~ i))) i)) φ
-                  (\ { (φ = i1) → u 1=1 .fst .tails y pb , u 1=1 .snd .tails≈ y
-                                  ((fromPathP (\ i → peq (~ i))) (~ i)) pb
-                                  \ j → lemma _ (λ h → C .snd x (u _ .snd .head≈ h) y) pa pb peq i j })) r
-
-  contr-T : ∀ x a φ → Partial φ (T {x} a) → T a
-  contr-T x a φ u .fst = contr-T-fst x a φ u
-  contr-T x a φ u .snd = contr-T-snd x a φ u
-
-
-  contr-T-φ-fst : ∀ x a → (u : Partial i1 (T {x} a)) → contr-T x a i1 u .fst ≡ u 1=1 .fst
-  contr-T-φ-fst x a u i .head = u 1=1 .fst .head
-  contr-T-φ-fst x a u i .tails y p
-   = let
-        q = (transp (\ i → C .snd x (hfill (\ i o → u o .snd .head≈ i) (inS (a .head)) (~ i)) y) i0 p)
-      in contr-T-φ-fst y (a .tails y q)
-                       (\ o → u o .fst .tails y p
-                            , u o .snd .tails≈ y q p \ j → transp (\ i → C .snd x (u 1=1 .snd .head≈ (~ i ∨ j)) y) j p)
-                       i
-
-  -- `contr-T-φ-snd` is productive as the corecursive call appears as
-  -- the main argument of transport, which is guardedness-preserving (even for paths of a coinductive type).
-  {-# TERMINATING #-}
-  contr-T-φ-snd : ∀ x a → (u : Partial i1 (T {x} a)) → (\ i → a ≈ contr-T-φ-fst x a u i) [ contr-T x a i1 u .snd ≡ u 1=1 .snd ]
-  contr-T-φ-snd x a u i .head≈ = u _ .snd .head≈
-  contr-T-φ-snd x a u i .tails≈ y pa pb peq = let
-    eqh = u 1=1 .snd .head≈
-    r = contr-T-φ-snd y (a .tails y pa) (\ o → u o .fst .tails y pb , u 1=1 .snd .tails≈ y pa pb peq)
-    F : I → Type _
-    F k = a .tails y pa
-        ≈ contr-T-fst y
-            (a .tails y (transp (λ j → C .snd x (eqh (k ∧ ~ j)) y) (~ k) (peq k)))
-            i1
-            (λ _ → u _ .fst .tails y pb
-                 , u _ .snd .tails≈ y
-                       (transp (λ j → C .snd x (eqh (k ∧ ~ j)) y) (~ k) (peq k))
-                       pb
-                       (λ j → lemma (C .snd x (u 1=1 .fst .head) y) (λ h → C .snd x (eqh h) y) pa pb peq k j)
-             )
-    u0 = contr-T-snd y (a .tails y pa) i1 (λ o → u o .fst .tails y pb , u o .snd .tails≈ y pa pb peq)
-   in transport
-         (λ l → PathP
-           (λ z → a .tails y pa
-                ≈ contr-T-φ-fst y
-                   (a .tails y (transp (λ k → C .snd x (u 1=1 .snd .head≈ (~ k ∧ l)) y) (~ l) (peq l)))
-                   (λ _ → u _ .fst .tails y pb
-                        , u _ .snd .tails≈ y (transp (λ k → C .snd x (u _ .snd .head≈ (~ k ∧ l)) y) (~ l) (peq l)) pb
-                               \ j → lemma (C .snd x (u 1=1 .fst .head) y) (λ h → C .snd x (eqh h) y) pa pb peq l j)
-                   z)
-           (transpFill {A = F i0} i0 (\ i → inS (F i)) u0 l)
-           (u _ .snd .tails≈ y pa pb peq))
-         r
-         i
-
-  contr-T-φ : ∀ x a → (u : Partial i1 (T {x} a)) → contr-T x a i1 u ≡ u 1=1
-  contr-T-φ x a u i .fst = contr-T-φ-fst x a u i
-  contr-T-φ x a u i .snd = contr-T-φ-snd x a u i
-
-
-  contr-T' : ∀ {x} a → isContr (T {x} a)
-  contr-T' a = isContrPartial→isContr (contr-T _ a) \ u → sym (contr-T-φ _ a (\ _ → u))
-
-
-  bisimEquiv : ∀ {x} {a b : M C x} → isEquiv (misib a b)
-  bisimEquiv = isContrToUniv _≈_ (misib _ _) contr-T'
diff --git a/Cubical/Codata/Stream.agda b/Cubical/Codata/Stream.agda
index 45011fd312..07ae80fd54 100644
--- a/Cubical/Codata/Stream.agda
+++ b/Cubical/Codata/Stream.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --guardedness #-}
+{-# OPTIONS --safe --guardedness #-}
 
 module Cubical.Codata.Stream where
 
diff --git a/GNUmakefile b/GNUmakefile
index 92830cce3f..95211febbf 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -35,12 +35,12 @@ check-everythings:
 
 .PHONY : gen-everythings
 gen-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations Codata
+	$(EVERYTHINGS) gen-except Core Foundations
 
 .PHONY : gen-and-check-everythings
 gen-and-check-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations Codata
-	$(EVERYTHINGS) check Core Foundations Codata
+	$(EVERYTHINGS) gen-except Core Foundations
+	$(EVERYTHINGS) check Core Foundations
 
 .PHONY : check-README
 check-README:

From 7deb8be42d035b5f953690d31e1d42421dec9ba8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Mon, 13 May 2024 15:30:32 +0200
Subject: [PATCH 02/11] move things around

---
 Cubical/Codata/M.agda                         | 95 -------------------
 Cubical/Codata/M/AsLimit/Coalg.agda           |  5 -
 Cubical/Codata/M/Coalg.agda                   |  5 +
 .../Codata/M/{AsLimit => }/Coalg/Base.agda    |  6 +-
 Cubical/Codata/M/{AsLimit => }/Container.agda |  4 +-
 Cubical/Codata/M/{AsLimit => }/M.agda         |  6 +-
 Cubical/Codata/M/{AsLimit => }/M/Base.agda    |  9 +-
 .../Codata/M/{AsLimit => }/M/Properties.agda  |  8 +-
 Cubical/Codata/M/{AsLimit => }/helper.agda    |  2 +-
 Cubical/Codata/M/{AsLimit => }/itree.agda     |  8 +-
 Cubical/Codata/M/{AsLimit => }/stream.agda    |  8 +-
 11 files changed, 30 insertions(+), 126 deletions(-)
 delete mode 100644 Cubical/Codata/M.agda
 delete mode 100644 Cubical/Codata/M/AsLimit/Coalg.agda
 create mode 100644 Cubical/Codata/M/Coalg.agda
 rename Cubical/Codata/M/{AsLimit => }/Coalg/Base.agda (90%)
 rename Cubical/Codata/M/{AsLimit => }/Container.agda (96%)
 rename Cubical/Codata/M/{AsLimit => }/M.agda (59%)
 rename Cubical/Codata/M/{AsLimit => }/M/Base.agda (98%)
 rename Cubical/Codata/M/{AsLimit => }/M/Properties.agda (93%)
 rename Cubical/Codata/M/{AsLimit => }/helper.agda (98%)
 rename Cubical/Codata/M/{AsLimit => }/itree.agda (93%)
 rename Cubical/Codata/M/{AsLimit => }/stream.agda (76%)

diff --git a/Cubical/Codata/M.agda b/Cubical/Codata/M.agda
deleted file mode 100644
index 4399a07c62..0000000000
--- a/Cubical/Codata/M.agda
+++ /dev/null
@@ -1,95 +0,0 @@
-{-# OPTIONS --safe --guardedness #-}
-module Cubical.Codata.M where
-
-open import Cubical.Foundations.Prelude
-
--- TODO move
-module Helpers where
-  module _ {ℓ ℓ'} {A : Type ℓ} {x : A} (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
-    -- A version with y as an explicit argument can be used to make Agda
-    -- infer the family P.
-    J' : ∀ y (p : x ≡ y) → P y p
-    J' y p = J P d p
-
-  lem-transp : ∀ {ℓ} {A : Type ℓ} (i : I) → (B : Type ℓ) (P : A ≡ B) → (p : P i) → PathP (\ j → P j) (transp (\ k → P (~ k ∧ i)) (~ i) p)
-                                                                                         (transp (\ k → P (k ∨ i)) i p)
-  lem-transp {A = A} i = J' _ (\ p j → transp (\ _ → A) ((~ j ∧ ~ i) ∨ (j ∧ i)) p )
-
-  transp-over : ∀ {ℓ} (A : I → Type ℓ) (i j : I) → A i → A j
-  transp-over A i k p = transp (\ j → A ((~ j ∧ i) ∨ (j ∧ k))) (~ i ∧ ~ k) p
-
-  transp-over-1 : ∀ {ℓ} (A : I → Type ℓ) (i j : I) → A i → A j
-  transp-over-1 A i k p = transp (\ j → A ((j ∨ i) ∧ (~ j ∨ k))) (i ∧ k) p
-
-  compPathD : {ℓ ℓ' : _} {X : Type ℓ} (F : X → Type ℓ') {A B C : X} (P : A ≡ B) (Q : B ≡ C)
-              → ∀ {x y z} → (\ i → F (P i)) [ x ≡ y ] → (\ i → F (Q i)) [ y ≡ z ] → (\ i → F ((P ∙ Q) i)) [ x ≡ z ]
-  compPathD F {A = A} P Q {x} p q i =
-     comp (\ j → F (hfill (λ j → \ { (i = i0) → A ; (i = i1) → Q j })
-                          (inS (P i))
-                          j))
-          (λ j → \ { (i = i0) → x; (i = i1) → q j })
-          (p i)
-
-open Helpers
-
-IxCont : ∀ {ℓ} -> Type ℓ → Type (ℓ-suc ℓ)
-IxCont {ℓ} X = Σ (X → Type ℓ) λ S → ∀ x → S x → X → Type ℓ
-
-
-⟦_⟧ : ∀ {ℓ} {X : Type ℓ} → IxCont X → (X → Type ℓ) → (X → Type ℓ)
-⟦ (S , P) ⟧ X x = Σ (S x) λ s → ∀ y → P x s y → X y
-
-
-record M {ℓ} {X : Type ℓ} (C : IxCont X) (x : X) : Type ℓ where -- Type₀
-  coinductive
-  field
-    head : C .fst x
-    tails : ∀ y → C .snd x head y → M C y
-
-open M public
-
-module _ {ℓ} {X : Type ℓ} {C : IxCont X} where
-
-  private
-    F = ⟦ C ⟧
-
-  inM : ∀ x → F (M C) x → M C x
-  inM x (head , tail) = record { head = head ; tails = tail }
-
-  out : ∀ x → M C x → F (M C) x
-  out x a = (a .head) , (a .tails)
-
-  mapF : ∀ {A B} → (∀ x → A x → B x) → ∀ x → F A x → F B x
-  mapF f x (s , t) = s , \ y p → f _ (t y p)
-
-  unfold : ∀ {A} (α : ∀ x → A x → F A x) → ∀ x → A x → M C x
-  unfold α x a .head = α x a .fst
-  unfold α x a .tails y p = unfold α y (α x a .snd y p)
-
-
-  -- We generalize the type to avoid upsetting --guardedness by
-  -- transporting after the corecursive call.
-  -- Recognizing hcomp/transp as guardedness-preserving could be a better solution.
-  unfold-η' : ∀ {A} (α : ∀ x → A x → F A x) → (h : ∀ x → A x → M C x)
-                     → (∀ (x : X) (a : A x) → out x (h x a) ≡ mapF h x (α x a))
-                     → ∀ (x : X) (a : A x) m → h x a ≡ m → m ≡ unfold α x a
-  unfold-η' α h eq x a m eq' = let heq = cong head (sym eq') ∙ cong fst (eq x a)
-                               in \ where
-                                    i .head → heq i
-                                    i .tails y p →
-                                     let  p0 = (transp-over-1 (\ k → C .snd x (heq k) y) i i1 p)
-                                          p1 = (transp-over (\ k → C .snd x (heq k) y) i i0 p)
-                                          pe = lem-transp i _ (\ k → C .snd x (heq k) y) p
-                                          tl = compPathD (λ p → C .snd x p y → M C y)
-                                                         (cong head (sym eq')) (cong fst (eq x a))
-                                                         (cong (\ f → f .tails y) (sym eq'))
-                                                         (cong (\ f → f .snd   y) (eq x a))
-                                     in unfold-η' α h eq y (α x a .snd y p0)
-                                                           (m .tails y p1)
-                                                           (sym (\ k → tl k (pe k)))
-                                                           i
-
-  unfold-η : ∀ {A} (α : ∀ x → A x → F A x) → (h : ∀ x → A x → M C x)
-                     → (∀ (x : X) (a : A x) → out x (h x a) ≡ mapF h x (α x a))
-                     → ∀ (x : X) (a : A x) → h x a ≡ unfold α x a
-  unfold-η α h eq x a = unfold-η' α h eq x a _ refl
diff --git a/Cubical/Codata/M/AsLimit/Coalg.agda b/Cubical/Codata/M/AsLimit/Coalg.agda
deleted file mode 100644
index 4118df13c7..0000000000
--- a/Cubical/Codata/M/AsLimit/Coalg.agda
+++ /dev/null
@@ -1,5 +0,0 @@
-{-# OPTIONS --guardedness --safe #-}
-
-module Cubical.Codata.M.AsLimit.Coalg where
-
-open import Cubical.Codata.M.AsLimit.Coalg.Base public
diff --git a/Cubical/Codata/M/Coalg.agda b/Cubical/Codata/M/Coalg.agda
new file mode 100644
index 0000000000..184589d90a
--- /dev/null
+++ b/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
diff --git a/Cubical/Codata/M/AsLimit/Coalg/Base.agda b/Cubical/Codata/M/Coalg/Base.agda
similarity index 90%
rename from Cubical/Codata/M/AsLimit/Coalg/Base.agda
rename to Cubical/Codata/M/Coalg/Base.agda
index d4c7105c23..324d2d0f0d 100644
--- a/Cubical/Codata/M/AsLimit/Coalg/Base.agda
+++ b/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 --
diff --git a/Cubical/Codata/M/AsLimit/Container.agda b/Cubical/Codata/M/Container.agda
similarity index 96%
rename from Cubical/Codata/M/AsLimit/Container.agda
rename to Cubical/Codata/M/Container.agda
index f0c9cb6e8f..c96ec2c81d 100644
--- a/Cubical/Codata/M/AsLimit/Container.agda
+++ b/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 --
diff --git a/Cubical/Codata/M/AsLimit/M.agda b/Cubical/Codata/M/M.agda
similarity index 59%
rename from Cubical/Codata/M/AsLimit/M.agda
rename to Cubical/Codata/M/M.agda
index 238b294064..333260c7c7 100644
--- a/Cubical/Codata/M/AsLimit/M.agda
+++ b/Cubical/Codata/M/M.agda
@@ -5,7 +5,7 @@
 -- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
 -}
 {-# OPTIONS --guardedness --safe #-}
-module Cubical.Codata.M.AsLimit.M where
+module Cubical.Codata.M.M where
 
-open import Cubical.Codata.M.AsLimit.M.Base public
-open import Cubical.Codata.M.AsLimit.M.Properties public
+open import Cubical.Codata.M.M.Base public
+open import Cubical.Codata.M.M.Properties public
diff --git a/Cubical/Codata/M/AsLimit/M/Base.agda b/Cubical/Codata/M/M/Base.agda
similarity index 98%
rename from Cubical/Codata/M/AsLimit/M/Base.agda
rename to Cubical/Codata/M/M/Base.agda
index a07b2d8116..a1dce924ff 100644
--- a/Cubical/Codata/M/AsLimit/M/Base.agda
+++ b/Cubical/Codata/M/M/Base.agda
@@ -5,7 +5,7 @@
 -- "Non-wellfounded trees in Homotopy Type Theory"
 -- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
 
-module Cubical.Codata.M.AsLimit.M.Base where
+module Cubical.Codata.M.M.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv using (_≃_)
@@ -27,10 +27,9 @@ open import Cubical.Foundations.GroupoidLaws
 
 open import Cubical.Data.Sum
 
-open import Cubical.Codata.M.AsLimit.helper
-open import Cubical.Codata.M.AsLimit.Container
-
-open import Cubical.Codata.M.AsLimit.Coalg.Base
+open import Cubical.Codata.M.helper
+open import Cubical.Codata.M.Container
+open import Cubical.Codata.M.Coalg.Base
 
 open Iso
 
diff --git a/Cubical/Codata/M/AsLimit/M/Properties.agda b/Cubical/Codata/M/M/Properties.agda
similarity index 93%
rename from Cubical/Codata/M/AsLimit/M/Properties.agda
rename to Cubical/Codata/M/M/Properties.agda
index adabd33a1e..1f5a8112eb 100644
--- a/Cubical/Codata/M/AsLimit/M/Properties.agda
+++ b/Cubical/Codata/M/M/Properties.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --guardedness --safe #-}
 
-module Cubical.Codata.M.AsLimit.M.Properties where
+module Cubical.Codata.M.M.Properties where
 
 open import Cubical.Data.Unit
 open import Cubical.Data.Prod
@@ -19,9 +19,9 @@ open import Cubical.Foundations.Equiv
 
 open import Cubical.Functions.Embedding
 
-open import Cubical.Codata.M.AsLimit.helper
-open import Cubical.Codata.M.AsLimit.M.Base
-open import Cubical.Codata.M.AsLimit.Container
+open import Cubical.Codata.M.helper
+open import Cubical.Codata.M.M.Base
+open import Cubical.Codata.M.Container
 
 -- in-fun and out-fun are inverse
 
diff --git a/Cubical/Codata/M/AsLimit/helper.agda b/Cubical/Codata/M/helper.agda
similarity index 98%
rename from Cubical/Codata/M/AsLimit/helper.agda
rename to Cubical/Codata/M/helper.agda
index 33be276fd7..fb649edd5b 100644
--- a/Cubical/Codata/M/AsLimit/helper.agda
+++ b/Cubical/Codata/M/helper.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --guardedness --safe #-}
 
-module Cubical.Codata.M.AsLimit.helper where
+module Cubical.Codata.M.helper where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv using (_≃_)
diff --git a/Cubical/Codata/M/AsLimit/itree.agda b/Cubical/Codata/M/itree.agda
similarity index 93%
rename from Cubical/Codata/M/AsLimit/itree.agda
rename to Cubical/Codata/M/itree.agda
index 50d8e10757..6edb0d4ebb 100644
--- a/Cubical/Codata/M/AsLimit/itree.agda
+++ b/Cubical/Codata/M/itree.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --guardedness --safe #-}
 
-module Cubical.Codata.M.AsLimit.itree where
+module Cubical.Codata.M.itree where
 
 open import Cubical.Data.Unit
 open import Cubical.Data.Prod
@@ -12,9 +12,9 @@ open import Cubical.Data.Bool
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Prelude
 
-open import Cubical.Codata.M.AsLimit.Container
-open import Cubical.Codata.M.AsLimit.M
-open import Cubical.Codata.M.AsLimit.Coalg
+open import Cubical.Codata.M.Container
+open import Cubical.Codata.M.M
+open import Cubical.Codata.M.Coalg
 
 -- Delay monad defined as an M-type
 delay-S : (R : Type₀) -> Container ℓ-zero
diff --git a/Cubical/Codata/M/AsLimit/stream.agda b/Cubical/Codata/M/stream.agda
similarity index 76%
rename from Cubical/Codata/M/AsLimit/stream.agda
rename to Cubical/Codata/M/stream.agda
index f6fc3c19eb..4e952cac3f 100644
--- a/Cubical/Codata/M/AsLimit/stream.agda
+++ b/Cubical/Codata/M/stream.agda
@@ -1,14 +1,14 @@
 {-# OPTIONS --guardedness --safe #-}
 
-module Cubical.Codata.M.AsLimit.stream where
+module Cubical.Codata.M.stream where
 
 open import Cubical.Data.Unit
 
 open import Cubical.Foundations.Prelude
 
-open import Cubical.Codata.M.AsLimit.M
-open import Cubical.Codata.M.AsLimit.helper
-open import Cubical.Codata.M.AsLimit.Container
+open import Cubical.Codata.M.M
+open import Cubical.Codata.M.helper
+open import Cubical.Codata.M.Container
 
 --------------------------------------
 -- Stream definitions using M.AsLimit --

From 73ac573fafe9d8f388e5f8e9850bc9f7e24dc59b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Mon, 13 May 2024 15:31:24 +0200
Subject: [PATCH 03/11] revert

---
 Cubical/Codata/Everything.agda | 15 +++++++++++++++
 GNUmakefile                    |  6 +++---
 2 files changed, 18 insertions(+), 3 deletions(-)
 create mode 100644 Cubical/Codata/Everything.agda

diff --git a/Cubical/Codata/Everything.agda b/Cubical/Codata/Everything.agda
new file mode 100644
index 0000000000..163e335490
--- /dev/null
+++ b/Cubical/Codata/Everything.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --safe --guardedness #-}
+module Cubical.Codata.Everything where
+
+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
diff --git a/GNUmakefile b/GNUmakefile
index 95211febbf..92830cce3f 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -35,12 +35,12 @@ check-everythings:
 
 .PHONY : gen-everythings
 gen-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations
+	$(EVERYTHINGS) gen-except Core Foundations Codata
 
 .PHONY : gen-and-check-everythings
 gen-and-check-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations
-	$(EVERYTHINGS) check Core Foundations
+	$(EVERYTHINGS) gen-except Core Foundations Codata
+	$(EVERYTHINGS) check Core Foundations Codata
 
 .PHONY : check-README
 check-README:

From ea7c6602959802477390f77dbfc8746c6ed7f65d Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 13 May 2024 14:35:45 +0200
Subject: [PATCH 04/11] remove foundation/everything

---
 Cubical/Foundations/Everything.agda | 34 -----------------------------
 GNUmakefile                         |  6 ++---
 2 files changed, 3 insertions(+), 37 deletions(-)
 delete mode 100644 Cubical/Foundations/Everything.agda

diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda
deleted file mode 100644
index def615db0f..0000000000
--- a/Cubical/Foundations/Everything.agda
+++ /dev/null
@@ -1,34 +0,0 @@
-{-# OPTIONS --safe #-}
-module Cubical.Foundations.Everything where
-
--- Basic cubical prelude
-open import Cubical.Foundations.Prelude public
-
-open import Cubical.Foundations.Function public
-open import Cubical.Foundations.Equiv public
-  hiding (transpEquiv) -- Hide to avoid clash with Transport.transpEquiv
-open import Cubical.Foundations.Equiv.Properties public
-open import Cubical.Foundations.Equiv.Fiberwise
-open import Cubical.Foundations.Equiv.PathSplit public
-open import Cubical.Foundations.Equiv.BiInvertible public
-open import Cubical.Foundations.Equiv.HalfAdjoint
-open import Cubical.Foundations.Equiv.Dependent
-open import Cubical.Foundations.HLevels public
-open import Cubical.Foundations.HLevels.Extend
-open import Cubical.Foundations.Path public
-open import Cubical.Foundations.Pointed public
-open import Cubical.Foundations.RelationalStructure public
-open import Cubical.Foundations.Structure public
-open import Cubical.Foundations.Transport public
-open import Cubical.Foundations.Univalence public
-open import Cubical.Foundations.Univalence.Universe
-open import Cubical.Foundations.Univalence.Dependent
-open import Cubical.Foundations.GroupoidLaws public
-open import Cubical.Foundations.Isomorphism public
-open import Cubical.Foundations.CartesianKanOps
-open import Cubical.Foundations.Powerset
-open import Cubical.Foundations.SIP
-open import Cubical.Foundations.Cubes
-open import Cubical.Foundations.Cubes.Subtypes
-open import Cubical.Foundations.Cubes.Dependent
-open import Cubical.Foundations.Cubes.HLevels
diff --git a/GNUmakefile b/GNUmakefile
index 92830cce3f..ac20959549 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -35,12 +35,12 @@ check-everythings:
 
 .PHONY : gen-everythings
 gen-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations Codata
+	$(EVERYTHINGS) gen-except Core Codata
 
 .PHONY : gen-and-check-everythings
 gen-and-check-everythings:
-	$(EVERYTHINGS) gen-except Core Foundations Codata
-	$(EVERYTHINGS) check Core Foundations Codata
+	$(EVERYTHINGS) gen-except Core Codata
+	$(EVERYTHINGS) check Core Codata
 
 .PHONY : check-README
 check-README:

From fd4918705ae3f2e4cd62122ca2593544a2d9dd08 Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 13 May 2024 14:36:20 +0200
Subject: [PATCH 05/11] delete outdated README.md

---
 Cubical/Core/README.md | 16 ----------------
 1 file changed, 16 deletions(-)
 delete mode 100644 Cubical/Core/README.md

diff --git a/Cubical/Core/README.md b/Cubical/Core/README.md
deleted file mode 100644
index da6b3180d1..0000000000
--- a/Cubical/Core/README.md
+++ /dev/null
@@ -1,16 +0,0 @@
-Core library for Cubical Agda
-=============================
-
-This folder contains the core library for Cubical Agda. It contains
-the following things:
-
-* **Primitives**: exposes cubical agda primitives.
-
-* **Glue**: definition of equivalences, Glue types and the univalence
-  theorem.
-
-* **Id**: identity types and definitions of J, funExt, univalence and
-  propositional truncation using Id instead of Path.
-
-This library is intentionally kept as minimal as possible and does not
-depend on the Agda standard library.

From 721d93a328b6c9515d8d1cd7c46f5226baee011e Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 13 May 2024 15:29:53 +0200
Subject: [PATCH 06/11] remove Core/Everything, update and clean up imports

---
 .gitignore                                       |  2 --
 Cubical/Codata/Conat/Properties.agda             |  2 --
 Cubical/Codata/Stream/Base.agda                  |  2 +-
 Cubical/Codata/Stream/Properties.agda            |  2 --
 Cubical/Core/Everything.agda                     |  8 --------
 Cubical/Core/Glue.agda                           |  5 ++---
 Cubical/Data/Bool/Properties.agda                |  2 --
 Cubical/Data/Bool/SwitchStatement.agda           |  2 --
 Cubical/Data/DescendingList/Strict.agda          |  2 +-
 Cubical/Data/Fin/Properties.agda                 | 10 ++++------
 Cubical/Data/InfNat/Base.agda                    |  3 ++-
 Cubical/Data/Int/Base.agda                       |  3 ++-
 Cubical/Data/Int/MoreInts/BiInvInt/Base.agda     | 10 +++-------
 Cubical/Data/Int/MoreInts/QuoInt/Base.agda       |  3 +--
 Cubical/Data/Int/MoreInts/QuoInt/Properties.agda |  3 ++-
 Cubical/Data/Int/Properties.agda                 |  3 +--
 Cubical/Data/List/Base.agda                      |  4 +++-
 Cubical/Data/List/Properties.agda                |  9 ++++-----
 Cubical/Data/Maybe/Base.agda                     |  2 +-
 Cubical/Data/Nat/Algebra.agda                    |  2 --
 Cubical/Data/Nat/Base.agda                       |  2 --
 Cubical/Data/Prod/Base.agda                      |  2 --
 Cubical/Data/Prod/Properties.agda                | 10 ++++------
 Cubical/Data/Sigma/Properties.agda               |  9 ++++-----
 Cubical/Data/Sum/Base.agda                       |  2 +-
 Cubical/Data/Sum/Properties.agda                 | 11 ++++++-----
 Cubical/Data/Unit/Properties.agda                |  7 +------
 Cubical/Foundations/Equiv/Fiberwise.agda         |  3 +--
 Cubical/Foundations/Equiv/Properties.agda        |  6 ++----
 Cubical/Foundations/Isomorphism.agda             |  2 +-
 Cubical/Foundations/Structure.agda               |  2 +-
 Cubical/Foundations/Univalence/Universe.agda     |  2 +-
 Cubical/HITs/GroupoidQuotients/Properties.agda   |  2 --
 Cubical/HITs/InfNat/Base.agda                    |  7 +++----
 Cubical/HITs/InfNat/Properties.agda              |  7 +++----
 Cubical/HITs/Interval/Base.agda                  |  2 --
 Cubical/HITs/KleinBottle/Base.agda               |  2 +-
 .../HITs/PropositionalTruncation/Properties.agda |  2 --
 Cubical/HITs/SetQuotients/Properties.agda        |  2 --
 Cubical/HITs/SetTruncation/Properties.agda       |  4 ++--
 Cubical/Homotopy/Loopspace.agda                  | 16 ++++++++--------
 Cubical/Relation/Binary/Base.agda                |  2 --
 .../Relation/ZigZag/Applications/MultiSet.agda   |  3 ++-
 Cubical/Relation/ZigZag/Base.agda                |  4 +++-
 GNUmakefile                                      |  6 +++---
 45 files changed, 74 insertions(+), 122 deletions(-)
 delete mode 100644 Cubical/Core/Everything.agda

diff --git a/.gitignore b/.gitignore
index 7d344f2d84..7448c776f5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,6 +3,4 @@
 \.*#*
 \#*
 Cubical/*/Everything.agda
-!Cubical/Core/Everything.agda
-!Cubical/Foundations/Everything.agda
 !Cubical/Codata/Everything.agda
diff --git a/Cubical/Codata/Conat/Properties.agda b/Cubical/Codata/Conat/Properties.agda
index d9cc9c8d7a..b620efb598 100644
--- a/Cubical/Codata/Conat/Properties.agda
+++ b/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
diff --git a/Cubical/Codata/Stream/Base.agda b/Cubical/Codata/Stream/Base.agda
index d4a62600a3..dedb0284ec 100644
--- a/Cubical/Codata/Stream/Base.agda
+++ b/Cubical/Codata/Stream/Base.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --safe --guardedness #-}
 module Cubical.Codata.Stream.Base where
 
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
 
 record Stream (A : Type₀) : Type₀ where
   coinductive
diff --git a/Cubical/Codata/Stream/Properties.agda b/Cubical/Codata/Stream/Properties.agda
index 85927262c1..22db042543 100644
--- a/Cubical/Codata/Stream/Properties.agda
+++ b/Cubical/Codata/Stream/Properties.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --safe --guardedness #-}
 module Cubical.Codata.Stream.Properties where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Data.Nat
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Core/Everything.agda b/Cubical/Core/Everything.agda
deleted file mode 100644
index c82602edc9..0000000000
--- a/Cubical/Core/Everything.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-{-# OPTIONS --safe #-}
-module Cubical.Core.Everything where
-
--- Basic primitives (some are from Agda.Primitive)
-open import Cubical.Core.Primitives public
-
--- Definition of equivalences and Glue types
-open import Cubical.Core.Glue public
diff --git a/Cubical/Core/Glue.agda b/Cubical/Core/Glue.agda
index 89f9dd49ed..68d2b6ae0f 100644
--- a/Cubical/Core/Glue.agda
+++ b/Cubical/Core/Glue.agda
@@ -125,9 +125,8 @@ private
     e1 : T1 ≃ A1
     e1 = e i1 1=1
 
-    open import Cubical.Foundations.Prelude using (transport)
     transportA : A0 → A1
-    transportA = transport (λ i → A i)
+    transportA = transp (λ i → A i) i0
 
     -- copied over from Foundations/Equiv for readability, can't directly import due to cyclic dependency
     invEq : ∀ {X : Type ℓ'} {ℓ''} {Y : Type ℓ''} (w : X ≃ Y) → Y → X
@@ -136,4 +135,4 @@ private
     -- transport in Glue reduces to transport in A + the application of the equivalences in forward and backward
     -- direction.
     transp-S : (t0 : T0) → T1 [ i1 ↦ (λ _ → invEq e1 (transportA (equivFun e0 t0))) ]
-    transp-S t0 = inS (transport (λ i → Glue (A i) (Te i)) t0)
+    transp-S t0 = inS (transp (λ i → Glue (A i) (Te i)) i0 t0)
diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda
index 5570fabbd6..be192d0af6 100644
--- a/Cubical/Data/Bool/Properties.agda
+++ b/Cubical/Data/Bool/Properties.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Bool.Properties where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Functions.Involution
 
 open import Cubical.Foundations.Prelude
diff --git a/Cubical/Data/Bool/SwitchStatement.agda b/Cubical/Data/Bool/SwitchStatement.agda
index 841dbdbda6..9911eca09a 100644
--- a/Cubical/Data/Bool/SwitchStatement.agda
+++ b/Cubical/Data/Bool/SwitchStatement.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Bool.SwitchStatement where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Data.Bool.Base
diff --git a/Cubical/Data/DescendingList/Strict.agda b/Cubical/Data/DescendingList/Strict.agda
index 4141c6d76f..9429c2880f 100644
--- a/Cubical/Data/DescendingList/Strict.agda
+++ b/Cubical/Data/DescendingList/Strict.agda
@@ -4,7 +4,7 @@
 
 {-# OPTIONS --safe #-}
 
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
 
 module Cubical.Data.DescendingList.Strict
  (A : Type₀)
diff --git a/Cubical/Data/Fin/Properties.agda b/Cubical/Data/Fin/Properties.agda
index c14c1e236f..dda477bf43 100644
--- a/Cubical/Data/Fin/Properties.agda
+++ b/Cubical/Data/Fin/Properties.agda
@@ -1,19 +1,17 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Data.Fin.Properties where
 
-open import Cubical.Core.Everything
-
-open import Cubical.Functions.Embedding
-open import Cubical.Functions.Surjection
+open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Transport
 
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
 open import Cubical.HITs.PropositionalTruncation renaming (rec to ∥∥rec)
 
 open import Cubical.Data.Fin.Base as Fin
diff --git a/Cubical/Data/InfNat/Base.agda b/Cubical/Data/InfNat/Base.agda
index d368954645..020c95c0d7 100644
--- a/Cubical/Data/InfNat/Base.agda
+++ b/Cubical/Data/InfNat/Base.agda
@@ -2,8 +2,9 @@
 
 module Cubical.Data.InfNat.Base where
 
+open import Cubical.Foundations.Prelude
+
 open import Cubical.Data.Nat as ℕ using (ℕ)
-open import Cubical.Core.Primitives
 
 data ℕ+∞ : Type₀ where
   ∞ : ℕ+∞
diff --git a/Cubical/Data/Int/Base.agda b/Cubical/Data/Int/Base.agda
index ba7500dfe5..0576b0f241 100644
--- a/Cubical/Data/Int/Base.agda
+++ b/Cubical/Data/Int/Base.agda
@@ -3,7 +3,8 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Int.Base where
 
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
+
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat hiding (_+_ ; _·_) renaming (isEven to isEvenℕ ; isOdd to isOddℕ)
 open import Cubical.Data.Fin.Inductive.Base
diff --git a/Cubical/Data/Int/MoreInts/BiInvInt/Base.agda b/Cubical/Data/Int/MoreInts/BiInvInt/Base.agda
index 83af6718b4..040b45754f 100644
--- a/Cubical/Data/Int/MoreInts/BiInvInt/Base.agda
+++ b/Cubical/Data/Int/MoreInts/BiInvInt/Base.agda
@@ -16,21 +16,18 @@ This file contains:
 {-# OPTIONS --safe #-}
 module Cubical.Data.Int.MoreInts.BiInvInt.Base where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
-open import Cubical.Data.Nat
-open import Cubical.Data.Int
-
 open import Cubical.Foundations.GroupoidLaws
-
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Equiv.BiInvertible
 open import Cubical.Foundations.Equiv.HalfAdjoint
 
+open import Cubical.Data.Nat
+open import Cubical.Data.Int
+
 open import Cubical.Relation.Nullary
 
 
@@ -307,4 +304,3 @@ private
 
   predl'-suc : ∀ z → predl' (suc z) ≡ z
   predl'-suc z = refl
-
diff --git a/Cubical/Data/Int/MoreInts/QuoInt/Base.agda b/Cubical/Data/Int/MoreInts/QuoInt/Base.agda
index 96decf2200..92a3802f7a 100644
--- a/Cubical/Data/Int/MoreInts/QuoInt/Base.agda
+++ b/Cubical/Data/Int/MoreInts/QuoInt/Base.agda
@@ -2,13 +2,12 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Int.MoreInts.QuoInt.Base where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
+
 open import Cubical.Relation.Nullary
 
 open import Cubical.Data.Int using ()
diff --git a/Cubical/Data/Int/MoreInts/QuoInt/Properties.agda b/Cubical/Data/Int/MoreInts/QuoInt/Properties.agda
index 8669ba9a0c..6090457ab8 100644
--- a/Cubical/Data/Int/MoreInts/QuoInt/Properties.agda
+++ b/Cubical/Data/Int/MoreInts/QuoInt/Properties.agda
@@ -1,13 +1,14 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Int.MoreInts.QuoInt.Properties where
 
-open import Cubical.Core.Everything
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
+
 open import Cubical.Functions.FunExtEquiv
+
 open import Cubical.Relation.Nullary
 
 open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda
index 9a3c1d36fd..1fc854cafa 100644
--- a/Cubical/Data/Int/Properties.agda
+++ b/Cubical/Data/Int/Properties.agda
@@ -1,12 +1,11 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Int.Properties where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Equiv
 
 open import Cubical.Relation.Nullary
 
diff --git a/Cubical/Data/List/Base.agda b/Cubical/Data/List/Base.agda
index a78ac00455..2695f1de8c 100644
--- a/Cubical/Data/List/Base.agda
+++ b/Cubical/Data/List/Base.agda
@@ -2,7 +2,9 @@
 module Cubical.Data.List.Base where
 
 open import Agda.Builtin.List public
-open import Cubical.Core.Everything
+
+open import Cubical.Foundations.Prelude
+
 open import Cubical.Data.Maybe.Base as Maybe hiding (rec ; elim)
 open import Cubical.Data.Nat.Base hiding (elim)
 
diff --git a/Cubical/Data/List/Properties.agda b/Cubical/Data/List/Properties.agda
index 7b755944f5..5dc57b71b6 100644
--- a/Cubical/Data/List/Properties.agda
+++ b/Cubical/Data/List/Properties.agda
@@ -1,22 +1,21 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.List.Properties where
 
-open import Agda.Builtin.List
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
+
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
 open import Cubical.Data.Sum as ⊎ hiding (map)
 open import Cubical.Data.Unit
-open import Cubical.Relation.Nullary
-
 open import Cubical.Data.List.Base as List
 
+open import Cubical.Relation.Nullary
+
 module _ {ℓ} {A : Type ℓ} where
 
   ++-unit-r : (xs : List A) → xs ++ [] ≡ xs
diff --git a/Cubical/Data/Maybe/Base.agda b/Cubical/Data/Maybe/Base.agda
index 1712b822ca..713b9e8d10 100644
--- a/Cubical/Data/Maybe/Base.agda
+++ b/Cubical/Data/Maybe/Base.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Maybe.Base where
 
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
 
 private
   variable
diff --git a/Cubical/Data/Nat/Algebra.agda b/Cubical/Data/Nat/Algebra.agda
index 0ee04806b4..d6d9761b89 100644
--- a/Cubical/Data/Nat/Algebra.agda
+++ b/Cubical/Data/Nat/Algebra.agda
@@ -15,8 +15,6 @@ by Steve Awodey, Nicola Gambino and Kristina Sojakova.
 
 module Cubical.Data.Nat.Algebra where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
diff --git a/Cubical/Data/Nat/Base.agda b/Cubical/Data/Nat/Base.agda
index 9f424f947b..87e9c4aa86 100644
--- a/Cubical/Data/Nat/Base.agda
+++ b/Cubical/Data/Nat/Base.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --no-exact-split --safe #-}
 module Cubical.Data.Nat.Base where
 
-open import Cubical.Core.Primitives
-
 open import Agda.Builtin.Nat public
   using (zero; suc; _+_)
   renaming (Nat to ℕ; _-_ to _∸_; _*_ to _·_)
diff --git a/Cubical/Data/Prod/Base.agda b/Cubical/Data/Prod/Base.agda
index 89c8b92bba..b3f3c8795c 100644
--- a/Cubical/Data/Prod/Base.agda
+++ b/Cubical/Data/Prod/Base.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Prod.Base where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 
diff --git a/Cubical/Data/Prod/Properties.agda b/Cubical/Data/Prod/Properties.agda
index 393352c444..58e0f01b6b 100644
--- a/Cubical/Data/Prod/Properties.agda
+++ b/Cubical/Data/Prod/Properties.agda
@@ -1,11 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Prod.Properties where
 
-open import Cubical.Core.Everything
-
-open import Cubical.Data.Prod.Base
-open import Cubical.Data.Sigma renaming (_×_ to _×Σ_) hiding (prodIso ; toProdIso ; curryIso)
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
@@ -13,6 +8,9 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
 
+open import Cubical.Data.Prod.Base
+open import Cubical.Data.Sigma renaming (_×_ to _×Σ_) hiding (prodIso ; toProdIso ; curryIso)
+
 private
   variable
     ℓ ℓ' : Level
@@ -22,7 +20,7 @@ private
 -- Swapping is an equivalence
 
 ×≡ : {a b : A × B} → proj₁ a ≡ proj₁ b → proj₂ a ≡ proj₂ b → a ≡ b
-×≡ {a = (a1 , b1)} {b = (a2 , b2)} id1 id2 i = (id1 i) , (id2 i)
+×≡ {a = (_ , _)} {b = (_ , _)} id1 id2 i = (id1 i) , (id2 i)
 
 swap : A × B → B × A
 swap (x , y) = (y , x)
diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda
index a3db8125dc..fea7559aad 100644
--- a/Cubical/Data/Sigma/Properties.agda
+++ b/Cubical/Data/Sigma/Properties.agda
@@ -15,10 +15,6 @@ Basic properties about Σ-types
 {-# OPTIONS --safe #-}
 module Cubical.Data.Sigma.Properties where
 
-open import Cubical.Data.Sigma.Base
-
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
@@ -28,10 +24,13 @@ open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Path
 open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Univalence
-open import Cubical.Relation.Nullary
+
+open import Cubical.Data.Sigma.Base
 open import Cubical.Data.Unit.Base
 open import Cubical.Data.Empty.Base
 
+open import Cubical.Relation.Nullary
+
 open import Cubical.Reflection.StrictEquiv
 
 open Iso
diff --git a/Cubical/Data/Sum/Base.agda b/Cubical/Data/Sum/Base.agda
index 769fb811a0..b4ddd0f8b5 100644
--- a/Cubical/Data/Sum/Base.agda
+++ b/Cubical/Data/Sum/Base.agda
@@ -3,7 +3,7 @@ module Cubical.Data.Sum.Base where
 
 open import Cubical.Relation.Nullary.Base
 
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
 
 private
   variable
diff --git a/Cubical/Data/Sum/Properties.agda b/Cubical/Data/Sum/Properties.agda
index 2be7be3c1f..0cc5687221 100644
--- a/Cubical/Data/Sum/Properties.agda
+++ b/Cubical/Data/Sum/Properties.agda
@@ -1,19 +1,20 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Sum.Properties where
 
-open import Cubical.Core.Everything
-open import Cubical.Foundations.Function
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
-open import Cubical.Functions.Embedding
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Functions.Embedding
+
+open import Cubical.Data.Sum.Base as ⊎
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
-open import Cubical.Relation.Nullary
 
-open import Cubical.Data.Sum.Base as ⊎
+open import Cubical.Relation.Nullary
 
 open Iso
 
diff --git a/Cubical/Data/Unit/Properties.agda b/Cubical/Data/Unit/Properties.agda
index 85b37dc14b..d219f49696 100644
--- a/Cubical/Data/Unit/Properties.agda
+++ b/Cubical/Data/Unit/Properties.agda
@@ -1,23 +1,18 @@
 {-# OPTIONS --safe #-}
 module Cubical.Data.Unit.Properties where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
 
 open import Cubical.Data.Nat
 open import Cubical.Data.Unit.Base
 open import Cubical.Data.Prod.Base
 open import Cubical.Data.Sigma hiding (_×_)
 
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Univalence
-
 open import Cubical.Reflection.StrictEquiv
 
 open Iso
diff --git a/Cubical/Foundations/Equiv/Fiberwise.agda b/Cubical/Foundations/Equiv/Fiberwise.agda
index 9bcbf5021e..9b2e69a1b1 100644
--- a/Cubical/Foundations/Equiv/Fiberwise.agda
+++ b/Cubical/Foundations/Equiv/Fiberwise.agda
@@ -1,13 +1,12 @@
 {-# OPTIONS --safe #-}
 module Cubical.Foundations.Equiv.Fiberwise where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels
+
 open import Cubical.Data.Sigma
 
 private
diff --git a/Cubical/Foundations/Equiv/Properties.agda b/Cubical/Foundations/Equiv/Properties.agda
index b629b6ecbb..0cf3e1eba3 100644
--- a/Cubical/Foundations/Equiv/Properties.agda
+++ b/Cubical/Foundations/Equiv/Properties.agda
@@ -12,10 +12,6 @@ A couple of general facts about equivalences:
 {-# OPTIONS --safe #-}
 module Cubical.Foundations.Equiv.Properties where
 
-open import Cubical.Core.Everything
-
-open import Cubical.Data.Sigma
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv
@@ -27,6 +23,8 @@ open import Cubical.Foundations.HLevels
 
 open import Cubical.Functions.FunExtEquiv
 
+open import Cubical.Data.Sigma
+
 private
   variable
     ℓ ℓ' ℓ'' : Level
diff --git a/Cubical/Foundations/Isomorphism.agda b/Cubical/Foundations/Isomorphism.agda
index a1a128eb11..237a24a251 100644
--- a/Cubical/Foundations/Isomorphism.agda
+++ b/Cubical/Foundations/Isomorphism.agda
@@ -10,7 +10,7 @@ Theory about isomorphisms
 {-# OPTIONS --safe #-}
 module Cubical.Foundations.Isomorphism where
 
-open import Cubical.Core.Everything
+open import Cubical.Core.Glue
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.GroupoidLaws
diff --git a/Cubical/Foundations/Structure.agda b/Cubical/Foundations/Structure.agda
index 099bb8a2eb..eba47e0b78 100644
--- a/Cubical/Foundations/Structure.agda
+++ b/Cubical/Foundations/Structure.agda
@@ -1,8 +1,8 @@
 {-# OPTIONS --safe #-}
 module Cubical.Foundations.Structure where
 
-open import Cubical.Core.Everything
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
 
 private
   variable
diff --git a/Cubical/Foundations/Univalence/Universe.agda b/Cubical/Foundations/Univalence/Universe.agda
index 0857ad7c6d..bf038ddee5 100644
--- a/Cubical/Foundations/Univalence/Universe.agda
+++ b/Cubical/Foundations/Univalence/Universe.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --safe --postfix-projections #-}
 
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
 
 open import Cubical.Functions.Embedding
 open import Cubical.Foundations.Equiv
diff --git a/Cubical/HITs/GroupoidQuotients/Properties.agda b/Cubical/HITs/GroupoidQuotients/Properties.agda
index 6ca1bf5db7..67882c701c 100644
--- a/Cubical/HITs/GroupoidQuotients/Properties.agda
+++ b/Cubical/HITs/GroupoidQuotients/Properties.agda
@@ -9,8 +9,6 @@ module Cubical.HITs.GroupoidQuotients.Properties where
 
 open import Cubical.HITs.GroupoidQuotients.Base
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
diff --git a/Cubical/HITs/InfNat/Base.agda b/Cubical/HITs/InfNat/Base.agda
index 992ab56fcf..ae590cb3a5 100644
--- a/Cubical/HITs/InfNat/Base.agda
+++ b/Cubical/HITs/InfNat/Base.agda
@@ -2,13 +2,12 @@
 
 module Cubical.HITs.InfNat.Base where
 
-open import Cubical.Core.Everything
-open import Cubical.Data.Maybe
-open import Cubical.Data.Nat
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 
+open import Cubical.Data.Maybe
+open import Cubical.Data.Nat
+
 data ℕ+∞ : Type₀ where
   zero : ℕ+∞
   suc : ℕ+∞ → ℕ+∞
diff --git a/Cubical/HITs/InfNat/Properties.agda b/Cubical/HITs/InfNat/Properties.agda
index f974ba7a9e..f5fd33b412 100644
--- a/Cubical/HITs/InfNat/Properties.agda
+++ b/Cubical/HITs/InfNat/Properties.agda
@@ -2,13 +2,12 @@
 
 module Cubical.HITs.InfNat.Properties where
 
-open import Cubical.Core.Everything
-open import Cubical.Data.Maybe
-open import Cubical.Data.Nat
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 
+open import Cubical.Data.Maybe
+open import Cubical.Data.Nat
+
 open import Cubical.HITs.InfNat.Base
 import Cubical.Data.InfNat as Coprod
 
diff --git a/Cubical/HITs/Interval/Base.agda b/Cubical/HITs/Interval/Base.agda
index 54865c63b3..fc52a4bae2 100644
--- a/Cubical/HITs/Interval/Base.agda
+++ b/Cubical/HITs/Interval/Base.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.HITs.Interval.Base where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 
 data Interval : Type₀ where
diff --git a/Cubical/HITs/KleinBottle/Base.agda b/Cubical/HITs/KleinBottle/Base.agda
index 3e9645c0b2..2119e43500 100644
--- a/Cubical/HITs/KleinBottle/Base.agda
+++ b/Cubical/HITs/KleinBottle/Base.agda
@@ -6,7 +6,7 @@ Definition of the Klein bottle as a HIT
 {-# OPTIONS --safe #-}
 module Cubical.HITs.KleinBottle.Base where
 
-open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
 
 data KleinBottle : Type where
   point : KleinBottle
diff --git a/Cubical/HITs/PropositionalTruncation/Properties.agda b/Cubical/HITs/PropositionalTruncation/Properties.agda
index e0b91cf50f..7f143a450c 100644
--- a/Cubical/HITs/PropositionalTruncation/Properties.agda
+++ b/Cubical/HITs/PropositionalTruncation/Properties.agda
@@ -8,8 +8,6 @@ This file contains:
 {-# OPTIONS --safe #-}
 module Cubical.HITs.PropositionalTruncation.Properties where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
diff --git a/Cubical/HITs/SetQuotients/Properties.agda b/Cubical/HITs/SetQuotients/Properties.agda
index 02ca17a0f3..f2327a424d 100644
--- a/Cubical/HITs/SetQuotients/Properties.agda
+++ b/Cubical/HITs/SetQuotients/Properties.agda
@@ -9,8 +9,6 @@ module Cubical.HITs.SetQuotients.Properties where
 
 open import Cubical.HITs.SetQuotients.Base
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
diff --git a/Cubical/HITs/SetTruncation/Properties.agda b/Cubical/HITs/SetTruncation/Properties.agda
index 33d3deefa0..bc42ebb1d1 100644
--- a/Cubical/HITs/SetTruncation/Properties.agda
+++ b/Cubical/HITs/SetTruncation/Properties.agda
@@ -8,8 +8,6 @@ This file contains:
 {-# OPTIONS --safe #-}
 module Cubical.HITs.SetTruncation.Properties where
 
-open import Cubical.HITs.SetTruncation.Base
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Function
@@ -18,9 +16,11 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Pointed.Base
+
 open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation
   renaming (rec to pRec ; elim to pElim) hiding (elim2 ; elim3 ; rec2 ; map)
+open import Cubical.HITs.SetTruncation.Base
 
 private
   variable
diff --git a/Cubical/Homotopy/Loopspace.agda b/Cubical/Homotopy/Loopspace.agda
index b5b2d5aecd..36fef7ea1f 100644
--- a/Cubical/Homotopy/Loopspace.agda
+++ b/Cubical/Homotopy/Loopspace.agda
@@ -2,26 +2,26 @@
 
 module Cubical.Homotopy.Loopspace where
 
-open import Cubical.Core.Everything
-
-open import Cubical.Data.Nat
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Pointed.Homogeneous
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.GroupoidLaws
-open import Cubical.HITs.SetTruncation
-open import Cubical.HITs.Truncation hiding (elim2) renaming (rec to trRec)
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Path
-open import Cubical.Foundations.Equiv.HalfAdjoint
-open import Cubical.Foundations.Equiv
+
 open import Cubical.Functions.Morphism
+
+open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
+
+open import Cubical.HITs.SetTruncation
+open import Cubical.HITs.Truncation hiding (elim2) renaming (rec to trRec)
+
 open Iso
 
 {- loop space of a pointed type -}
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index d583115a76..07d31701af 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Relation.Binary.Base where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
diff --git a/Cubical/Relation/ZigZag/Applications/MultiSet.agda b/Cubical/Relation/ZigZag/Applications/MultiSet.agda
index 5f5b2bfd48..104f5464af 100644
--- a/Cubical/Relation/ZigZag/Applications/MultiSet.agda
+++ b/Cubical/Relation/ZigZag/Applications/MultiSet.agda
@@ -2,7 +2,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Relation.ZigZag.Applications.MultiSet where
 
-open import Cubical.Core.Everything
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
@@ -11,6 +10,7 @@ open import Cubical.Foundations.RelationalStructure
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.SIP
 open import Cubical.Foundations.Univalence
+
 open import Cubical.Data.Unit
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
@@ -20,6 +20,7 @@ open import Cubical.HITs.SetQuotients
 open import Cubical.HITs.FiniteMultiset as FMS hiding ([_] ; _++_)
 open import Cubical.HITs.FiniteMultiset.CountExtensionality
 open import Cubical.HITs.PropositionalTruncation
+
 open import Cubical.Relation.Nullary
 open import Cubical.Relation.ZigZag.Base
 
diff --git a/Cubical/Relation/ZigZag/Base.agda b/Cubical/Relation/ZigZag/Base.agda
index a13ff42989..257be78f87 100644
--- a/Cubical/Relation/ZigZag/Base.agda
+++ b/Cubical/Relation/ZigZag/Base.agda
@@ -3,12 +3,14 @@
 {-# OPTIONS --safe #-}
 module Cubical.Relation.ZigZag.Base where
 
-open import Cubical.Core.Everything
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+
 open import Cubical.Data.Sigma
+
 open import Cubical.HITs.SetQuotients
 open import Cubical.HITs.PropositionalTruncation as Trunc
 open import Cubical.Relation.Binary.Base
diff --git a/GNUmakefile b/GNUmakefile
index ac20959549..f9d8a6e9b5 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -35,12 +35,12 @@ check-everythings:
 
 .PHONY : gen-everythings
 gen-everythings:
-	$(EVERYTHINGS) gen-except Core Codata
+	$(EVERYTHINGS) gen-except Codata
 
 .PHONY : gen-and-check-everythings
 gen-and-check-everythings:
-	$(EVERYTHINGS) gen-except Core Codata
-	$(EVERYTHINGS) check Core Codata
+	$(EVERYTHINGS) gen-except Codata
+	$(EVERYTHINGS) check Codata
 
 .PHONY : check-README
 check-README:

From 9181ef85d9979f849bb37056cd69120861b77b3a Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 13 May 2024 15:42:03 +0200
Subject: [PATCH 07/11] fix imports

---
 Cubical/Codata/Conat/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/Codata/Conat/Base.agda b/Cubical/Codata/Conat/Base.agda
index fdb5ec5fa6..ea21bafe9f 100644
--- a/Cubical/Codata/Conat/Base.agda
+++ b/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

From ee26992597f93537b53cf1049f9712733de42957 Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 13 May 2024 16:13:48 +0200
Subject: [PATCH 08/11] fix imports

---
 Cubical/Papers/Pi4S3.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Papers/Pi4S3.agda b/Cubical/Papers/Pi4S3.agda
index a1c4ecc21d..677d0b4968 100644
--- a/Cubical/Papers/Pi4S3.agda
+++ b/Cubical/Papers/Pi4S3.agda
@@ -19,7 +19,7 @@ module Cubical.Papers.Pi4S3 where
 open import Cubical.Data.Int hiding (_+_)
 open import Cubical.Data.Nat
 open import Cubical.Data.Nat.Order
-open import Cubical.Foundations.Everything
+open import Cubical.Foundations.Equiv
 open import Cubical.Data.Sum
 open import Cubical.Data.Sigma
 

From 4b6a4881840145de3df61f034337f7f6ed0538cb Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 13 May 2024 16:24:37 +0200
Subject: [PATCH 09/11] fix imports

---
 Cubical/Papers/Pi4S3.agda | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Cubical/Papers/Pi4S3.agda b/Cubical/Papers/Pi4S3.agda
index 677d0b4968..6bcc7e8642 100644
--- a/Cubical/Papers/Pi4S3.agda
+++ b/Cubical/Papers/Pi4S3.agda
@@ -16,10 +16,15 @@ Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical A
 module Cubical.Papers.Pi4S3 where
 
 -- Misc.
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.HLevels
+
 open import Cubical.Data.Int hiding (_+_)
 open import Cubical.Data.Nat
 open import Cubical.Data.Nat.Order
-open import Cubical.Foundations.Equiv
 open import Cubical.Data.Sum
 open import Cubical.Data.Sigma
 

From 0603aadb8964f783ab5d8f7c6ffa95676efd6760 Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Mon, 13 May 2024 17:12:38 +0200
Subject: [PATCH 10/11] fix imports

---
 Cubical/Papers/ZCohomology.agda | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/Cubical/Papers/ZCohomology.agda b/Cubical/Papers/ZCohomology.agda
index 97d9a9dfd9..347427d55e 100644
--- a/Cubical/Papers/ZCohomology.agda
+++ b/Cubical/Papers/ZCohomology.agda
@@ -20,18 +20,17 @@ module Cubical.Papers.ZCohomology where
 -- Misc.
 open import Cubical.Data.Int hiding (_+_)
 open import Cubical.Data.Nat
-open import Cubical.Foundations.Everything
 open import Cubical.HITs.S1
 open import Cubical.Data.Sum
 open import Cubical.Data.Sigma
 
 -- 2
 open import Cubical.Core.Glue                                as Glue
-import Cubical.Foundations.Prelude                           as Prelude
-import Cubical.Foundations.GroupoidLaws                      as GroupoidLaws
+open import Cubical.Foundations.Prelude                      as Prelude
+open import Cubical.Foundations.GroupoidLaws                 as GroupoidLaws
+open import Cubical.Foundations.Isomorphism
 import Cubical.Foundations.Path                              as Path
-import Cubical.Foundations.Pointed                           as Pointed
-  renaming (Pointed to Type∙)
+open import Cubical.Foundations.Pointed
 open import Cubical.HITs.S1                                  as S1
 open import Cubical.HITs.Susp                                as Suspension
 open import Cubical.HITs.Sn                                  as Sn
@@ -108,9 +107,6 @@ open Prelude using ( transport
 
 --- 2.2 Important concepts from HoTT/UF in Cubical Agda
 
--- Pointed Types
-open Pointed using (Type∙)
-
 -- The circle, 𝕊¹
 open S1 using (S¹)
 
@@ -356,7 +352,7 @@ open Cup using (_⌣_)
 
 -- 4.2
 -- Lemma 14
-Lem14 : ∀ {ℓ} {A : Type∙ ℓ} (n : ℕ) (f g : A →∙ K∙ n) → fst f ≡ fst g → f ≡ g
+Lem14 : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (f g : A →∙ K∙ n) → fst f ≡ fst g → f ≡ g
 Lem14 n f g p = Homogen.→∙Homogeneous≡ (Properties.isHomogeneousKn n) p
 
 -- Proposition 15

From 6fd7080d6802d933c53668f159ec043a512c8d1b Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Tue, 14 May 2024 21:49:20 +0200
Subject: [PATCH 11/11] fix imports

---
 Cubical/Relation/ZigZag/Applications/MultiSet.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cubical/Relation/ZigZag/Applications/MultiSet.agda b/Cubical/Relation/ZigZag/Applications/MultiSet.agda
index 104f5464af..270472e60f 100644
--- a/Cubical/Relation/ZigZag/Applications/MultiSet.agda
+++ b/Cubical/Relation/ZigZag/Applications/MultiSet.agda
@@ -9,6 +9,7 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.RelationalStructure
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.SIP
+open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Univalence
 
 open import Cubical.Data.Unit