open import agda20200123

data ℕ : Type where
  zero : ℕ
  suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

id : ∀ {A : Type} → A → A
id x = x

id' : ∀ (A : Type) → A → A
id' A x = x

square-of-one : ℕ
square-of-one = id 1

square-of-one' : ℕ
square-of-one' = id' ℕ 1