Alex Rice

Your suggestion certainly seems to fit more with the standard definition. Perhaps the best way to implement it would be defining a predicate on the already existing type? My only...

That is understandable, would the content still be wanted if it were moved to the correct place (note this was far less work than it looks as I mainly copied...

There are two differences with the strict version. Firstly the definition of `f LeftInverseOf g` is changed from ``` \forall x -> f (g x) = x ``` to ```...

The issue with having this change the main definitions is that I expect other parts of the library use this a lot. It would probably be worth making helpers that...

I worked out everything that would need to be changed and it is virtually nothing as nothing seems to rely on the new function infrastructure yet. The downside is that...

> > > Two sets of definitions seems like a good idea to me as well. The simplifications in the proofs are impressive. I would slightly prefer having these defined...

> The problem is that `Strict` is overloaded. For example, in category theory, it seems that "having equality on objects" and "natural isos are actually equalities" are both described as...

I might have been confused but I thought the idea was to make a `Function.Definition.Strict` that mirrors `Function.Definition` but with the strict versions (and similar for structures and bundles)

I have tried this and get ``` Cannot open load file: No such file or directory, nix-company ``` I currently have the configuration ``` (use-package nix-company :commands (company-nix) ) (use-package...

Would it be easier if `company-nix` was provided as a separate melpa package or would this cause problems with it relying on nix repl