{-# OPTIONS --without-K #-} module equality where open import equality.core public open import equality.reasoning public open import equality.calculus public