Добавление определений к постулатам в Agda

Question

Начиная с модуля Agda, который определяет тип только как постулат

module M where 
  postulate 
   U : Set 

Я хочу иметь возможность определять U по-разному. Например:

module B where 
  open M public 
  -- define U as Bool 

и

module N where 
  open M public 
  -- define U as Nat 

Есть ли способ сделать это в Агде?

Answer 1

AFAIK, вы не можете, постулаты абстрактны.

Вы можете достичь того, что хотите, инвертировав порядок: вместо того, чтобы пытаться определить U внутри module B или N, как высделайте, вместо этого сделайте

module M (U : Set) where

, а затем создайте экземпляр U до Bool или Nat.