kang

Better Error Message?

2

I tried to define an indexed HIT as follows: ```agda module _ (X : Type ℓ)(x₀ : X) where data 𝕁Path (i : I) : Type ℓ where [] :...

This PR finishes the proof that a type is of h-level n if and only if any n-boundary can be extended to an n-cube. It is possible to make a...

This PR contains a few simple cases of cubical subtype, and shows: - Cubes with a pair of fixed constant opposite faces is equivalent to cubes in the path type;...

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,...

Dependent `ua` for dependent equivalences/isomorphisms.

Short Names or Long Names?

5

Recently I realized that there are many concepts in category theory that they have long names, and they become even longer if one combines them, such as `isUnivalentFullSubcategory` or `isFaithful+isFull→isFullyFaithful`....

2LTT, External Cubes and Cube Filling Macros

19

This PR contains macros that allow users to fill cubes, for both non-dependent and dependent, provided assumption of h-levels. To achieve this, I choose the approach that using 2LTT to...

I want to add some facts about 2LTT to the library but not sure the suitable place for them. See #910 .

This PR reorganizes the cube fillers in library. They've been renamed uniformly, deduced as corollaries of the `extend` operation and now collected in `Cubical.Foundations.HLevels.Fillers`. There are still some left in...

The General Extend Operation (a.k.a. The Cube-Filling Macro)

1

This PR implements the general version of `extendₙ` for all values of `n`. It's a fortunate development that this operation be done in the current version of Cubical Agda. Only...