Crash.agda

module Crash where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Bool : Set where
  true : Bool
  false : Bool

F : Bool -> Set
F true  = Nat
F false = Bool

not : Bool -> Bool
not true  = false
not false = true

h : ((x : F ?) -> F (not x)) -> Nat
h g = g zero