Is it possible to construct cyclic types in Agda?

cyclic.agda

data A : Set

data B : Set where
  b : A → B

data A where
  a : B → A
  

It seems as though this should be possible if you could somehow construct both A and B at the same time, and have them refer to one another, but I'm not sure if you can do this in Agda.

record A′ : Set
record B′ : Set

record A′ where
  coinductive
  constructor mka
  field geta : B′
open A′ public

record B′ where
  coinductive
  constructor mkb
  field getb : A′
open B′ public

a′ : A′
b′ : B′

a′ .geta = b′
b′ .getb = a′

and alternative property

data A : Set

data B : Set where
  b : A → B

data A where
  a : B → A

data ⊥ : Set where

¬a : A → ⊥
¬b : B → ⊥

¬a (a y) = ¬b y
¬b (b x) = ¬a x