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

[cxandru]

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]

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!!