1234567891011121314{-# OPTIONS --without-K #-}module Class.Show.Core where open import Class.Preludeopen import Class.Core record Show (A : Type ℓ) : Type ℓ where constructor mkShow field show : A → Stringopen Show ⦃...⦄ public Show¹ = Show ¹Show² = Show ²Show³ = Show ³