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] 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))