This work presents the formal core of a typed-predication framework for geometric objects, formalised within dependent type theory. Geometric objects are defined as dependent pairs of carrier and metric structure; shape predicates are typed on these pairs rather than on bare carriers. The central results are: (1) metric variation yields distinct geometric objects sharing one carrier, not one contradictory object; (2) any inference from carrier identity to identity in the dependent sum commits an illicit projection; (3) shape predicates are fibre-sensitive, meaning that their truth-value may vary across the fibre even when the carrier is held fixed; and (4) the round square is not a genuine contradiction but a grammatical illusion produced by suppression of metric structure. The apparatus is domain-general and admits transport into other fields where predicates are typed on structured objects.
Dmytro Sukhov (Mon,) studied this question.