Iowa Type Theory Commute artwork

Deriving disjointness of constructor ranges in RelTT

Iowa Type Theory Commute

English - February 02, 2021 06:00 - 11 minutes - 8.1 MB - ★★★★★ - 13 ratings
Technology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed


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.