Jacques Carette
Jacques Carette
Oh, you're asking for something much stronger than I expected. But it's still an interesting question. I'm investigating now.
Are you sure you're asking the right question? The objects aren't the same: ```agda module _ {C : Category o ℓ e} {o′ ℓ′ e′ : Level} where open Category...
There is `Functor.op`, which would line up better.
Thanks, that helps a lot. I'll fiddle some more.
Most definitely not! Things are staying as records in this library. The question is indeed, what makes some records different than others. There are definitely "options" that one can set...
I think we could create some "forget" functions that go from nominal to structural for when we want to explicitly do that. I think we generally want to keep things...
I think it is possible to add commits to this PR, at least for people who have push access to the repo (which I believe you do @sstucki ). Though...
Because of the stated reason, using the category tactic here seems reasonable.
Everything else in `Expr` represents an iso, so why not for ```agda [_↑] : X ⇒ Y → Expr (X ′) (Y ′) ``` as well? You should make the...
The `Expr` without `[_↑]` could only represent isos. That's why `invert` could exist.