Laine Taffin Altman

Any progress on this?

I think we can actually do something much simpler, exploiting `Borrow` and `ToOwned`; I'll put something together demonstrating it today.

In the meantime, you can use the following instead of `open import HoTT` to help fix it: ``` agda open import HoTT hiding (module TLevel) open TLevel renaming (S to...

@bluss This is ready for review, whenever you have time.

I suppose. I was assuming they wouldn't, since the `map_results` method this ”extends” is in `itertools` rather than `std`. Is there a particular procedure for checking?

@jswrenn Maybe `map_and_then`?

@jswrenn How's it look now?

@philmuemue I’d be more than happy to!

Understood! I basically made this as a drive-by contribution and don't mind if it's not acceptable. As for the how: https://imageoptim.com/ (I used the app version).

I'd also be very interested in this functionality, although I think it could be stop-gapped by providing some minimal sugar over the “hack” to make it not look quite as...