Multiple CoeFun instances

Stream: general

[David Holmqvist]

Is it possible to have multiple CoeFun instances? One concrete motivation would be functors that can be applied to both objects and morphisms:

structure Functor (C₁ : Category obj₁) (C₂ : Category obj₂) where
  Fₒ : C₁ → C₂
  Fₕ : Hom c₁ c₂ → Hom (Fₒ c₁) (Fₒ c₂)

  id   : ∀ {c₁ : C₁}, Fₕ (id c₁) = C₂.id (Fₒ c₁)
  comp : Fₕ (g ∘ f) = Fₕ g ∘ Fₕ f

infixr:60 " ⇒ " => Functor

instance [C₁ : Category obj₁] [C₂ : Category obj₂] : CoeFun (C₁ ⇒ C₂) (fun F ↦ ∀ {c₁ c₂ : C₁}, Hom c₁ c₂ → Hom (F.Fₒ c₁) (F.Fₒ c₂)) where
  coe F := F.Fₕ

instance [C₁ : Category obj₁] [C₂ : Category obj₂] : CoeFun (C₁ ⇒ C₂) (fun _ ↦ C₁ → C₂) where
  coe F := F.Fₒ

[Kim Morrison]

Why don't you try it out? (In your example you don't seem to be using the same Category definition as Mathlib -- I'd recommend using it!)

[Edward van de Meent]

it is possible, it just means that you're going against the assumption of autoParamoutParam that only one such instance will exist.

[Kim Morrison]

I'm not sure what you mean here, @Edward van de Meent, how does autoParam assume uniqueness of coercions?

[Edward van de Meent]

in my understanding/interpretation, using autoParamoutParam for a class definition is basically promising that all other parameters completely determine this one?

[Edward van de Meent]

and since CoeFun uses autoParamoutParam for the resulting (function)type, a (non-binding) promise is made that coercions are unique.

[Kim Morrison]

Are you thinking about outParam?

[Kim Morrison]

autoParam is for defaults provided by tactics

[Edward van de Meent]

ah right (oops) :clown:

[Edward van de Meent]

in all cases i meant outParam

[David Holmqvist]

I did try, but it seemed to choose the most recently defined instance unfortunately… but yes, I’m using my own definition of category, I’ll take a look at the Mathlib one.

But it sounds like in general this should be possible? As in, it won’t always choose the most recently defined instance?