intro b
case h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝¹ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a : α
⊢ ∀ (x : α), F_map = G_map
case h.h
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F_obj : α → List β
F_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := F_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := F_map } X)
map_comp✝¹ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := F_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := F_map } f ≫ Prefunctor.map { obj := F_obj, map := F_map } g
G_map : {X Y : α} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ :
  ∀ (X : α), Prefunctor.map { obj := F_obj, map := G_map } (𝟙 X) = 𝟙 (Prefunctor.obj { obj := F_obj, map := G_map } X)
map_comp✝ :
  ∀ {X Y Z : α} (f : X ⟶ Y) (g : Y ⟶ Z),
    Prefunctor.map { obj := F_obj, map := G_map } (f ≫ g) =
      Prefunctor.map { obj := F_obj, map := G_map } f ≫ Prefunctor.map { obj := F_obj, map := G_map } g
hobj :
  ∀ (a : α),
    Prefunctor.obj (Functor.mk { obj := F_obj, map := F_map }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := F_obj, map := G_map }).toPrefunctor a
hmap : ∀ (a₁ a₂ : α) (f : a₁ ⟶ a₂), DVect2.Eq (F_map f) (G_map f)
a b : α
⊢ F_map = G_map