------------------------------------------------------------------------ -- The Agda standard library -- -- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Definitions using (Substitutive; Symmetric; Total) module Algebra.FunctionProperties.Consequences {a ℓ} (S : Setoid a ℓ) where {-# WARNING_ON_IMPORT "Algebra.FunctionProperties.Consequences was deprecated in v1.3. Use Algebra.Consequences.Setoid instead." #-} open import Algebra.Consequences.Setoid S public