No I meant intuitive like easy to understand for humans. (It is also intuitionistic but that's a technical fact shared by both Coq and Agda (though not HOL)). The reason I said that is because thinking in terms of types is very straightforward for people. "Give me a View and Serializer so I can give you JSON" "Why is my code not working? Oh because you can't always find the head of a list, I need to give you NonEmpty List T". Similarly, proving something is a group is like trying to go Group somehow from the objects around.
ah, my bad, i see how that makes more sense. FWIW i agree – often, mentally converting a theorem to a type and thinking about the problem in that framework makes things easier for me to grasp. (also explains why we "apply" theorems/lemmas :) )