Lift types by instance resolution in Agda

lift.agda

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data ℤ : Set where
  nonneg : ℕ → ℤ
  negsuc : ℕ → ℤ

data ℚ : Set where
  frac_/suc_ : ℤ → ℕ → ℚ

record Embedding (A B : Set) : Set where
  field
    map : A → B
open Embedding renaming (map to _$_)

instance trivial↪ : {A : Set} → Embedding A A
trivial↪ $ x = x

-- Types can be lifted by finding their embedding via instance resolution
lift : {B : Set} {A : Set} ⦃ A↦B : Embedding A B ⦄ → A → B
lift ⦃ A↦B ⦄ x = A↦B $ x

instance
  ℕ↪ℤ : Embedding ℕ ℤ
  ℕ↪ℤ $ n = nonneg n

  ℕ↪ℚ : Embedding ℕ ℚ
  ℕ↪ℚ $ n = frac lift n /suc zero

  ℤ↪ℚ : Embedding ℤ ℚ
  ℤ↪ℚ $ a = frac a /suc zero