3abc

Very bad performance when filling high dimensional cubes

9

In cubical mode I tried to use `hcomp` to fill a high dimensional cube. The performance is very bad. For the [6d-cube](https://gist.github.com/3abc/b8fa06a5b3fd14db8642fbd4ec8c9cc8) it takes about `100s` to type check. But...

Proving Eliminators without using J.

14

I used a lemma called `g2TruncFib` similar to `setTruncFib`. Just one remark, for `g2TruncFib` (and similarly `setTruncFib`) to work we don't need that `gP x` is a 2-groupoid for all...

Currying inside systems

1

For this definition ``` def comp3 (A : type) (b : (j0 j1: 𝕀) → A) (k0 : [j1 k] A [ k = 0 → b 0 j1]) (l0...