∀ {f : Type u → Type v} [inst : Functor f],
  (∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β) →
    (∀ {α : Type u} (x : f α), id <$> x = x) →
      (∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x) → LawfulFunctor f