Alex Rice

Strict inverses

16

Adds versions of various inverses that compose in a strictly unital and associative way. i.e. Given `{A : Setoid} (f g h : Inverse A A)` we have ```agda2 (f...

nixpkgs-fmt as nix-indent-function

2

Are there any plans to make an indent function based on nixpkgs-fmt or at least one that agrees with nixpkgs-fmt?

How to use nix-company.el

5

I cannot work out how to use the `nix-company.el` file. It does not seem to make it into my installation. ``` . ├── nix-support │   └── setup-hook └── share └──...

hackage2nix: Always print extraVersions

8

See discussion in https://github.com/NixOS/nixpkgs/pull/90143 In short, I would like to be able to pin nixpkgs's `agdaPackages` to version 2.6.1. I had hoped that adding `Agda == 2.6.1` to `extra-packages` in...

I tried to add a generator and it's inverse to the middle of a diagram, I don't know if this is allowed [homotopy_io_state.zip](https://github.com/homotopy-io/homotopy-rs/files/13795204/homotopy_io_state.zip)

"-W error" invalidates interface files

11

This may be intentional, but currently it seems that adding the "-W error" flag to agda causes interface files to need to be remade and in fact the generated interface...