cubical-demo

cubical-demo copied to clipboard

Multiple ≃'s

2

`Cubical._≃_` is defined via `Σ`. `Cubical.Univalence._≃_` is congruent but defined via a record. What's the motivation? Would you mind it if I let `Cubical.Univalence` import and use the one defined...

fredefox

I propose the repo should be named `cubical` rather than `cubical-demo`. See e.g.: https://help.github.com/articles/renaming-a-repository/

fredefox

Use `set -e`

3

I believe you can use `set -e` rather rather than `|| exit 1` https://github.com/Saizan/cubical-demo/blob/f9f793cc925dcde1c84788a68eef5c53384627b7/test.sh#L1

fredefox

For instance the GradLemma file contains propIsEquiv. I found the proof by chance. We need to put the proofs into files with correct names so we can easily find them....

xekoukou

Could help, for instance, I do not know `Partial`...

andreasabel