module tutorial where
open import tutorial-generated

open import Data.Nat
open import Data.Bool
open import Data.List
open import Data.String using (String)
open import Relation.Binary.PropositionalEquality
  renaming (refl to by-definition-chasing)
  hiding ([_])

modus-ponens : {A B : Set}
             → (A → B)
             →  A
             → ----then----
                B
modus-ponens f x = f x -- function application lol


data False : Set where

data Empty : Set where

data Nope : Set where

data Void : Set where

-------------------------------------------------------------------------------

¬_ : Set → Set
¬ A = A → False -- ≈ Nope ≈ Empty ≈ Void

contrapositive : ∀ {A B}
                 → (A → B)
                 → (¬ B → ¬ A)
-- contrapositive f g a = g (f a)
contrapositive a→b b→nope = a→nope
  where a→nope = λ a → b→nope (a→b a)