{F : Type u → Type u} →
  [q : QPF F] →
    {G : Type u → Type u} →
      [inst : Functor G] →
        {FG_abs : {α : Type u} → F α → G α} →
          {FG_repr : {α : Type u} → G α → F α} →
            (∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x) →
              (∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x) → QPF G