The Internal n-Cubes

[kangrongji]

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.