search

agda / cubical

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

Dependent Cube Filling #909

Closed kangrongji closed 2 years ago

kangrongji commented 2 years ago

Dependent version of the previous PR. Characterize of isOfHLevelDep by lifting with specified boundary the cubes in the base to the cubes in the family. See Cubical.Foundations.Cubes.HLevels.