Benedikt Ahrens

On 20/12/2018 17:27, Daniel R. Grayson wrote: > I think they should all go into |Algebra|. Ok!

That would also be my preferred solution. Would you be willing to change the CI settings (in subdir `.github/workflows`)? I will then copy these changes to the satellite repositories and...

There is a spectrum of solutions to this issue, and I am trying to identify the most convenient one. For instance, the following could be made part of the definition...

On 07/05/18 18:14, Marco Maggesi wrote: > As you say, I think that the most obvious stack of structures is > functor > pointed functor > monad. I assume that...

Also, `grs` is not a good name for the category of groups - the identifier and the file need to be renamed.

On 08/02/18 14:41, Daniel R. Grayson wrote: > Good ideas. > > To be explicit - "grs" is not a good name because it's not a word or > concatenation...

On 29/10/2018 06:58, Daniel R. Grayson wrote: > I don't know a definition of "automation" in proof scripts, Benedikt. Surely, using a tactic called `auto` or `eauto` or `autorewrite` counts...

It seems particularly worrying that the automation is being used to define a structure (`Defined.`), not to do a proof (`Qed.`).

Oh, I am seeing that you would need a more complicated proof with opaque proofs of `is_precategory`. I don't think that this is related to 8.8.2. This is related to...

On 29/04/2019 18:50, Daniel R. Grayson wrote: > *@DanGrayson* commented on this pull request. > > ------------------------------------------------------------------------ > > In UniMath/CategoryTheory/DisplayedCats/Adjunctions.v > : > >> unfold homset_conj' in equiv1, equiv2....