------------------------------------------------------------------------ -- The Agda standard library -- -- The irrelevance axiom ------------------------------------------------------------------------ module Irrelevance where import Level