-
Notifications
You must be signed in to change notification settings - Fork 134
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The Internal n-Cubes #902
Merged
Merged
The Internal n-Cubes #902
Changes from 3 commits
Commits
Show all changes
8 commits
Select commit
Hold shift + click to select a range
cbe547e
done
kangrongji 6d03ce1
done
kangrongji 6a2b711
add import to Everything
kangrongji 1412d0d
better ident
kangrongji e257335
Merge branch 'master' of https://github.com/kangrongji/cubical
kangrongji ba7e0a2
Merge branch 'master' into cubes
kangrongji 1eab83b
comment
kangrongji 5b372f0
off-by-three
ecavallo File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
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,155 @@ | ||
{- | ||
|
||
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. | ||
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) | ||
Comment on lines
+122
to
+124
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes |
||
|
||
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Let's add a reminder here that we can fix this in 2.6.3 when I -> A becomes fibrant.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
done