------------------------------------------------------------------------ -- The Agda standard library -- -- This module is DEPRECATED. Please use -- Data.Sum.Relation.Binary.Pointwise directly. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Sum.Relation.Pointwise where open import Data.Sum.Relation.Binary.Pointwise public