Tested install:

$ rpm -q idris2
idris2-0.7.0-4.fc42.x86_64
$ rpm -q idris2 chez-scheme
idris2-0.7.0-4.fc42.x86_64
chez-scheme-10.1.0-4.fc42.x86_64
$ idris2 --version
Idris 2, version 0.7.0

Simple typechecking appears to work:

$ cat semigroup.idr
record SemigroupOf A where
  constructor MkSemigroupOf
  op : A -> A -> A
  associativity : (a : A) -> (b : A) -> (c : A) -> (op (op a b) c) = (op a (op b c))

-- Borrowed from anotherArka/Idris-Number-Theory
associativePlus : (a : Nat) -> (b : Nat) -> (c : Nat) -> ((a + b) + c = a + (b + c))
associativePlus Z b c = Refl
associativePlus (S k) b c = rewrite (associativePlus k b c) in Refl

natPlus : SemigroupOf Nat
natPlus = MkSemigroupOf (+) associativePlus
$ idris2 --check semigroup.idr 
1/1: Building semigroup (semigroup.idr)

as well as building an executable:

$ cat hello.idr
main : IO Unit
main = putStrLn "Hello from Fedora!"
$ idris2 hello.idr -o hello
$ build/exec/hello
Hello from Fedora!