The General Extend Operation (a.k.a. The Cube-Filling Macro)

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

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
+{-
+
+-- to conveniently present 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 _
-  {X : I → I → Type}
+  (ϕ : 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)