{-# OPTIONS --safe #-}
module Prelude.Initial where
 
open import Prelude.Init
 
record HasInitial (A : Type ℓ) : Type (lsuc ℓ) where
  field Initial : A → Type
open HasInitial ⦃...⦄ public