Reed Mullanix

Looks like I missed some renames during the merge: mind giving this a final ✅ @ncfavier?

Ok, there is one catch. We do have an instance that uses `Total-hom` in a non-trivial way in [Cat.Displayed.Univalence.Thin](https://github.com/the1lab/1lab/blob/main/src/Cat/Displayed/Univalence/Thin.lagda.md#L131): ```agda instance Extensional-Hom : ∀ {a b ℓr} ⦃ sa :...

There are also some places where inference gets much worse. Consider the following code from [Algebra.Group.Cat.FinitelyComplete](https://github.com/the1lab/1lab/blob/main/src/Algebra/Group/Cat/FinitelyComplete.lagda.md) ```agda Direct-product : Group ℓ → Group ℓ → Group ℓ Direct-product (G ,...

After sleeping on this, I think we can solve the problem by introducing a wrapper record around morphisms in Sets so we can retain the telescope. Definitely makes the experience...

If all else fails then yeah, that works. I do want to try and see if there's some reasonably generic way to do this though: we are going to have...

There are also a couple of other places where inference absolutely dies when working over Sets, so I'm not 100% convinced that wrapping is a bad idea. As a concrete...

Yeah, I was somewhat worried about this. In the 1Lab we define (pre)categories to have an hSet of morphisms, which means that we can ignore any sort of coherence issues...

Another perspective on this is that E-categories are sort of like half of a bicategory: we've got the 2-dimensional data of a bicategory, yet none of the equations or coherences....

I'm very interested in this as well; even in settings where you do have transport, it tends to be pretty miserable in practice. (This is especially true in cubical, where...

As another addendum: there is a second perspective on E-categories, which is that they are [wild categories](https://ncatlab.org/nlab/show/wild%20category). FWIW, this makes `agda-categories` even more miraculous; it's really surprising that you can...