Much easier compared to what though? Agda is made in Haskell which recently got linear types. If you mean much easier than mainstream languages like JS, Python

Much easier compared to what though? Agda is made in Haskell which recently got linear types. If you mean much easier than mainstream languages like JS, Python or Java you're right. If you mean much easier than everything, I think you're wrong.