{-# OPTIONS --rewriting #-} -- The phase distinction for extension. module Calf.Phase.Core where open import Calf.Prelude -- Extensional phase. postulate ext : Ω