diff --git a/examples/Cubical/Examples/Category.agda b/examples/Cubical/Examples/Category.agda
index 6de8985..2ae521a 100644
--- a/examples/Cubical/Examples/Category.agda
+++ b/examples/Cubical/Examples/Category.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical #-}
 module Cubical.Examples.Category where
 
-open import PathPrelude
+open import Cubical.FromStdLib
+open import Cubical.PathPrelude
 
 -- Functor
 record Func {ℓ} : Set (ℓ-suc ℓ) where
@@ -56,19 +57,21 @@ G ∘ᶠ F = record
           module G = Func G
 
 idᶠLeft : ∀{ℓ}{F : Func {ℓ}} → idᶠ ∘ᶠ F ≡ F
-idᶠLeft {ℓ} {F} = Func≡.path r where
+idᶠLeft {ℓ} {F} =
+  directpath where
+  -- Func≡.path r where
   module L = Func (idᶠ ∘ᶠ F)
   module R = Func F
-  map≡ : L.map ≡ R.map
-  map≡ = funExt (λ _ → refl)
-  r = record { F         = idᶠ ∘ᶠ F
-             ; G         = F
-             ; map≡      = λ A → refl
-             ; fmap≡     = λ f → funExt λ _ → refl
-             ; presId≡   = λ A → {!!}
-             ; presComp≡ = λ f g → {!!}
-             }
-  open import Comp
+  -- map≡ : L.map ≡ R.map
+  -- map≡ = funExt (λ _ → refl)
+  -- r = record { F         = idᶠ ∘ᶠ F
+  --            ; G         = F
+  --            ; map≡      = λ A → refl
+  --            ; fmap≡     = λ f → funExt λ _ → refl
+  --            ; presId≡   = λ A → {!!}
+  --            ; presComp≡ = λ f g → {!!}
+  --            }
+  open import Cubical.Comp as Comp
 
   trans-id : ∀ {ℓ}{A : Set ℓ} {x y : A} → (p : x ≡ y) → trans p (\ i → y) ≡ p
   trans-id {A = A} {x} {y} p i j = Comp.fill (λ _ → A) _
diff --git a/examples/Cubical/Examples/Cube.agda b/examples/Cubical/Examples/Cube.agda
index e52ffbd..60504af 100644
--- a/examples/Cubical/Examples/Cube.agda
+++ b/examples/Cubical/Examples/Cube.agda
@@ -3,6 +3,7 @@ module Cubical.Examples.Cube where
 
 open import Cubical.PathPrelude
 open import Cubical.Id
+open import Cubical.FromStdLib
 
 test-sym : ∀ {ℓ} {A : Set ℓ} → {x y : A} → (p : x ≡ y) → sym (sym p) ≡ p
 test-sym p = refl
diff --git a/examples/Cubical/Examples/Everything.agda b/examples/Cubical/Examples/Everything.agda
index c039501..20d5887 100644
--- a/examples/Cubical/Examples/Everything.agda
+++ b/examples/Cubical/Examples/Everything.agda
@@ -14,6 +14,12 @@ open import Cubical.Examples.Cube
 open import Cubical.Examples.OTTU
 
 open import Cubical.Examples.BinNat
+open import Cubical.Examples.Int
+open import Cubical.Examples.SizedStream
+
+open import Cubical.Examples.Category
+open import Cubical.Examples.FunctorCWF
+
 
 -- Demo
 open import Cubical.Examples.AIM_Demo.DemoPath
diff --git a/examples/Cubical/Examples/FunctorCWF.agda b/examples/Cubical/Examples/FunctorCWF.agda
index 966f245..8e2e69f 100644
--- a/examples/Cubical/Examples/FunctorCWF.agda
+++ b/examples/Cubical/Examples/FunctorCWF.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical #-}
-module FunctorCWF where
+module Cubical.Examples.FunctorCWF where
 
-open import PathPrelude hiding (_∘_)
+open import Cubical.PathPrelude
+open import Cubical.FromStdLib hiding (_∘_)
 
 Σ= : ∀ {a b} {A : Set a} {B : A → Set b} {x y : Σ A B} (eq : x .fst ≡ y .fst)
      → PathP (\ i → B (eq i)) (x .snd) (y .snd) → x ≡ y
diff --git a/examples/Cubical/Examples/OTTU.agda b/examples/Cubical/Examples/OTTU.agda
index 68bbada..0bfd41d 100644
--- a/examples/Cubical/Examples/OTTU.agda
+++ b/examples/Cubical/Examples/OTTU.agda
@@ -2,6 +2,7 @@
 module Cubical.Examples.OTTU where
 
 open import Cubical.PathPrelude
+open import Cubical.FromStdLib
 
 open import Cubical.Examples.Cube
 
diff --git a/examples/Cubical/Examples/SizedStream.agda b/examples/Cubical/Examples/SizedStream.agda
index dd2404d..d248f95 100644
--- a/examples/Cubical/Examples/SizedStream.agda
+++ b/examples/Cubical/Examples/SizedStream.agda
@@ -1,9 +1,9 @@
 {-# OPTIONS --cubical #-}
-module SizedStream where
+module Cubical.Examples.SizedStream where
 
-open import Data.Product using (_×_)
-open import PathPrelude
-open import Size
+open import Cubical.PathPrelude
+open import Cubical.FromStdLib using (_×_)
+open import Agda.Builtin.Size
 
 record Stream (A : Set) (i : Size) : Set where
   coinductive
diff --git a/examples/Cubical/Examples/Stream.agda b/examples/Cubical/Examples/Stream.agda
index 0a2edfe..2fcaf78 100644
--- a/examples/Cubical/Examples/Stream.agda
+++ b/examples/Cubical/Examples/Stream.agda
@@ -2,7 +2,7 @@
 
 module Cubical.Examples.Stream where
 
-open import Cubical.FromStdLib using (_×_)
+open import Cubical.FromStdLib using (_×_; ℕ; zero; suc)
 open import Cubical.PathPrelude