Guilherme Silva

I defined my ≤-Induction without needing to create a new inequality for that.

Added Unordered Pair

11

I created Unordered Pair, which means that `a , b = b , a`.

I created a new data structure `FinWeak` and I proved that it is isomorphic to Fin. ```agda data FinPure : ℕ → Type where zero : FinPure 1 suc :...

Add Nix flakes

20

With this flake file, it becomes easier to import this library into other projects. This is based on: https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/agda/default.nix https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/libraries/agda/cubical/default.nix

It is a dependent version of N-Ary Vector.

Added Z mod n as Fin

10

In `Data.Integer.DivMod`, there are already some properties of Z mod n, but in this pull request, it is represented as Fin n.