Agda-2.3.2.2: test/succeed/Squash.agda

module Squash where

data _==_ {A : Set}(a : A) : A -> Set where
  refl : a == a

data Wrap (A : Set) : Set where
  wrap : A -> Wrap A

data Squash (A : Set) : Set where
  squash : .A -> Squash A

postulate
  A : Set
  a1 a2 : A

irr : squash a1 == squash a2
irr = refl