My first thought: “okay this looks like haskell.”. Ctrl+f haskell: one result, not about the language. Ctrl+f monad: none. So for everone else that had the same train of thought, I found this link explaining the differences between Haskell and Agda: http://learnyouanagda.liamoc.net/pages/introduction.html
I just bought the HoTT book! I’m very excited to read it. There is a HoTT library for Coq and the Arend Theorem Prover by JetBrains which has HoTT built in for those that want something other than Agda.