search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
454 stars 139 forks source link

The Internal n-Cubes #902

Closed kangrongji closed 2 years ago

kangrongji commented 2 years ago

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 number n 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 about isSet' and isGroupoid' already existing in library.

ecavallo commented 2 years ago

Looks good to me!

kangrongji commented 2 years ago

Ehhh.... How could I write 2.9.3?