blob: 91d4b3e68b39ca7acaee9fbba45687c227dcf657 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of ordered magmas
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Algebra.Ordered.StrictTotal.Bundles
module Helium.Algebra.Ordered.StrictTotal.Properties.Magma
{ℓ₁ ℓ₂ ℓ₃}
(magma : Magma ℓ₁ ℓ₂ ℓ₃)
where
open Magma magma
renaming
( trans to <-trans
; irrefl to <-irrefl
; asym to <-asym
)
open import Algebra.Definitions
open import Data.Product using (_,_)
open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder
open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
--------------------------------------------------------------------------------
-- Properties of _∙_
---- Congruences
-- _<_
∙-mono-< : Congruent₂ _<_ _∙_
∙-mono-< = invariant⇒mono-< ∙-invariant
∙-monoˡ-< : LeftCongruent _<_ _∙_
∙-monoˡ-< = invariantˡ⇒monoˡ-< ∙-invariantˡ
∙-monoʳ-< : RightCongruent _<_ _∙_
∙-monoʳ-< = invariantʳ⇒monoʳ-< ∙-invariantʳ
-- _≤_
∙-mono-≤ : Congruent₂ _≤_ _∙_
∙-mono-≤ = cong+invariant⇒mono-≤ ∙-cong ∙-invariant
∙-monoˡ-≤ : LeftCongruent _≤_ _∙_
∙-monoˡ-≤ {x} = congˡ+monoˡ-<⇒monoˡ-≤ (∙-congˡ {x}) (∙-monoˡ-< {x}) {x}
∙-monoʳ-≤ : RightCongruent _≤_ _∙_
∙-monoʳ-≤ {x} = congʳ+monoʳ-<⇒monoʳ-≤ (∙-congʳ {x}) (∙-monoʳ-< {x}) {x}
---- Cancelling
-- _≈_
∙-cancelˡ : LeftCancellative _≈_ _∙_
∙-cancelˡ = monoˡ-<⇒cancelˡ ∙-monoˡ-<
∙-cancelʳ : RightCancellative _≈_ _∙_
∙-cancelʳ {x} = monoʳ-<⇒cancelʳ (∙-monoʳ-< {x}) {x}
∙-cancel : Cancellative _≈_ _∙_
∙-cancel = ∙-cancelˡ , ∙-cancelʳ
-- _<_
∙-cancelˡ-< : LeftCancellative _<_ _∙_
∙-cancelˡ-< = monoˡ-≤⇒cancelˡ-< ∙-monoˡ-≤
∙-cancelʳ-< : RightCancellative _<_ _∙_
∙-cancelʳ-< {x} = monoʳ-≤⇒cancelʳ-< (∙-monoʳ-≤ {x}) {x}
∙-cancel-< : Cancellative _<_ _∙_
∙-cancel-< = ∙-cancelˡ-< , ∙-cancelʳ-<
-- _≤_
∙-cancelˡ-≤ : LeftCancellative _≤_ _∙_
∙-cancelˡ-≤ = monoˡ-<⇒cancelˡ-≤ ∙-monoˡ-<
∙-cancelʳ-≤ : RightCancellative _≤_ _∙_
∙-cancelʳ-≤ {x} = monoʳ-<⇒cancelʳ-≤ (∙-monoʳ-< {x}) {x}
∙-cancel-≤ : Cancellative _≤_ _∙_
∙-cancel-≤ = ∙-cancelˡ-≤ , ∙-cancelʳ-≤
|
