Guilherme Silva

From Wikipedia (https://en.wikipedia.org/wiki/Vector_space), I think that Vector Space is defined over a Field and not from a Commutative Ring.

```sh cat test.agda {-# OPTIONS --cubical #-} open import Cubical.Foundations.Prelude EOF nix --extra-experimental-features "nix-command flakes" shell github:guilhermehas/cubical/52dfed7b703e6294b7acd11244cd838480839367#agdaWithCubical agda -l cubical -i . test.agda ``` With these commands, I can use...

I have put the instructions in `INSTALL.md` and also changed the CI to just work when deploying on the master branch.

> after some changes to the library. If I understand you right, @guilhermehas, you would like this job to run (at least) whenever a PR is merged into master. I...

I tried to use this Agda flake, but it didn't work here. It looks like it is broken. I put `inputs.nixpkgs.url = "nixpkgs/nixos-22.05"` , so now nixpkgs is pinned in...

@ncfavier I created an overlay. Look if it is good. I don't know if it is possible to change the Agda compiler using my overlay.

> Also, whatever steps need to be taken could just be documented in [RELEASE.md](https://github.com/agda/cubical/blob/master/RELEASE.md) :) I put the instructions in `RELEASE.md`.

Yes, I know the relation. I will try to put in the properties. For example, in Agda Stdlib (https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Recursive.agda), they defined Vec using Product. So maybe it is possible to...

I was trying to define the recursive definition: ```agda FMSet : (A : Type ℓ) (n : ℕ) → Type ℓ FMSet A 0 = Unit* FMSet A 1 =...

I figured out how to do: ```agda addN : UnorderedPair (A × ℕ) → ℕ addN = rec isSetℕ (λ x y → proj₂ x + proj₂ y) λ x...