------------------------------------------------------------------------
-- The Agda standard library
--
-- Lemmas relating algebraic definitions (such as associativity and
-- commutativity) that don't require the equality relation to be a setoid.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Consequences.Base
{a} {A : Set a} where
open import Algebra.Core using (Op₁; Op₂)
import Algebra.Definitions as Definitions
using (Congruent₂; LeftCongruent; RightCongruent
; Selective; Idempotent; SelfInverse; Involutive)
open import Data.Sum.Base using (_⊎_; reduce)
open import Relation.Binary.Consequences
using (mono₂⇒monoˡ; mono₂⇒monoʳ)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Reflexive)
module Congruence {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_)
(cong : Congruent₂ _∙_) (refl : Reflexive _≈_)
where
∙-congˡ : LeftCongruent _∙_
∙-congˡ {x} = mono₂⇒monoˡ _ _≈_ _≈_ (refl {x = x}) cong x
∙-congʳ : RightCongruent _∙_
∙-congʳ {x} = mono₂⇒monoʳ _≈_ _ _≈_ (refl {x = x}) cong x
module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
sel⇒idem : Selective _∙_ → Idempotent _∙_
sel⇒idem sel x = reduce (sel x x)
module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
SelfInverse f →
Involutive f
reflexive∧selfInverse⇒involutive refl inv _ = inv refl
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.0
reflexive+selfInverse⇒involutive = reflexive∧selfInverse⇒involutive
{-# WARNING_ON_USAGE reflexive+selfInverse⇒involutive
"Warning: reflexive+selfInverse⇒involutive was deprecated in v2.0.
Please use reflexive∧selfInverse⇒involutive instead."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4