From 9241ba1cdbc70f3a037f4f0fa2fafb195a426125 Mon Sep 17 00:00:00 2001
From: kangrongji <smallpigkang@gmail.com>
Date: Wed, 20 Sep 2023 00:47:27 +0800
Subject: [PATCH 1/6] done

---
 Cubical/Foundations/Everything.agda           |   1 +
 Cubical/Foundations/HLevels/Extend.agda       | 159 +++++++-------
 .../HLevels/ExtendConstruction.agda           | 206 ++++++++++++++++++
 3 files changed, 289 insertions(+), 77 deletions(-)
 create mode 100644 Cubical/Foundations/HLevels/ExtendConstruction.agda

diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda
index fb8d41e6d7..ba404b2497 100644
--- a/Cubical/Foundations/Everything.agda
+++ b/Cubical/Foundations/Everything.agda
@@ -14,6 +14,7 @@ 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.HLevels.ExtendConstruction
 open import Cubical.Foundations.Path public
 open import Cubical.Foundations.Pointed public
 open import Cubical.Foundations.RelationalStructure public
diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda
index ebdae59c6e..c013d24819 100644
--- a/Cubical/Foundations/HLevels/Extend.agda
+++ b/Cubical/Foundations/HLevels/Extend.agda
@@ -2,109 +2,114 @@
 
 Kan Operations for n-Truncated Types
 
-It provides an efficient way to construct cubes in truncated types.
+This file contain the `extend` operation
+that provides an efficient way to construct cubes in truncated types.
+It is a meta-theorem of Cubical Agda's type theory.
+The detail of construction is collected in
+  `Cubical.Foundations.HLevels.ExtendConstruction`.
 
 A draft note on this can be found online at
