Non-transparently-reducible Hom types

Stream: lean4

[Robert Maxton]

I seem to have used a rather badly behaved type for the hom-types of a quiver I'm working with:

def Vertex (F : Quiv₀ ⥤ Type max u v) := F.obj 0
def Edge (F : Quiv₀ ⥤ Type max u v) (s t : Vertex F) := {e : F.obj 1 // F.map .source e = x ∧ F.map .target e = y}

@[simps (config := .lemmasOnly)]
def ofFunctor (F : Quiv₀ ⥤ Type max u v)  [Small.{u] (F.obj 0)] [∀ x y, Small.{v} (Edge F X Y)]  : Quiv.{v, u} where
  α := Shrink.{u} (Vertex F)
  str := {Hom x y := Shrink.{v} (Edge F (equivShrink _ |>.symm x) (equivShrink _ |>.symm y))}

--Obviously doesn't work, since `(equivShrink _).symm (equivShrink _ X) = X` only holds propositionally`
unif_hint ofFunctor_hom_eq (X Y : Vertex F) where
  ⊢ (@Quiver.Hom (ofFunctor F) _ (equivShrink _ X) (equivShrink _ Y)) ≟ Shrink (Edge F X Y)

[Robert Maxton]

It's badly behaved for a whole bunch of reasons -- anywhere that unif_hint would be useful, for starters; anywhere Lean manages to 'half-forget' the definition, so that a proof term composes two functions (g : _ → Shrink (Edge F X Y)) (f : (equivShrink _ X) ⟶ (equivShrink _Y)) → _ but I get a type error when I write f (g x); and in general, the fact that Equivs only cancel with themselves propositionally mean that I end up with ever-increasingly-long terms of the form (eqv1.symm (eqv1 (eqv2.symm (eqv2 (... in places that are hard to reach.

Clearly, my definition needs a rework, but I'm not at all sure what specifically to change. My constraints are primarily that the functor I'm operating on needs to stay Quiv₀ ⥤ Type max u v, but the resulting quiver needs to be a Quiv.{v, u}. So far, this is the only way I've found to achieve this goal; categories have EssentiallySmall but a) SmallModel only creates homogenous categories where the level of the objects and arrows match, and b) I'm not really working with categories to begin with.

[Robert Maxton]

Here's a #mwe; I'll try and add some concrete examples of issues as I rediscover them:

import Mathlib.CategoryTheory.Category.Quiv
import Mathlib.CategoryTheory.Types
import Mathlib.Logic.Small.Defs

def Quiv₀ := Fin 2

instance {n} : OfNat (Quiv₀) n := inferInstanceAs (OfNat (Fin 2) n)

inductive Quiv₀.Hom : Quiv₀ → Quiv₀ → Type
| id X : Quiv₀.Hom X X
| source : Quiv₀.Hom 1 0
| target: Quiv₀.Hom 1 0

instance : Category Quiv₀ where
  Hom := Quiv₀.Hom
  id := Quiv₀.Hom.id
  comp  | Quiv₀.Hom.id _, g => g  | f, Quiv₀.Hom.id _ => f
  id_comp f := by cases f <;> rfl
  comp_id f := by cases f <;> rfl
  assoc {W X Y Z} f g h := by sorry

abbrev Vertex (F : Quiv₀ ⥤ Type w) := F.obj 0
abbrev Edge (F : Quiv₀ ⥤ Type w) (s t : Vertex F) := {e : F.obj 1 // F.map .source e = s ∧ F.map .target e = t}

@[simps (config := .lemmasOnly)]
def ofFunctor (F : Quiv₀ ⥤ Type max u v)  [Small.{u] (Vertex F)] [∀ X Y, Small.{v} (Edge F X Y)]  : Quiv.{v, u} where
  α := Shrink.{u} (Vertex F)
  str := {Hom x y := Shrink.{v} (Edge F (equivShrink _ |>.symm x) (equivShrink _ |>.symm y))}