I am new to type theory and may have misstated my understanding when stating it in formal language.
Anyways, we dont need any type theory to understand the Pali canon. I’ll explain in plain English how the concept of anātman is employed in the pāli canon and show why the pali canon is not denying ātman thereby - in a new thread. Someone asked me that very question in a private message and I’ve explained the concept to them so I’ll post it in a new thread and people can evaluate it there.
Update: see The meaning of anattā in "rūpaṃ bhikkhave anattā" - a review