How to properly define a record with parameters in Agda?

Question

I'm using Agda 2.5.3 and the HoTT Agda library to learn some homotopy type theory. I've defined a simple S¹:

data S¹ : Type₀ where
  base : S¹

postulate
  loop : base == base

and now I'm trying to define a record type for a function that acts as the circle recursion principle for a type A:

record is-S¹-rec {i} {A : Set i} (base* : A) (loop* : base* == base*) : Set i where
  field
    f : S¹ → A
    f-base : f base == base*
    f-loop : apd f loop == loop* [ Path ↓ f-base ]

But I get this error:

(_A_22 base* loop* f f-base → Set (_i_20 base* loop* f f-base)) !=<
Set (_i_20 base* loop* f f-base) of type
Set (lsucc (_i_20 base* loop* f f-base))
when checking that the expression Path has type
_A_22 base* loop* f f-base → Type (_i_20 base* loop* f f-base)

I've tried increasing the universe level of the record with no luck. Any tips on what this message means would be greatly appreciated.