Zhan Shi: Partial Gradual Dependent Type Theory. SPLASH Companion 2023: 22-24