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