{-# OPTIONS --safe #-}

module Interface.TypeClasses.HasSubset where

open import Level using (Level; suc)


record HasSubset {a} (A : Set a) : Set (suc a) where
  field _⊆_ : A → A → Set a
  infix  _⊆_


open HasSubset ⦃...⦄ public