Dagur Asgeirsson
Dagur Asgeirsson
Actually, it seems you get everything you're proving in this PR from existing API in `Sites.Equivalence` together with the following: ```lean instance {X : C} (f : Over X) :...
Thanks! maintainer delegate
I just pushed a suggestion I had forgotten to comment. No need to do anything, this is ready to be merged IMO. The suggestion was to change `inv (e.unit.app _)`...
@FlAmmmmING I think you accidentally resolved two comments about the docstring that you hadn't addressed. I've unresolved them, please address them
To make this easier to review, could you please open a separate PR with all the changes in all the files except the transvection file? The changes there are already...
I don't know of any tool... A hack you could use in this case is to branch of this PR's branch and remove the transvection file, and open a new...