Deriving disjointness of constructor ranges in RelTT
Iowa Type Theory Commute
English - February 02, 2021 06:00 - 11 minutes - 8.1 MB - ★★★★★ - 13 ratingsTechnology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: Software Design and Intrinsic Identity
Next Episode: Introduction to Intersection Types
Responding to an email question from a listener, I explain how to derive a form of inconsistency from the assumption that True is related to False at type Bool.