diff --git a/src/logic/equiv/basic.lean b/src/logic/equiv/basic.lean index 25b4b421b8435..d4d647a945220 100644 --- a/src/logic/equiv/basic.lean +++ b/src/logic/equiv/basic.lean @@ -69,7 +69,6 @@ universes u v w z variables {α : Sort u} {β : Sort v} {γ : Sort w} /-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/ -@[nolint has_inhabited_instance] structure equiv (α : Sort*) (β : Sort*) := (to_fun : α → β) (inv_fun : β → α)