saizan / cubical-demo Goto Github PK

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 in PathPrelude?

@Saizan, can you give me the version of agda-stdlib and agda that you've successfully managed to build this project with?

On my system:

§ agda --version
Agda version 2.6.0-47bba7d
§ cd ~/.agda/libs/agda-stdlib && git show
commit d3df3e41156ba4981dd1e08784cc5bfd94999184
...
§ cd ~/workspace/cubical-demo && agda --cubical Everything.agda
...
~/workspace/cubical-demo/Id.agda:12,27-32
PathP (λ _ → .A) .x (ouc y) !=< Path' (_x_24 φ w) (_y_25 φ w) of
type Set .a
when checking that the expression ouc w has type
Path' (_x_24 φ w) (_y_25 φ w)

As the title says.

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.

Another task would be to find correct names for the proofs.

I could do the first as good as I can.

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

Using the latest (or nearly-so) master versions of agda and the standard library, I get an error when trying to load Sigma.agda. The error is:

...cubical-demo/Sigma.agda:103,61-63
(Set ℓ') !=< (PathP (λ _ → Set ℓ') (_a_440 t u p) (_x_441 t u p))
of type (Set (ℓ-suc ℓ'))
when checking that the expression T0 has type
Path (_a_440 t u p) (_x_441 t u p)

I believe you can use set -e rather rather than || exit 1

I propose the repo should be named cubical rather than cubical-demo.

See e.g.: https://help.github.com/articles/renaming-a-repository/

Did you forget to commit notIsEquiv?