Termination checking failed for the following functions:
  ℕ, ℕ, ℕ′
Problematic calls:
  .TypeConstructorsWhichPreserveGuardedness1.ℕ₁.♯-0
    (at TypeConstructorsWhichPreserveGuardedness1.agda:26,16-17)
  ℕ (at TypeConstructorsWhichPreserveGuardedness1.agda:26,18-19)
  ℕ′
    (at TypeConstructorsWhichPreserveGuardedness1.agda:50,24-26)
  .TypeConstructorsWhichPreserveGuardedness1.ℕ₂.♯-1
    (at TypeConstructorsWhichPreserveGuardedness1.agda:54,21-22)
  ℕ (at TypeConstructorsWhichPreserveGuardedness1.agda:54,23-24)