Reed Mullanix

Agree with @JacquesCarette here; `WeaklyDecidable` isn't a great alias, and it just complicates the import graph. I would really caution against `SemiDecidable`; that name is already occupied by a much...

We actually don't have `SemiDecidable` yet! The reason why is exactly the one you stated; I haven't found a nice enough story for generalizing beyond Nat. I suspect that it...

Will take a look again at this: seems like a nice opportunity to clean up the mess that is Cat.Displayed.Reasoning.

Have some draft code up at https://github.com/the1lab/1lab/blob/displayed-reasoning/src/Cat/Displayed/Reasoning.lagda.md but I don't exactly _love_ the ergonomics. Being able to re-use the reasoning combinators is pretty sweet and it does feel _much_ snappier,...

IIRC the reason I went with a record in the first place was to use `no-eta-equality`, but this ended up causing quite a bit of trouble. I _think_ we could...

Completely agree that naming is hard! I am not aware of any area of computer science/mathematics where bottom and top elements are called minimum and maximum elements though. The terms...

For the "chosen join" vs. "is join" I completely agree that you want both. As for a less piecemeal discussion, where would be the best venue for that?

There are definitely some organizational reasons to prefer homomorphisms between raw structures, but this does not play out well in practice IME. The reasons for this are a bit subtle...

Sorry, should have been more clear! In general, one should aim to be able to infer bundles/structures from their morphisms. Deviating from this leads to yellow when you try to...

STRONG +1 on this: we've been using https://opam.ocaml.org/packages/bwd/ in RedPRL projects for years and it makes life so much easier.