Next Types Are Theorems; Programs Are Proofs 11

Propositions vs. types

      inhabited                   a → a               TRUE    
                       
      uninhabited                 a → b               FALSE   
                       
      inhabited                   a → (b → b)         TRUE    
                       
      inhabited                   a → (b → a)         TRUE    
                       
      uninhabited                 a → (a → b)         FALSE   

Huh, that's funny.
Next Next