{-# OPTIONS --safe --cubical-compatible #-}
module stdlib-classes.Class.HasCast.Base where

open import Level using (_⊔_)

record HasCast {a b} (A : Set a) (B : Set b) : Set (a  b) where
  field
    cast : A  B

open HasCast ⦃...⦄ public