-
Notifications
You must be signed in to change notification settings - Fork 134
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #902 from kangrongji/cubes
The Internal n-Cubes
- Loading branch information
Showing
3 changed files
with
347 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters