Anders Mörtberg

I think it's inspired by the type categories of section 6.3 in: https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf I think whoever formalized that file was inspired by https://github.com/UniMath/TypeTheory/blob/master/TypeTheory/ALV1/TypeCat.v I did not look or think very...

For each algebraic structure `S` I would suggest the following organization: - `Base.agda` : definition and basic operation of `S` - `SIP.agda`: all the SIP stuff - `Properties.agda` : basic...

> @mortberg I would agree on the general organization you are offering. The question to me now is would be how much do you split foo I think it's impossible...

> > For each algebraic structure `S` I would suggest the following organization: > > ``` > > * `Base.agda` : definition and basic operation of `S`, maybe some basic...

> For each algebraic structure `S` I would suggest the following organization: > > * `Base.agda` : definition and basic operation of `S` > > * `SIP.agda`: all the SIP...

These issues are related: - https://github.com/agda/cubical/issues/116 - https://github.com/agda/cubical/issues/126 - https://github.com/agda/cubical/issues/150 It might be possible to close some of them.

@mchristianl I don't know why, but I can't assign you to this issue...

The question about boolean or non-boolean orders is orthogonal to this issue... But I personally like boolean tests that then get lifted to types using boolean reflection à la SSReflect....

Discussion to be continued :-)

Yes, we should have naming conventions for CategoryTheory similar to those we recently added for Algebra: https://github.com/agda/cubical/blob/master/Cubical/Algebra/NAMING.md