Core.agda

{-# OPTIONS --rewriting #-}

-- The phase distinction for extension.

module Calf.Phase.Core where

open import Calf.Prelude


-- Extensional phase.

postulate
  ext : Ω