From c8173589b9a222e66ca8fb2f37b7d371b225bef1 Mon Sep 17 00:00:00 2001 From: kangrongji Date: Fri, 15 Sep 2023 01:06:09 +0800 Subject: [PATCH 1/7] done --- Cubical/Foundations/HLevels/Extend.agda | 102 ++++++++++++++++++++++++ 1 file changed, 102 insertions(+) create mode 100644 Cubical/Foundations/HLevels/Extend.agda diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda new file mode 100644 index 0000000000..fd1dc85226 --- /dev/null +++ b/Cubical/Foundations/HLevels/Extend.agda @@ -0,0 +1,102 @@ +{- + +Kan Operations for n-Truncated Types + +A draft note on this can be found at +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 renaming (extend to extend₀) + +private + variable + ℓ : Level + + +-- For easily representing boundary of cubes +∂ : I → I +∂ i = i ∨ ~ i + +-- TODO: Write a macro to generate these stuff + +module _ + {X : I → Type ℓ} + (h : (i : I) → isProp (X i)) + {ϕ : I} where + + extend₁ : + (x : (i : I) → Partial (ϕ ∨ ∂ i) (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 i0 (bottom i0) (x i0 1=1) j + ; (i = i1) → h i1 (bottom i1) (x i1 1=1) j }) + (bottom i)) + where + pd : (a : X i0) (b : X i1) → PathP X a b + pd a b i = (hcomp (λ j → λ + { (i = i0) → a + ; (i = i1) → h i1 (tp i1) b j }) + (tp i)) + where + tp : (i : I) → X i + tp i = transport-filler (λ i → X i) a i + + bottom : (i : I) → X i + bottom i = pd (x i0 1=1) (x i1 1=1) i + + +module _ + {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) + (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 From 89b4b4d1e69032fb72447ad568038ad7d948e68c Mon Sep 17 00:00:00 2001 From: kangrongji Date: Fri, 15 Sep 2023 01:24:36 +0800 Subject: [PATCH 2/7] fix Everything --- Cubical/Foundations/Everything.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda index 6f6889b8ff..fb8d41e6d7 100644 --- a/Cubical/Foundations/Everything.agda +++ b/Cubical/Foundations/Everything.agda @@ -13,6 +13,7 @@ open import Cubical.Foundations.Equiv.BiInvertible public 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.Path public open import Cubical.Foundations.Pointed public open import Cubical.Foundations.RelationalStructure public From 6fb02eefd0ce2fc3d5ba2e4d143709ef410849b9 Mon Sep 17 00:00:00 2001 From: kangrongji Date: Fri, 15 Sep 2023 23:32:18 +0800 Subject: [PATCH 3/7] update --- Cubical/Foundations/HLevels/Extend.agda | 34 ++++++++++++++----------- 1 file changed, 19 insertions(+), 15 deletions(-) diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda index fd1dc85226..3dbde1feb5 100644 --- a/Cubical/Foundations/HLevels/Extend.agda +++ b/Cubical/Foundations/HLevels/Extend.agda @@ -2,7 +2,9 @@ Kan Operations for n-Truncated Types -A draft note on this can be found at +They provide an efficient way to construct cubes within truncated types. + +A draft note on this can be found online at https://kangrongji.github.io/files/extend-operations.pdf -} @@ -10,7 +12,7 @@ https://kangrongji.github.io/files/extend-operations.pdf module Cubical.Foundations.HLevels.Extend where open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels renaming (extend to extend₀) +open import Cubical.Foundations.HLevels private variable @@ -23,6 +25,17 @@ private -- TODO: Write a macro to generate these stuff +module _ + {X : Type ℓ} + (h : isContr X) + {ϕ : I} where + + extend₀ : + (x : Partial ϕ X) + → X [ ϕ ↦ x ] + extend₀ = extend h _ + + module _ {X : I → Type ℓ} (h : (i : I) → isProp (X i)) @@ -32,22 +45,13 @@ module _ (x : (i : I) → Partial (ϕ ∨ ∂ i) (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 i0 (bottom i0) (x i0 1=1) j - ; (i = i1) → h i1 (bottom i1) (x i1 1=1) 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 - pd : (a : X i0) (b : X i1) → PathP X a b - pd a b i = (hcomp (λ j → λ - { (i = i0) → a - ; (i = i1) → h i1 (tp i1) b j }) - (tp i)) - where - tp : (i : I) → X i - tp i = transport-filler (λ i → X i) a i - bottom : (i : I) → X i - bottom i = pd (x i0 1=1) (x i1 1=1) i + bottom i = isProp→PathP h (x i0 1=1) (x i1 1=1) i module _ From 601555b66452888b169429310f577ca22381ed95 Mon Sep 17 00:00:00 2001 From: kangrongji Date: Fri, 15 Sep 2023 23:41:26 +0800 Subject: [PATCH 4/7] add an example --- Cubical/Foundations/HLevels/Extend.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda index 3dbde1feb5..fe754349be 100644 --- a/Cubical/Foundations/HLevels/Extend.agda +++ b/Cubical/Foundations/HLevels/Extend.agda @@ -104,3 +104,15 @@ module _ 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 + + +private + -- An example shows how to directly fill a 3-cube in a h-proposition. + -- It can help when one wants to pattern match HITs toward some n-types. + + isProp→Cube : + {X : Type ℓ} (h : isProp X) + (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) From aa4d2b2a0dff47d08d8e3902e387fff8f5e7168f Mon Sep 17 00:00:00 2001 From: kangrongji Date: Sat, 16 Sep 2023 00:08:48 +0800 Subject: [PATCH 5/7] fix --- Cubical/Foundations/HLevels/Extend.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda index fe754349be..3ec2d69ef4 100644 --- a/Cubical/Foundations/HLevels/Extend.agda +++ b/Cubical/Foundations/HLevels/Extend.agda @@ -107,12 +107,12 @@ module _ private - -- An example shows how to directly fill a 3-cube in a h-proposition. - -- It can help when one wants to pattern match HITs toward some n-types. + -- An example shows how to directly fill 3-cubes in an h-proposition. + -- It can help when one wants to pattern match certain HITs towards some n-types. isProp→Cube : {X : Type ℓ} (h : isProp X) (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 = + isProp→Cube h x i j = extend₁ (λ _ → h) {∂ i ∨ ∂ j} (x i j) From 6653bc3c744daadf12121674dc013c5545388e40 Mon Sep 17 00:00:00 2001 From: kangrongji Date: Sat, 16 Sep 2023 01:37:03 +0800 Subject: [PATCH 6/7] typos --- Cubical/Foundations/HLevels/Extend.agda | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda index 3ec2d69ef4..43a24f9b83 100644 --- a/Cubical/Foundations/HLevels/Extend.agda +++ b/Cubical/Foundations/HLevels/Extend.agda @@ -2,7 +2,7 @@ Kan Operations for n-Truncated Types -They provide an efficient way to construct cubes within truncated types. +It provides an efficient way to construct cubes in truncated types. A draft note on this can be found online at https://kangrongji.github.io/files/extend-operations.pdf @@ -19,11 +19,12 @@ private ℓ : Level --- For easily representing boundary of cubes +-- For conveniently representing the boundary of cubes ∂ : I → I ∂ i = i ∨ ~ i --- TODO: Write a macro to generate these stuff + +-- TODO: Write a macro to generate these stuff. module _ {X : Type ℓ} @@ -107,7 +108,7 @@ module _ private - -- An example shows how to directly fill 3-cubes in an h-proposition. + -- An example showing how to directly fill 3-cubes in an h-proposition. -- It can help when one wants to pattern match certain HITs towards some n-types. isProp→Cube : From 11346d7dd3fe4095240125b7440bd93f0837ed0e Mon Sep 17 00:00:00 2001 From: kangrongji Date: Sat, 16 Sep 2023 02:10:25 +0800 Subject: [PATCH 7/7] alignment --- 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 43a24f9b83..ebdae59c6e 100644 --- a/Cubical/Foundations/HLevels/Extend.agda +++ b/Cubical/Foundations/HLevels/Extend.agda @@ -32,7 +32,7 @@ module _ {ϕ : I} where extend₀ : - (x : Partial ϕ X) + (x : Partial _ X) → X [ ϕ ↦ x ] extend₀ = extend h _ @@ -43,7 +43,7 @@ module _ {ϕ : I} where extend₁ : - (x : (i : I) → Partial (ϕ ∨ ∂ i) (X i)) + (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