-
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
The Internal n-Cubes #902
Conversation
Cubical/Foundations/Cubes/Base.agda
Outdated
-- 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 |
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
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) |
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.
Is set
short for section?
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.
Yes
Looks good to me! |
Ehhh.... How could I write 2.9.3? |
This PR contains a mutual recursive definition of n-cubes, their boundaries and n-cubes with fixed boundary, as family of types parametrized over
ℕ
. They're strictly isomorphic to external ones as, for example,(i j : I) → A
,(i j : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A
and(i j : I) → A [ (i ∨ ~ i ∨ j ∨ ~ j) ↦ u i j ]
. Unless one fixes a canonical natural numbern
as dimension, these isomorphisms cannot be described internally, so for more general results one must resort to macros or 2LTT.My aim is to prove that a type has h-level
n
if and only if n-boundaries can always be filled into n-cubes, generalizing the special cases aboutisSet'
andisGroupoid'
already existing in library.