-https://kangrongji.github.io/files/extend-operations.pdf
+  https://kangrongji.github.io/files/extend-operations.pdf
 
 -}
 {-# OPTIONS --safe #-}
 module Cubical.Foundations.HLevels.Extend where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.HLevels hiding (extend)
+open import Cubical.Foundations.HLevels.ExtendConstruction
+open import Cubical.Data.Nat
+
+open import Agda.Builtin.List
+open import Agda.Builtin.Reflection hiding (Type)
+open import Cubical.Reflection.Base
+
 
 private
   variable
     ℓ : Level
 
 
--- For conveniently representing the boundary of cubes
+{-
+
+-- for conveniently representing the boundary of cubes
+
 ∂ : I → I
 ∂ i = i ∨ ~ i
 
+-}
 
--- TODO: Write a macro to generate these stuff.
 
-module _
-  {X : Type ℓ}
-  (h : isContr X)
-  {ϕ : I} where
+-- Transform internal ℕural numbers to external ones
+-- In fact it's impossible in Agda's 2LTT, so we could only use a macro.
+
+ℕ→MetaℕTerm : ℕ → Term
+ℕ→MetaℕTerm 0 = quoteTerm Metaℕ.zero
+ℕ→MetaℕTerm (suc n) = con (quote Metaℕ.suc) (ℕ→MetaℕTerm n v∷ [])
+
+macro
+  ℕ→Metaℕ : ℕ → Term → TC Unit
+  ℕ→Metaℕ n t = unify t (ℕ→MetaℕTerm n)
+
 
-  extend₀ :
-    (x : Partial _ X)
-    → X [ ϕ ↦ x ]
-  extend₀ = extend h _
 
+-- This `extend` operation "using internal natural number as index"
 
-module _
+macro
+  extend : (n : ℕ) → Term → TC Unit
+  extend n t = unify t
+    (def (quote extendCurried) (ℕ→MetaℕTerm n v∷ []))
+
+
+{-
+
+The type of `extend` operation could be understood as:
+
+extend :
+  (n : ℕ) {ℓ : Level}
+  (X : (i₁ ... iₙ : I) → Type ℓ)
+  (h : (i₁ ... iₙ : I) → isOfHLevel n (X i₁ ... iₙ))
+  (ϕ : I)
+  (x : (i₁ ... iₙ : I) → Partial (ϕ ∨ ∂ i₁ ∨ ... ∨ ∂ iₙ) (X i₁ ... iₙ))
+  (i₁ ... iₙ : I) → X i₁ ... iₙ [ _ ↦ x i₁ ... iₙ ]
+
+-}
+
+
+-- `extendₙ` for small value of `n`
+
+
+extendContr :
+  {X : Type ℓ}
+  (h : isContr X)
+  (ϕ : I)
+  (x : Partial _ X)
+  → X [ ϕ ↦ x ]
+extendContr = extend 0
+
+extendProp :
   {X : I → Type ℓ}
   (h : (i : I) → isProp (X i))
-  {ϕ : I} where
-
-  extend₁ :
-    (x : (i : I) → Partial _ (X i))
-    (i : I) → X i [ ϕ ∨ ∂ i ↦ x i ]
-  extend₁ x i = inS (hcomp (λ j → λ
-    { (ϕ = i1) → h i (bottom i) (x i 1=1) j
-    ; (i = i0) → h i (bottom i) (x i 1=1) j
-    ; (i = i1) → h i (bottom i) (x i 1=1) j })
-    (bottom i))
-    where
-    bottom : (i : I) → X i
-    bottom i = isProp→PathP h (x i0 1=1) (x i1 1=1) i
-
-
-module _
+  (ϕ : I)
+  (x : (i : I) → Partial _ (X i))
+  (i : I) → X i [ ϕ ∨ ∂ i ↦ x i ]
+extendProp = extend 1
+
+extendSet :
   {X : I → I → Type}
   (h : (i j : I) → isSet (X i j))
-  {ϕ : I} where
-
-  extend₂ :
-    (x : (i j : I) → Partial _ (X i j))
-    (i j : I) → X i j [ ϕ ∨ ∂ i ∨ ∂ j ↦ x i j ]
-  extend₂ x i j = inS (outS (extend₁PathP p i) j)
-    where
-    isOfHLevel₁PathP : (i : I) (a : X i i0) (b : X i i1)
-      → isProp (PathP (λ j → X i j) a b)
-    isOfHLevel₁PathP i = isOfHLevelPathP' 1 (h i i1)
-
-    extend₁PathP :
-      (p : (i : I) → Partial _ (PathP _ (x i i0 1=1) (x i i1 1=1)))
-      (i : I) → PathP _ (x i i0 1=1) (x i i1 1=1) [ ϕ ∨ ∂ i ↦ p i ]
-    extend₁PathP = extend₁ (λ i → isOfHLevel₁PathP i (x i i0 1=1) (x i i1 1=1)) {ϕ}
-
-    p : (i : I) → Partial _ (PathP _ (x i i0 1=1) (x i i1 1=1))
-    p i (i = i0) = λ j → x i j 1=1
-    p i (i = i1) = λ j → x i j 1=1
-    p i (ϕ = i1) = λ j → x i j 1=1
-
-
-module _
-  (X : I → I → I → Type)
+  (ϕ : I)
+  (x : (i j : I) → Partial _ (X i j))
+  (i j : I) → X i j [ ϕ ∨ ∂ i ∨ ∂ j ↦ x i j ]
+extendSet = extend 2
+
+extendGroupoid :
+  {X : I → I → I → Type}
   (h : (i j k : I) → isGroupoid (X i j k))
-  {ϕ : I} where
-
-  extend₃ :
-    (x : (i j k : I) → Partial _ (X i j k))
-    (i j k : I) → X i j k [ ϕ ∨ ∂ i ∨ ∂ j ∨ ∂ k ↦ x i j k ]
-  extend₃ x i j k = inS (outS (extend₂PathP p i j) k)
-    where
-    isOfHLevel₂PathP : (i j : I) (a : X i j i0) (b : X i j i1)
-      → isSet (PathP (λ k → X i j k) a b)
-    isOfHLevel₂PathP i j = isOfHLevelPathP' 2 (h i j i1)
-
-    extend₂PathP :
-      (p : (i j : I) → Partial _ (PathP _ (x i j i0 1=1) (x i j i1 1=1)))
-      (i j : I) → PathP _ (x i j i0 1=1) (x i j i1 1=1) [ ϕ ∨ ∂ i ∨ ∂ j ↦ p i j ]
-    extend₂PathP = extend₂ (λ i j → isOfHLevel₂PathP i j (x i j i0 1=1) (x i j i1 1=1)) {ϕ}
-
-    p : (i j : I) → Partial _ (PathP (λ k → X i j k) (x i j i0 1=1) (x i j i1 1=1))
-    p i j (i = i0) = λ k → x i j k 1=1
-    p i j (i = i1) = λ k → x i j k 1=1
-    p i j (j = i0) = λ k → x i j k 1=1
-    p i j (j = i1) = λ k → x i j k 1=1
-    p i j (ϕ = i1) = λ k → x i j k 1=1
+  (ϕ : I)
+  (x : (i j k : I) → Partial _ (X i j k))
+  (i j k : I) → X i j k [ ϕ ∨ ∂ i ∨ ∂ j ∨ ∂ k ↦ x i j k ]
+extendGroupoid = extend 3
 
 
 private
@@ -116,4 +121,4 @@ private
     (x : (i j k : I) → Partial _ X)
     (i j k : I) → X [ ∂ i ∨ ∂ j ∨ ∂ k ↦ x i j k ]
   isProp→Cube h x i j =
-    extend₁ (λ _ → h) {∂ i ∨ ∂ j} (x i j)
+    extendProp (λ _ → h) (∂ i ∨ ∂ j) (x i j)
diff --git a/Cubical/Foundations/HLevels/ExtendConstruction.agda b/Cubical/Foundations/HLevels/ExtendConstruction.agda
new file mode 100644
index 0000000000..e7a53c9f19
--- /dev/null
+++ b/Cubical/Foundations/HLevels/ExtendConstruction.agda
@@ -0,0 +1,206 @@
+{-
+
+The Construction of `extend` Operation
+
+To find explanation and examples, see `Cubical.Foundations.HLevels.Extend`.
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Foundations.HLevels.ExtendConstruction where
+
+open import Cubical.Foundations.Prelude hiding (Cube)
+open import Cubical.Foundations.HLevels renaming (extend to extend₀)
+open import Cubical.Data.Nat
+
+
+private
+  variable
+    ℓ : Level
+
+
+-- for conveniently representing the boundary of cubes
+
+∂ : I → I
+∂ i = i ∨ ~ i
+
+
+-- The external natural number
+
+data Metaℕ : SSet where
+  zero : Metaℕ
+  suc  : (n : Metaℕ) → Metaℕ
+
+-- transform external to internal natural number
+toℕ : Metaℕ → ℕ
+toℕ  zero   = zero
+toℕ (suc n) = suc (toℕ n)
+
+
+{-
+
+The Uncurried Version of `extend`
+
+-}
+
+
+-- A cheating version of I × I × ... × I
+-- pattern matching makes things easy
+
+data Cube : Metaℕ → SSet where
+  ∙   : Cube zero
+  _,_ : {n : Metaℕ} → I → Cube n → Cube (suc n)
+
+-- The boundary cofibration
+
+bd :  {n : Metaℕ} → Cube n → I
+bd ∙ = i0
+bd (i , 𝓳) = bd 𝓳 ∨ ∂ i
+
+
+-- boundary with an extra cofibration, partial elements and extension types
+-- all non-fibrant
+
+module _ {n : Metaℕ} where
+
+  bdc : (ϕ : I) → Cube n → I
+  bdc ϕ 𝓲 = ϕ ∨ bd 𝓲
+
+  Part : (ϕ : I) → Cube n → Type ℓ → SSet ℓ
+  Part ϕ 𝓲 X = Partial (bdc ϕ 𝓲) X
+
+  Ext : (X : Type ℓ) (ϕ : I) (𝓲 : Cube n) → Part ϕ 𝓲 X → SSet ℓ
+  Ext X ϕ 𝓲 x = X [ bdc ϕ 𝓲 ↦ x ]
+
+
+-- methods to use in induction
+
+module _
+  {ϕ : I}
+  {X : I → Type ℓ}
+  (x : (i : I) → Partial (ϕ ∨ ∂ i) (X i))
+  where
+
+  toPathPart : Partial ϕ (PathP X (x i0 1=1) (x i1 1=1))
+  toPathPart 1=1 i = x i (IsOne1 _ (∂ i) 1=1)
+
+  toPathExt :
+    (p : PathP X (x i0 1=1) (x i1 1=1) [ ϕ ↦ toPathPart ])
+    (i : I) → X i [ ϕ ∨ ∂ i ↦ x i ]
+  toPathExt p i = inS (outS p i)
+
+module _
+  {n : Metaℕ} {ϕ : I}
+  (X : Cube (suc n) → Type ℓ)
+  (x : (𝓲 : Cube (suc n)) → Part ϕ 𝓲 (X 𝓲))
+  where
+
+  PathPFam : (𝓳 : Cube n) → Type ℓ
+  PathPFam 𝓳 = PathP (λ i → X (i , 𝓳)) (x (i0 , 𝓳) 1=1) (x (i1 , 𝓳) 1=1)
+
+  toPart :
+    (𝓳 : Cube n) → Part ϕ 𝓳 (PathPFam 𝓳)
+  toPart 𝓳 = toPathPart (λ i → x (i , 𝓳))
+
+  toExt :
+    (p : (𝓳 : Cube n) → Ext _ ϕ 𝓳 (toPathPart (λ i → x (i , 𝓳))))
+    (𝓲 : Cube (suc n)) → Ext _ ϕ 𝓲 (x 𝓲)
+  toExt p (i , 𝓳) = toPathExt (λ i → x (i , 𝓳)) (p 𝓳) i
+
+  isOfHLevelₙPathP :
+    (h : (𝓲 : Cube (suc n)) → isOfHLevel (toℕ (suc n)) (X 𝓲))
+    (𝓳 : Cube n) → isOfHLevel (toℕ n) (PathPFam 𝓳)
+  isOfHLevelₙPathP h 𝓳 = isOfHLevelPathP' _ (h (i1 , 𝓳)) _ _
+
+
+
+-- the uncurried `extend`
+
+extendUncurried :
+  {n : Metaℕ} {ϕ : I} {X : Cube n → Type ℓ}
+  (h : (𝓲 : Cube n) → isOfHLevel (toℕ n) (X 𝓲))
+  (x : (𝓲 : Cube n) → Part ϕ 𝓲 (X 𝓲))
+  (𝓲 : Cube n) → Ext _ ϕ 𝓲 (x 𝓲)
+extendUncurried {n = zero} h _ ∙ = extend₀ (h ∙) _ _
+extendUncurried {n = suc n} {ϕ} h x =
+  toExt {ϕ = ϕ} _ _ (extendUncurried {ϕ = ϕ} (isOfHLevelₙPathP {ϕ = ϕ} _ x h) _)
+
+
+
+{-
+
+The Curried Version of `extend`
+
+-}
+
+-- Tons of definitions to curry things
+
+CubeType : (ℓ : Level) → Metaℕ → Type (ℓ-suc ℓ)
+CubeType ℓ zero = Type ℓ
+CubeType ℓ (suc n) = I → CubeType ℓ n
+
+CubeTerm : {n : Metaℕ} → CubeType ℓ n → Type ℓ
+CubeTerm {n = zero} X = X
+CubeTerm {n = suc n} P = (i : I) → CubeTerm (P i)
+
+CubeSSet : (ℓ : Level) → Metaℕ → SSet (ℓ-suc ℓ)
+CubeSSet ℓ zero = SSet ℓ
+CubeSSet ℓ (suc n) = I → CubeSSet ℓ n
+
+CubeSTerm : {n : Metaℕ} → CubeSSet ℓ n → SSet ℓ
+CubeSTerm {n = zero} X = X
+CubeSTerm {n = suc n} P = (i : I) → CubeSTerm (P i)
+
+uncurryType : {n : Metaℕ} → CubeType ℓ n → Cube n → Type ℓ
+uncurryType {n = zero} X ∙ = X
+uncurryType {n = suc n} X (i , 𝓳) = uncurryType (X i) 𝓳
+
+
+isOfHLevelCubeType : (m : HLevel) {n : Metaℕ} → CubeType ℓ n → CubeType ℓ n
+isOfHLevelCubeType m {zero}  X = isOfHLevel m X
+isOfHLevelCubeType m {suc n} X i = isOfHLevelCubeType m (X i)
+
+PartCubeType : {n : Metaℕ} (ϕ : I) → CubeType ℓ n → CubeSSet ℓ n
+PartCubeType {n = zero}  ϕ X = Partial ϕ X
+PartCubeType {n = suc n} ϕ X i = PartCubeType (ϕ ∨ ∂ i) (X i)
+
+ExtCubeType : {n : Metaℕ} {ϕ : I} {X : CubeType ℓ n} → CubeSTerm (PartCubeType ϕ X) → CubeSSet ℓ n
+ExtCubeType {n = zero}  {ϕ} x = _ [ _ ↦ x ]
+ExtCubeType {n = suc n} {ϕ} x i = ExtCubeType {ϕ = ϕ ∨ ∂ i} (x i)
+
+
+uncurryIsOfHLevelCubeType :
+  (m : HLevel) {n : Metaℕ}
+  {X : CubeType ℓ n}
+  (h : CubeTerm (isOfHLevelCubeType m X))
+  (𝓲 : Cube n) → isOfHLevel m (uncurryType X 𝓲)
+uncurryIsOfHLevelCubeType m {n = zero} h ∙ = h
+uncurryIsOfHLevelCubeType m {n = suc n} h (i , 𝓳) =
+  uncurryIsOfHLevelCubeType m {n = n} (h i) _
+
+uncurryPart :
+  {ϕ : I} {n : Metaℕ}
+  {X : CubeType ℓ n}
+  (u : CubeSTerm (PartCubeType ϕ X))
+  (𝓲 : Cube n) → Part ϕ 𝓲 (uncurryType X 𝓲)
+uncurryPart {ϕ = ϕ} {zero} {X} u ∙ = u
+uncurryPart {ϕ = ϕ} {n = suc n} {X} u (i , 𝓳) = uncurryPart (u i) 𝓳
+
+curryExt :
+  {ϕ : I} {n : Metaℕ}
+  {X : CubeType ℓ n}
+  (u : CubeSTerm (PartCubeType ϕ X))
+  (x : (𝓲 : Cube n) → Ext _ ϕ 𝓲 (uncurryPart u 𝓲))
+  → CubeSTerm (ExtCubeType {X = X} u)
+curryExt {n = zero} _ x = x ∙
+curryExt {n = suc n} u x i = curryExt (u i) (λ 𝓳 → x (i , 𝓳))
+
+
+-- the curried `extend`
+
+extendCurried :
+  (n : Metaℕ) {ℓ : Level} {X : CubeType ℓ n}
+  (h : CubeTerm  (isOfHLevelCubeType (toℕ n) X))
+  (ϕ : I) (x : CubeSTerm (PartCubeType ϕ X))
+  → CubeSTerm (ExtCubeType {X = X} x)
+extendCurried n {X = X} h ϕ x =
+  curryExt {X = X} _ (extendUncurried {ϕ = ϕ} (uncurryIsOfHLevelCubeType _ h) (uncurryPart x))

From dcb5a35ee7e36d9b9073787143f74230669bc2b6 Mon Sep 17 00:00:00 2001
From: kangrongji <smallpigkang@gmail.com>
Date: Wed, 20 Sep 2023 01:13:47 +0800
Subject: [PATCH 2/6] typos

---
 Cubical/Foundations/HLevels/Extend.agda             | 2 +-
 Cubical/Foundations/HLevels/ExtendConstruction.agda | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda
index c013d24819..9ca9292238 100644
--- a/Cubical/Foundations/HLevels/Extend.agda
+++ b/Cubical/Foundations/HLevels/Extend.agda
@@ -32,7 +32,7 @@ private
 
 {-
 
--- for conveniently representing the boundary of cubes
+-- to conveniently present the boundary of cubes
 
 ∂ : I → I
 ∂ i = i ∨ ~ i
diff --git a/Cubical/Foundations/HLevels/ExtendConstruction.agda b/Cubical/Foundations/HLevels/ExtendConstruction.agda
index e7a53c9f19..ff2261d8a2 100644
--- a/Cubical/Foundations/HLevels/ExtendConstruction.agda
+++ b/Cubical/Foundations/HLevels/ExtendConstruction.agda
@@ -18,7 +18,7 @@ private
     ℓ : Level
 
 
--- for conveniently representing the boundary of cubes
+-- to conveniently present the boundary of cubes
 
 ∂ : I → I
 ∂ i = i ∨ ~ i
@@ -30,7 +30,7 @@ data Metaℕ : SSet where
   zero : Metaℕ
   suc  : (n : Metaℕ) → Metaℕ
 
--- transform external to internal natural number
+-- transform external natural numbers to internal ones
 toℕ : Metaℕ → ℕ
 toℕ  zero   = zero
 toℕ (suc n) = suc (toℕ n)
@@ -72,7 +72,7 @@ module _ {n : Metaℕ} where
   Ext X ϕ 𝓲 x = X [ bdc ϕ 𝓲 ↦ x ]
 
 
--- methods to use in induction
+-- methods to be used in induction
 
 module _
   {ϕ : I}

From 297cf9037fb781f1e0c08fffb2c80b14726736a6 Mon Sep 17 00:00:00 2001
From: kangrongji <smallpigkang@gmail.com>
Date: Wed, 20 Sep 2023 01:32:11 +0800
Subject: [PATCH 3/6] space

---
 Cubical/Foundations/HLevels/ExtendConstruction.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Cubical/Foundations/HLevels/ExtendConstruction.agda b/Cubical/Foundations/HLevels/ExtendConstruction.agda
index ff2261d8a2..d5b2671e9e 100644
--- a/Cubical/Foundations/HLevels/ExtendConstruction.agda
+++ b/Cubical/Foundations/HLevels/ExtendConstruction.agda
@@ -112,7 +112,6 @@ module _
   isOfHLevelₙPathP h 𝓳 = isOfHLevelPathP' _ (h (i1 , 𝓳)) _ _
 
 
-
 -- the uncurried `extend`
 
 extendUncurried :
@@ -125,7 +124,6 @@ extendUncurried {n = suc n} {ϕ} h x =
   toExt {ϕ = ϕ} _ _ (extendUncurried {ϕ = ϕ} (isOfHLevelₙPathP {ϕ = ϕ} _ x h) _)
 
 
-
 {-
 
 The Curried Version of `extend`

From 9cf1d730b884451ad40d51bb08b52d60898b7398 Mon Sep 17 00:00:00 2001
From: kangrongji <smallpigkang@gmail.com>
Date: Wed, 20 Sep 2023 01:34:45 +0800
Subject: [PATCH 4/6] long-lines

---
 Cubical/Foundations/HLevels/ExtendConstruction.agda | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Cubical/Foundations/HLevels/ExtendConstruction.agda b/Cubical/Foundations/HLevels/ExtendConstruction.agda
index d5b2671e9e..8371cdbfae 100644
--- a/Cubical/Foundations/HLevels/ExtendConstruction.agda
+++ b/Cubical/Foundations/HLevels/ExtendConstruction.agda
@@ -130,7 +130,7 @@ The Curried Version of `extend`
 
 -}
 
--- Tons of definitions to curry things
+-- Tons of definitions to curry/uncurry things
 
 CubeType : (ℓ : Level) → Metaℕ → Type (ℓ-suc ℓ)
 CubeType ℓ zero = Type ℓ
@@ -161,7 +161,8 @@ PartCubeType : {n : Metaℕ} (ϕ : I) → CubeType ℓ n → CubeSSet ℓ n
 PartCubeType {n = zero}  ϕ X = Partial ϕ X
 PartCubeType {n = suc n} ϕ X i = PartCubeType (ϕ ∨ ∂ i) (X i)
 
-ExtCubeType : {n : Metaℕ} {ϕ : I} {X : CubeType ℓ n} → CubeSTerm (PartCubeType ϕ X) → CubeSSet ℓ n
+ExtCubeType : {n : Metaℕ} {ϕ : I} {X : CubeType ℓ n}
+  → CubeSTerm (PartCubeType ϕ X) → CubeSSet ℓ n
 ExtCubeType {n = zero}  {ϕ} x = _ [ _ ↦ x ]
 ExtCubeType {n = suc n} {ϕ} x i = ExtCubeType {ϕ = ϕ ∨ ∂ i} (x i)
 
@@ -197,8 +198,9 @@ curryExt {n = suc n} u x i = curryExt (u i) (λ 𝓳 → x (i , 𝓳))
 
 extendCurried :
   (n : Metaℕ) {ℓ : Level} {X : CubeType ℓ n}
-  (h : CubeTerm  (isOfHLevelCubeType (toℕ n) X))
+  (h : CubeTerm (isOfHLevelCubeType (toℕ n) X))
   (ϕ : I) (x : CubeSTerm (PartCubeType ϕ X))
   → CubeSTerm (ExtCubeType {X = X} x)
 extendCurried n {X = X} h ϕ x =
-  curryExt {X = X} _ (extendUncurried {ϕ = ϕ} (uncurryIsOfHLevelCubeType _ h) (uncurryPart x))
+  curryExt {X = X} _
+    (extendUncurried {ϕ = ϕ} (uncurryIsOfHLevelCubeType _ h) (uncurryPart x))

From 223e7b339185ab4ecac61905f6380db633b3581c Mon Sep 17 00:00:00 2001
From: kangrongji <smallpigkang@gmail.com>
Date: Wed, 20 Sep 2023 02:59:50 +0800
Subject: [PATCH 5/6] make more implicit

---
 .../HLevels/ExtendConstruction.agda           | 79 +++++++++----------
 1 file changed, 37 insertions(+), 42 deletions(-)

diff --git a/Cubical/Foundations/HLevels/ExtendConstruction.agda b/Cubical/Foundations/HLevels/ExtendConstruction.agda
index 8371cdbfae..5440c71dda 100644
--- a/Cubical/Foundations/HLevels/ExtendConstruction.agda
+++ b/Cubical/Foundations/HLevels/ExtendConstruction.agda
@@ -31,6 +31,7 @@ data Metaℕ : SSet where
   suc  : (n : Metaℕ) → Metaℕ
 
 -- transform external natural numbers to internal ones
+
 toℕ : Metaℕ → ℕ
 toℕ  zero   = zero
 toℕ (suc n) = suc (toℕ n)
@@ -44,40 +45,36 @@ The Uncurried Version of `extend`
 
 
 -- A cheating version of I × I × ... × I
--- pattern matching makes things easy
+-- pattern matching makes things easy!
 
 data Cube : Metaℕ → SSet where
   ∙   : Cube zero
   _,_ : {n : Metaℕ} → I → Cube n → Cube (suc n)
 
--- The boundary cofibration
+-- the boundary cofibration
 
 bd :  {n : Metaℕ} → Cube n → I
 bd ∙ = i0
 bd (i , 𝓳) = bd 𝓳 ∨ ∂ i
 
 
--- boundary with an extra cofibration, partial elements and extension types
+-- partial elements and extension types
 -- all non-fibrant
 
 module _ {n : Metaℕ} where
 
-  bdc : (ϕ : I) → Cube n → I
-  bdc ϕ 𝓲 = ϕ ∨ bd 𝓲
-
   Part : (ϕ : I) → Cube n → Type ℓ → SSet ℓ
-  Part ϕ 𝓲 X = Partial (bdc ϕ 𝓲) X
+  Part ϕ 𝓲 X = Partial (ϕ ∨ bd 𝓲) X
 
   Ext : (X : Type ℓ) (ϕ : I) (𝓲 : Cube n) → Part ϕ 𝓲 X → SSet ℓ
-  Ext X ϕ 𝓲 x = X [ bdc ϕ 𝓲 ↦ x ]
+  Ext X ϕ 𝓲 x = X [ ϕ ∨ bd 𝓲 ↦ x ]
 
 
 -- methods to be used in induction
 
 module _
-  {ϕ : I}
   {X : I → Type ℓ}
-  (x : (i : I) → Partial (ϕ ∨ ∂ i) (X i))
+  {ϕ : I} (x : (i : I) → Partial (ϕ ∨ ∂ i) (X i))
   where
 
   toPathPart : Partial ϕ (PathP X (x i0 1=1) (x i1 1=1))
@@ -88,10 +85,10 @@ module _
     (i : I) → X i [ ϕ ∨ ∂ i ↦ x i ]
   toPathExt p i = inS (outS p i)
 
+
 module _
-  {n : Metaℕ} {ϕ : I}
-  (X : Cube (suc n) → Type ℓ)
-  (x : (𝓲 : Cube (suc n)) → Part ϕ 𝓲 (X 𝓲))
+  {n : Metaℕ} {X : Cube (suc n) → Type ℓ}
+  (ϕ : I) (x : (𝓲 : Cube (suc n)) → Part ϕ 𝓲 (X 𝓲))
   where
 
   PathPFam : (𝓳 : Cube n) → Type ℓ
@@ -115,13 +112,13 @@ module _
 -- the uncurried `extend`
 
 extendUncurried :
-  {n : Metaℕ} {ϕ : I} {X : Cube n → Type ℓ}
+  {n : Metaℕ} {ℓ : Level} {X : Cube n → Type ℓ}
   (h : (𝓲 : Cube n) → isOfHLevel (toℕ n) (X 𝓲))
-  (x : (𝓲 : Cube n) → Part ϕ 𝓲 (X 𝓲))
+  (ϕ : I) (x : (𝓲 : Cube n) → Part ϕ 𝓲 (X 𝓲))
   (𝓲 : Cube n) → Ext _ ϕ 𝓲 (x 𝓲)
-extendUncurried {n = zero} h _ ∙ = extend₀ (h ∙) _ _
-extendUncurried {n = suc n} {ϕ} h x =
-  toExt {ϕ = ϕ} _ _ (extendUncurried {ϕ = ϕ} (isOfHLevelₙPathP {ϕ = ϕ} _ x h) _)
+extendUncurried {zero}  h _ _ ∙ = extend₀ (h ∙) _ _
+extendUncurried {suc n} h ϕ x =
+  toExt ϕ _ (extendUncurried (isOfHLevelₙPathP ϕ x h) ϕ _)
 
 
 {-
@@ -133,38 +130,38 @@ The Curried Version of `extend`
 -- Tons of definitions to curry/uncurry things
 
 CubeType : (ℓ : Level) → Metaℕ → Type (ℓ-suc ℓ)
-CubeType ℓ zero = Type ℓ
+CubeType ℓ  zero   = Type ℓ
 CubeType ℓ (suc n) = I → CubeType ℓ n
 
 CubeTerm : {n : Metaℕ} → CubeType ℓ n → Type ℓ
-CubeTerm {n = zero} X = X
+CubeTerm {n = zero}  X = X
 CubeTerm {n = suc n} P = (i : I) → CubeTerm (P i)
 
 CubeSSet : (ℓ : Level) → Metaℕ → SSet (ℓ-suc ℓ)
-CubeSSet ℓ zero = SSet ℓ
+CubeSSet ℓ  zero   = SSet ℓ
 CubeSSet ℓ (suc n) = I → CubeSSet ℓ n
 
 CubeSTerm : {n : Metaℕ} → CubeSSet ℓ n → SSet ℓ
-CubeSTerm {n = zero} X = X
+CubeSTerm {n = zero}  X = X
 CubeSTerm {n = suc n} P = (i : I) → CubeSTerm (P i)
 
 uncurryType : {n : Metaℕ} → CubeType ℓ n → Cube n → Type ℓ
-uncurryType {n = zero} X ∙ = X
+uncurryType {n = zero}  X ∙ = X
 uncurryType {n = suc n} X (i , 𝓳) = uncurryType (X i) 𝓳
 
 
 isOfHLevelCubeType : (m : HLevel) {n : Metaℕ} → CubeType ℓ n → CubeType ℓ n
-isOfHLevelCubeType m {zero}  X = isOfHLevel m X
+isOfHLevelCubeType m {zero}  X   = isOfHLevel m X
 isOfHLevelCubeType m {suc n} X i = isOfHLevelCubeType m (X i)
 
 PartCubeType : {n : Metaℕ} (ϕ : I) → CubeType ℓ n → CubeSSet ℓ n
-PartCubeType {n = zero}  ϕ X = Partial ϕ X
+PartCubeType {n = zero}  ϕ X   = Partial ϕ X
 PartCubeType {n = suc n} ϕ X i = PartCubeType (ϕ ∨ ∂ i) (X i)
 
 ExtCubeType : {n : Metaℕ} {ϕ : I} {X : CubeType ℓ n}
   → CubeSTerm (PartCubeType ϕ X) → CubeSSet ℓ n
-ExtCubeType {n = zero}  {ϕ} x = _ [ _ ↦ x ]
-ExtCubeType {n = suc n} {ϕ} x i = ExtCubeType {ϕ = ϕ ∨ ∂ i} (x i)
+ExtCubeType {n = zero}  x   = _ [ _ ↦ x ]
+ExtCubeType {n = suc n} x i = ExtCubeType (x i)
 
 
 uncurryIsOfHLevelCubeType :
@@ -172,25 +169,23 @@ uncurryIsOfHLevelCubeType :
   {X : CubeType ℓ n}
   (h : CubeTerm (isOfHLevelCubeType m X))
   (𝓲 : Cube n) → isOfHLevel m (uncurryType X 𝓲)
-uncurryIsOfHLevelCubeType m {n = zero} h ∙ = h
-uncurryIsOfHLevelCubeType m {n = suc n} h (i , 𝓳) =
-  uncurryIsOfHLevelCubeType m {n = n} (h i) _
+uncurryIsOfHLevelCubeType m h ∙ = h
+uncurryIsOfHLevelCubeType m h (i , 𝓳) =
+  uncurryIsOfHLevelCubeType m (h i) 𝓳
 
 uncurryPart :
-  {ϕ : I} {n : Metaℕ}
-  {X : CubeType ℓ n}
-  (u : CubeSTerm (PartCubeType ϕ X))
+  {n : Metaℕ} {X : CubeType ℓ n}
+  {ϕ : I} (u : CubeSTerm (PartCubeType ϕ X))
   (𝓲 : Cube n) → Part ϕ 𝓲 (uncurryType X 𝓲)
-uncurryPart {ϕ = ϕ} {zero} {X} u ∙ = u
-uncurryPart {ϕ = ϕ} {n = suc n} {X} u (i , 𝓳) = uncurryPart (u i) 𝓳
+uncurryPart u ∙ = u
+uncurryPart u (i , 𝓳) = uncurryPart (u i) 𝓳
 
 curryExt :
-  {ϕ : I} {n : Metaℕ}
-  {X : CubeType ℓ n}
-  (u : CubeSTerm (PartCubeType ϕ X))
+  {n : Metaℕ} {X : CubeType ℓ n}
+  {ϕ : I} (u : CubeSTerm (PartCubeType ϕ X))
   (x : (𝓲 : Cube n) → Ext _ ϕ 𝓲 (uncurryPart u 𝓲))
   → CubeSTerm (ExtCubeType {X = X} u)
-curryExt {n = zero} _ x = x ∙
+curryExt {n = zero}  _ x = x ∙
 curryExt {n = suc n} u x i = curryExt (u i) (λ 𝓳 → x (i , 𝓳))
 
 
@@ -201,6 +196,6 @@ extendCurried :
   (h : CubeTerm (isOfHLevelCubeType (toℕ n) X))
   (ϕ : I) (x : CubeSTerm (PartCubeType ϕ X))
   → CubeSTerm (ExtCubeType {X = X} x)
-extendCurried n {X = X} h ϕ x =
-  curryExt {X = X} _
-    (extendUncurried {ϕ = ϕ} (uncurryIsOfHLevelCubeType _ h) (uncurryPart x))
+extendCurried n h ϕ x =
+  curryExt {n = n} _
+    (extendUncurried (uncurryIsOfHLevelCubeType _ h) ϕ (uncurryPart x))

From b46c4bef58a73a659975b87127f32aa7bda7f56b Mon Sep 17 00:00:00 2001
From: kangrongji <smallpigkang@gmail.com>
Date: Wed, 20 Sep 2023 03:00:41 +0800
Subject: [PATCH 6/6] universe level

---
 Cubical/Foundations/HLevels/Extend.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda
index 9ca9292238..961bb72c61 100644
--- a/Cubical/Foundations/HLevels/Extend.agda
+++ b/Cubical/Foundations/HLevels/Extend.agda
@@ -96,7 +96,7 @@ extendProp :
 extendProp = extend 1
 
 extendSet :
-  {X : I → I → Type}
+  {X : I → I → Type ℓ}
   (h : (i j : I) → isSet (X i j))
   (ϕ : I)
   (x : (i j : I) → Partial _ (X i j))
@@ -104,7 +104,7 @@ extendSet :
 extendSet = extend 2
 
 extendGroupoid :
-  {X : I → I → I → Type}
+  {X : I → I → I → Type ℓ}
   (h : (i j k : I) → isGroupoid (X i j k))
   (ϕ : I)
   (x : (i j k : I) → Partial _ (X i j k))