Agda-2.3.2.2: test/interaction/Issue620.agda

module Issue620 where

module A where
  postulate _+_*_ : Set → Set → Set → Set

postulate X : Set

2X : Set
2X = X A.+ X * X