Andre Knispel

Oh, `Singleton` is a leftover from a previous try. Good to know that `Proposition` is a thing!

I'm not sure what you mean by 'the commuting triangle in `exists` would commute pointwise'. As for the dependent pair, do you mean that it would be nicer if we...

It might be better to have cartesian monoidal categories instead. That way, we get a general machinery and just have to show the existence of finite products or binary products...

I think it looks good, but I'm thinking that it might be a good idea to export `PreFreeMorphism` together with its constructors. There might be things that don't require quotienting,...

Ok, I've realized that the functions provided already enable writing morphisms in the FSSMC. It might still be a good idea to expose the `PreFreeMorphism` type, for convenience. Right now,...

This is problematic though if one is using `IntSet/IntMap` in Haskell code. I have some Haskell code using these and I have to add conversions in these places. One can...

Luckily, my numbers are never negative. In the paper it is mentioned that eventually you intend to use a 64-bit integer type. Is that anywhere on the horizon? (just out...

The minimal example that generates the `Deriving` imports is: ``` module TestModule where data Test = A | B | C deriving (Eq, Ord) ``` It is crucial that the...

The same file also generates an `Import GHC.Prim.Notations.`, which also does not exist, and the type class implementations don't work.

In the code of the generated instances, there are several lines like ```let 'lop_azh__ := (_Deriving.$con2tag_6RQENwcLfx1EMY3OJHNIZn_ a) in``` Do you see these lines too? These cause an issue for me,...