WIP: right adjoint to Functor.Slice.Free

[Taneb]

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]

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]

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

[Taneb]

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]

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