search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

WIP: right adjoint to Functor.Slice.Free #370

Closed Taneb closed 7 months ago

Taneb commented 1 year ago

I've been trying to get my head around this for a while now. It's getting painfully slow to compile so I'm pausing here hoping someone might suggest ways to speed it up (or tidy the code a bit)

Taneb commented 1 year ago

Had another look at this, and the load speeds make this so frustrating to work with. I'd really like some help speeding it up, the slowdown seems to be in unit/commute

JacquesCarette commented 1 year ago

I will try. First, I have to catch up on the backlog generated from me being away from home for essentially a month.

Taneb commented 9 months ago

I've tried this again from scratch on top of the changes in #347. Putting what this PR calls F₁-lemma in an abstract block significantly speeds up compilation of the functor, I think because Agda expands it out everywhere in F₁ and thence homomorphism-lemma. I haven't yet finished the proof of adjunction in that version.

JacquesCarette commented 9 months ago

Thanks @Taneb . Careful use of abstract (or even opaque? ) could indeed help. It is annoying how eager Agda seems to be to delta-expand.