agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard

Rename slice functors

Open Taneb opened this issue 1 year ago • 1 comments

Extracted from https://github.com/agda/agda-categories/pull/408

Taneb avatar Oct 24 '24 14:10 Taneb

FYI, swamped until Nov. 1. Will look after that.

JacquesCarette avatar Oct 26 '24 13:10 JacquesCarette

@JacquesCarette are you able to give this a review now?

Taneb avatar Nov 04 '24 15:11 Taneb

Very soon. Catching up on all the things I didn't do last week. This is explicitly on that list.

JacquesCarette avatar Nov 04 '24 18:11 JacquesCarette