Anders Mörtberg
Anders Mörtberg
Indeed, calling it `interp` or `interpolate` sounds good to me. Otherwise I think this could be merged? @ecavallo Any opinions?
> That's cool. What about using `intp`? not easy to pronounce though. This might be a reasonable compromise? What I don't like about `interp` is that my brain will complete...
Oops, CI unhappy... Please fix
> Attempted CI fix. > > I am praying that this PR can finally be over... > > I still haven't been able to run checks locally but I could...
The CI was finally happy so I merged. Thanks for the contribution!
Sounds like very good improvements to me. Let me know when it's ready for review and I'll take a closer look
@aljungstrom Can you please take a look and review this?
> If we do this, then wild categories should also share the same `CategoryStr` (since their only difference, hom-types being sets, is property), so we could reuse things, for example...
I misremembered how the algebra code is structured, but it's similar to what I described above: https://github.com/agda/cubical/blob/master/Cubical/Algebra/Group/Base.agda#L36 So for algebraic structures we first have the properties in a record parameterized...
FYI the bundling of algebraic structures in the library was inspired by agda-stdlib: https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Bundles.agda#L450 I had a look and the agda-categories library does not do something like this for their...