search

agda / agda-categories

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

`!-unique₂` takes implicit args in `Terminal`, whereas it takes explicit ones in `Initial` #366

Open cxandru opened 1 year ago

cxandru commented 1 year ago

In Terminal, !-unique₂ : ∀ {A} {f g : A ⇒ ⊤} → f ≈ g takes f, g as implicit arguments, whereas in Initial, the arguments to the same function (!-unique₂ : ∀ {A} → (f g : ⊥ ⇒ A) → f ≈ g) are explicit.

This is probably an mistake and should be unified. I'm willing to fix this after I finish #362 .

JacquesCarette commented 1 year ago

Yes, it is most likely a mistake. It would be worth looking through use sites of both to see if they end up being specified (in the implicit case) anyways. It could be that 'in context' they can usually be inferred.

On the flip side, it would be fascinating if there were somehow a difference, in practice, between Terminal and Initial situations that justified this choice!!