diff --git a/Cubical/Foundations/Cubes.agda b/Cubical/Foundations/Cubes.agda
new file mode 100644
index 0000000000..f221cf5f71
--- /dev/null
+++ b/Cubical/Foundations/Cubes.agda
@@ -0,0 +1,190 @@
+{-
+
+The Internal n-Cubes
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Foundations.Cubes where
+
+open import Cubical.Foundations.Prelude hiding (Cube)
+open import Cubical.Foundations.Cubes.Base public
+open import Cubical.Data.Nat
+
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
+
+{-
+
+By mutual recursion, one can define the type of
+
+- n-Cubes:
+  Cube    : (n : ℕ) (A : Type ℓ) → Type ℓ
+
+- Boundary of n-cubes:
+  ∂Cube   : (n : ℕ) (A : Type ℓ) → Type ℓ
+
+- n-Cubes with Fixed Boundary:
+  CubeRel : (n : ℕ) (A : Type ℓ) → ∂Cube n A → Type ℓ
+
+Their definitions are put in `Cubical.Foundations.Cubes.Base`,
+to avoid cyclic dependence.
+
+-}
+
+
+{-
+
+  Relation with the external (partial) cubes
+
+-}
+
+-- Concatenate two sides and parts in between to get a partial element.
+concat :
+  {φ : I} (a₋ : (i : I) → Partial φ A)
+  (a₀ : A [ φ ↦ a₋ i0 ]) (a₁ : A [ φ ↦ a₋ i1 ])
+  (i : I) → Partial (i ∨ ~ i ∨ φ) A
+concat {φ = φ} a₋ a₀ a₁ i (i = i0) = outS a₀
+concat {φ = φ} a₋ a₀ a₁ i (i = i1) = outS a₁
+concat {φ = φ} a₋ a₀ a₁ i (φ = i1) = a₋ i 1=1
+
+-- And the reverse procedure.
+module _ (φ : I) (a₋ : (i : I) → Partial (i ∨ ~ i ∨ φ) A) where
+
+  detach₀ : A
+  detach₀ = a₋ i0 1=1
+
+  detach₁ : A
+  detach₁ = a₋ i1 1=1
+
+  detach₋ : (i : I) → Partial φ A
+  detach₋ i (φ = i1) = a₋ i 1=1
+
+
+{- Lower Cubes Back and Forth -}
+
+-- Notice that the functions are meta-inductively defined,
+-- except for the first two cases when n = 0 or 1.
+
+-- TODO : Write macros to generate them!!!
+
+from0Cube : Cube 0 A → A
+from0Cube p = p
+
+from1Cube : Cube 1 A → (i : I) → A
+from1Cube p i = p .snd i
+
+from2Cube : Cube 2 A → (i j : I) → A
+from2Cube p i j = p .snd i j
+
+from3Cube : Cube 3 A → (i j k : I) → A
+from3Cube p i j k = p .snd i j k
+
+from4Cube : Cube 4 A → (i j k l : I) → A
+from4Cube p i j k l = p .snd i j k l
+
+
+to0Cube : A → Cube 0 A
+to0Cube p = p
+
+to1Cube : ((i : I) → A) → Cube 1 A
+to1Cube p = (p i0 , p i1) , λ i → p i
+
+to2Cube : ((i j : I) → A) → Cube 2 A
+to2Cube p = pathCube 0 (λ i → (to1Cube (λ j → p i j)))
+
+to3Cube : ((i j k : I) → A) → Cube 3 A
+to3Cube p = pathCube 1 (λ i → (to2Cube (λ j → p i j)))
+
+to4Cube : ((i j k l : I) → A) → Cube 4 A
+to4Cube p = pathCube 2 (λ i → (to3Cube (λ j → p i j)))
+
+
+-- The 0-cube has no (or empty) boundary...
+
+from∂1Cube : ∂Cube 1 A → (i : I) → Partial (i ∨ ~ i) A
+from∂1Cube (a , b) i = λ { (i = i0) → a ; (i = i1) → b }
+
+from∂2Cube : ∂Cube 2 A → (i j : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A
+from∂2Cube (a₀ , a₁ , ∂₋) i j =
+  concat (λ t → from∂1Cube (∂₋ t) j)
+    (inS (from1Cube a₀ j)) (inS (from1Cube a₁ j)) i
+
+from∂3Cube : ∂Cube 3 A → (i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k) A
+from∂3Cube (a₀ , a₁ , ∂₋) i j k =
+  concat (λ t → from∂2Cube (∂₋ t) j k)
+    (inS (from2Cube a₀ j k)) (inS (from2Cube a₁ j k)) i
+
+from∂4Cube : ∂Cube 4 A → (i j k l : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) A
+from∂4Cube (a₀ , a₁ , ∂₋) i j k l =
+  concat (λ t → from∂3Cube (∂₋ t) j k l)
+    (inS (from3Cube a₀ j k l)) (inS (from3Cube a₁ j k l)) i
+
+
+to∂1Cube : ((i : I) → Partial (i ∨ ~ i) A) → ∂Cube 1 A
+to∂1Cube p = p i0 1=1 , p i1 1=1
+
+to∂2Cube : ((i j : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A) → ∂Cube 2 A
+to∂2Cube p .fst      = to1Cube (λ j → detach₀ (j ∨ ~ j) (λ i → p i j))
+to∂2Cube p .snd .fst = to1Cube (λ j → detach₁ (j ∨ ~ j) (λ i → p i j))
+to∂2Cube p .snd .snd t = to∂1Cube (λ j → detach₋ _ (λ i → p i j) t)
+
+to∂3Cube : ((i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k) A) → ∂Cube 3 A
+to∂3Cube p .fst      = to2Cube (λ j k → detach₀ (j ∨ ~ j ∨ k ∨ ~ k) (λ i → p i j k))
+to∂3Cube p .snd .fst = to2Cube (λ j k → detach₁ (j ∨ ~ j ∨ k ∨ ~ k) (λ i → p i j k))
+to∂3Cube p .snd .snd t = to∂2Cube (λ j k → detach₋ _ (λ i → p i j k) t)
+
+to∂4Cube : ((i j k l : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) A) → ∂Cube 4 A
+to∂4Cube p .fst      = to3Cube (λ j k l → detach₀ (j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) (λ i → p i j k l))
+to∂4Cube p .snd .fst = to3Cube (λ j k l → detach₁ (j ∨ ~ j ∨ k ∨ ~ k ∨ l ∨ ~ l) (λ i → p i j k l))
+to∂4Cube p .snd .snd t = to∂3Cube (λ j k l → detach₋ _ (λ i → p i j k l) t)
+
+
+-- They're strict isomorphisms actually.
+-- The following is an example.
+
+private
+
+  ret-2Cube : {A : Type ℓ} (a : Cube 2 A) → to2Cube (from2Cube a) ≡ a
+  ret-2Cube a = refl
+
+  sec-2Cube : (p : (i j : I) → A) → (i j : I) → from2Cube (to2Cube p) i j ≡ p i j
+  sec-2Cube p i j = refl
+
+  ret-∂2Cube : {A : Type ℓ} (a : ∂Cube 2 A) → to∂2Cube (from∂2Cube a) ≡ a
+  ret-∂2Cube a = refl
+
+  sec-∂2Cube : (p : (i j : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A)
+    → (i j : I) → PartialP (i ∨ ~ i ∨ j ∨ ~ j) (λ o → from∂2Cube (to∂2Cube p) i j o ≡ p i j o)
+  sec-∂2Cube p i j = λ
+    { (i = i0) → refl ; (i = i1) → refl ; (j = i0) → refl ; (j = i1) → refl }
+
+
+{-
+
+  The n-cubes-can-always-be-filled is equivalent to be of h-level n
+
+-}
+
+-- The property that, given an n-boundary, there always exists an n-cube extending this boundary
+-- The case n=0 is not very meaningful, so we use `isContr` instead to keep its relation with h-levels.
+
+isCubeFilled : ℕ → Type ℓ → Type ℓ
+isCubeFilled 0 = isContr
+isCubeFilled (suc n) A = (∂ : ∂Cube (suc n) A) → CubeRel (suc n) A ∂
+
+
+{-
+
+TODO:
+
+-- It's not too difficult to show this for a specific n,
+-- the trickiest part is to make it for all n.
+
+isOfHLevel→isCubeFilled : (n : HLevel) → isOfHLevel n A → isCubeFilled n A
+
+isCubeFilled→isOfHLevel : (n : HLevel) → isCubeFilled n A → isOfHLevel n A
+
+-}
diff --git a/Cubical/Foundations/Cubes/Base.agda b/Cubical/Foundations/Cubes/Base.agda
new file mode 100644
index 0000000000..37d1bd1f8a
--- /dev/null
+++ b/Cubical/Foundations/Cubes/Base.agda
@@ -0,0 +1,156 @@
+{-
+
+This file contains:
+
+- The definition of the type of n-cubes;
+
+- Some basic operations.
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Foundations.Cubes.Base where
+
+open import Cubical.Foundations.Prelude  hiding (Cube)
+open import Cubical.Foundations.Function hiding (const)
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Data.Nat.Base
+open import Cubical.Data.Sigma.Base
+
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
+
+-- The Type of n-Cubes
+
+-- P.S.
+-- Only the definitions of `∂Cube` and `CubeRel` essentially use mutual recursion.
+-- The case of `Cube` is designed to gain more definitional equality.
+
+interleaved mutual
+
+  Cube    : (n : ℕ) (A : Type ℓ) → Type ℓ
+  ∂Cube   : (n : ℕ) (A : Type ℓ) → Type ℓ
+  CubeRel : (n : ℕ) (A : Type ℓ) → ∂Cube n A → Type ℓ
+
+  Cube    0 A = A
+  Cube    (suc n) A = Σ[ ∂ ∈ ∂Cube (suc n) A ] CubeRel (suc n) A ∂
+
+  ∂Cube   0 A = Unit*
+  ∂Cube   1 A = A × A
+  ∂Cube   (suc (suc n)) A = Σ[ a₀ ∈ Cube (suc n) A ] Σ[ a₁ ∈ Cube (suc n) A ] a₀ .fst ≡ a₁ .fst
+
+  CubeRel 0 A _ = A
+  CubeRel 1 A ∂ = ∂ .fst ≡ ∂ .snd
+  CubeRel (suc (suc n)) A (a₀ , a₁ , ∂₋) = PathP (λ i → CubeRel (suc n) A (∂₋ i)) (a₀ .snd) (a₁ .snd)
+
+
+-- Some basic operations
+
+∂_ : {n : ℕ}{A : Type ℓ} → Cube n A → ∂Cube n A
+∂_ {n = 0} _ = tt*
+∂_ {n = suc n} = fst
+
+∂₀ : {n : ℕ}{A : Type ℓ} → Cube (suc n) A → Cube n A
+∂₀ {n = 0} (_ , p) = p i0
+∂₀ {n = suc n} (_ , p) = _ , p i0
+
+∂₁ : {n : ℕ}{A : Type ℓ} → Cube (suc n) A → Cube n A
+∂₁ {n = 0} (_ , p) = p i1
+∂₁ {n = suc n} (_ , p) = _ , p i1
+
+∂ᵇ₀ : {n : ℕ}{A : Type ℓ} → ∂Cube (suc n) A → Cube n A
+∂ᵇ₀ {n = 0} (a₀ , a₁) = a₀
+∂ᵇ₀ {n = suc n} (a₀ , a₁ , ∂₋) = a₀
+
+∂ᵇ₁ : {n : ℕ}{A : Type ℓ} → ∂Cube (suc n) A → Cube n A
+∂ᵇ₁ {n = 0} (a₀ , a₁) = a₁
+∂ᵇ₁ {n = suc n} (a₀ , a₁ , ∂₋) = a₁
+
+
+make∂ : {n : ℕ}{A : Type ℓ}{∂₀ ∂₁ : ∂Cube n A} → ∂₀ ≡ ∂₁ → CubeRel n A ∂₀ → CubeRel n A ∂₁ → ∂Cube (suc n) A
+make∂ {n = 0} _ a b = a , b
+make∂ {n = suc n} ∂₋ a₀ a₁ = (_ , a₀) , (_ , a₁) , ∂₋
+
+makeCube : {n : ℕ}{A : Type ℓ}{a₀ a₁ : Cube n A} → a₀ ≡ a₁ → Cube (suc n) A
+makeCube {n = 0} a₋ = _ , a₋
+makeCube {n = suc n} a₋ = _ , λ i → a₋ i .snd
+
+-- A cube is just a path of cubes of one-lower-dimension.
+-- Unfortunately the following function cannot begin at 0,
+-- because Agda doesn't support pattern matching on ℕ towards pre-types.
+-- P.S. It will be fixed in Agda 2.6.3 when I → A becomes fibrant.
+pathCube : (n : ℕ) → (I → Cube (suc n) A) → Cube (suc (suc n)) A
+pathCube n p = _ , λ i → p i .snd
+
+CubeRel→Cube : {n : ℕ}{A : Type ℓ}{∂ : ∂Cube n A} → CubeRel n A ∂ → Cube n A
+CubeRel→Cube {n = 0} a = a
+CubeRel→Cube {n = suc n} cube = _ , cube
+
+
+-- Composition of internal cubes, with specified boundary
+
+hcomp∂ :
+  {n : ℕ} {A : Type ℓ}
+  {∂₀ ∂₁ : ∂Cube n A} (∂₋ : ∂₀ ≡ ∂₁)
+  (a₀ : CubeRel n A ∂₀)
+  → CubeRel n A ∂₁
+hcomp∂ ∂₋ = transport (λ i → CubeRel _ _ (∂₋ i))
+
+hfill∂ :
+  {n : ℕ} {A : Type ℓ}
+  {∂₀ ∂₁ : ∂Cube n A} (∂₋ : ∂₀ ≡ ∂₁)
+  (a₀ : CubeRel n A ∂₀)
+  → CubeRel (suc n) A (make∂ ∂₋ a₀ (hcomp∂ ∂₋ a₀))
+hfill∂ {n = 0} ∂₋ a₀ i = transportRefl a₀ (~ i)
+hfill∂ {n = suc n} ∂₋  = transport-filler (λ i → CubeRel _ _ (∂₋ i))
+
+
+-- Constant path of n-cube as (n+1)-cube
+
+constCube : {n : ℕ}{A : Type ℓ} → Cube n A → Cube (suc n) A
+constCube {n = 0} a = _ , λ i → a
+constCube {n = suc n} (∂ , cube) = _ , λ i → cube
+
+retConst : {n : ℕ}{A : Type ℓ} → (cube : Cube n A) → ∂₀ (constCube {n = n} cube) ≡ cube
+retConst {n = 0} _ = refl
+retConst {n = suc n} _ = refl
+
+setConst : {n : ℕ}{A : Type ℓ} → (cube : Cube (suc n) A) → constCube (∂₀ cube) ≡ cube
+setConst {n = 0} (_ , p) i = _ , λ j → p (i ∧ j)
+setConst {n = suc n} (_ , p) i  = _ , λ j → p (i ∧ j)
+
+isEquivConstCube : {n : ℕ}{A : Type ℓ} → isEquiv (constCube {n = n} {A = A})
+isEquivConstCube {n = n} = isoToEquiv (iso constCube ∂₀ setConst (retConst {n = n})) .snd
+
+
+-- Constant cubes
+
+const : (n : ℕ){A : Type ℓ} → A → Cube n A
+const 0 a = a
+const (suc n) a = constCube (const n a)
+
+isEquivConst : {n : ℕ}{A : Type ℓ} → isEquiv (const n {A = A})
+isEquivConst {n = 0} = idIsEquiv _
+isEquivConst {n = suc n} = compEquiv (_ , isEquivConst) (_ , isEquivConstCube) .snd
+
+cubeEquiv : {n : ℕ}{A : Type ℓ} → A ≃ Cube n A
+cubeEquiv = _ , isEquivConst
+
+makeConst : {n : ℕ}{A : Type ℓ} → (cube : Cube n A) → Σ[ a ∈ A ] cube ≡ const n a
+makeConst {n = n} cube = invEq cubeEquiv cube , sym (secEq (cubeEquiv {n = n}) cube)
+
+makeConstUniq : {n : ℕ}{A : Type ℓ} → (a : A) → makeConst (const n a) ≡ (a , refl)
+makeConstUniq {n = n} a i .fst   = isEquivConst .equiv-proof (const n a) .snd (a , refl) i .fst
+makeConstUniq {n = n} a i .snd j = isEquivConst .equiv-proof (const n a) .snd (a , refl) i .snd (~ j)
+
+
+-- Cube with constant boundary
+
+const∂ : (n : ℕ){A : Type ℓ} → A → ∂Cube n A
+const∂ 0 _ = tt*
+const∂ 1 a = a , a
+const∂ (suc (suc n)) a = const _ a , const _ a , refl
diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda
index e123a95480..7e35572a53 100644
--- a/Cubical/Foundations/Everything.agda
+++ b/Cubical/Foundations/Everything.agda
@@ -50,3 +50,4 @@ 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