Remove duplicated factorial function

[anshwad10]

_! is defined in Cubical.Data.Nat.Properties, factorial is defined in Cubical.Data.Fin.LehmerCode, and they both have identical definitions.

[felixwellen]

Good catch! A further improvement should be to move factorial to the definition of _!, so it can be used as an alternative and the definition is easier to find.

[anshwad10]

Wouldn't that break code that import Cubical.Data.Fin.LehmerCode but not Data.Nat.Properties and uses factorial? or is the change minor enough that backwards compatibility doesnt matter as much?

[felixwellen]

As long as the library still checks, it is okay. (Haven't looked if anything in the library imports lehmercode)

[anshwad10]

Good catch! A further improvement should be to move factorial to the definition of _!, so it can be used as an alternative and the definition is easier to find.

Do I do this in another PR or add a commit to this one?

[felixwellen]

Do it in a new PR