Jordan Barrett

I disagree, since I think `makeX` gives much more readable definitions. E.g. looking at the current definition of the group ℤ in `Cubical.Algebra.Group.Instances.Int`: ```agda ℤ : Group₀ fst ℤ =...

On the other hand, I just tried doing this with the `GroupStr` constructor `groupstr`: ```agda ℤ : Group₀ ℤ = ℤType , groupstr 0 _+ℤ_ (_-ℤ_ 0) (makeIsGroup isSetℤ +Assoc...

If `X` / `isX` is a record type, then can't we just use a constructor instead of `makeX` / `makeIsX`?

Sure. I'm more talking about stuff like taking the quotient of an abelian group by a subgroup, or using e.g. `Subgroup→Group` to turn a `Subgroup (AbGroup→Group A)` into an `AbGroup...

I think there's inevitably gonna be boilerplate somewhere, so better to have it written once and for all in the library.

Kubernetes handles the log rotation, so if there are a lot of logs, sure we're gonna lose the old logs. This is not really any different to the file case...

Hi @Juneezee, thanks a lot for this. Can you please sign [Canonical's contributor agreement](https://ubuntu.com/legal/contributors)? It just gives us permission to use your contributions in our code.

> @barrettj12 Signed smiley Hmm, the CLA check is still not passing. Did you provide your GitHub username + the email your commits are signed with? ([email protected])

> @barrettj12 Yes I did. I just submitted the CLA again. Could this be because my Ubuntu account is newly created and it takes a while for the system to...

Okay, thanks, that should do it. We just have to wait for your Launchpad account to be added to the [“Canonical Contributor Agreement” team](https://launchpad.net/~contributor-agreement-canonical). It will appear on your Launchpad...