Girard’s paradox demonstrates the inconsistency of dependent type theory when the type of Type is Type, adapting the Burali-Forti paradox of ordinals. In this performance, I live-code the paradox in a simplified type theory, using my system Soundproof to present the component proof terms as trees, both sonically and visually. The structure is synthesized across duration, pitch, rhythm, timbre, color, and motion, inspired by the music of Iannis Xenakis and Catherine C. Hennix.