I my experience, strict to loose is easier. You can always make types that encode something without the benefits of type safety. For instance, you can encode stuff in Strings without type safety.
Loose to strict, however, requires you to write a type checker. Not a gargantuan task, but not trivial either.
I think that’s what they try to do in the best cases. They’re building abstractions on top of abstractions, usually for stuff that are discovered in mathematics. That would be where category theory enters the conversation.
They will acknowledge that static types have a cost. But they perceive the benefit to be much greater. They’re willing to appease the pedantic type checking for the benefits of reasoning at a higher level of abstraction.
Eric