blob: 17228ac10c0e9cd28e45125345a0f75261954091 (
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
|
------------------------------------------------------------------------
-- Agda Helium
--
-- Algebraic properties of ordered semigroups
------------------------------------------------------------------------
{-# OPTIONS --safe --without-K #-}
open import Helium.Algebra.Ordered.StrictTotal.Bundles
module Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup
{ℓ₁ ℓ₂ ℓ₃}
(semigroup : Semigroup ℓ₁ ℓ₂ ℓ₃)
where
open Semigroup semigroup
renaming
( trans to <-trans
; irrefl to <-irrefl
; asym to <-asym
)
open import Helium.Algebra.Ordered.StrictTotal.Properties.Magma magma public
using
( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-<
; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤
; ∙-cancelˡ; ∙-cancelʳ; ∙-cancel
; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-<
; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤
)
open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
|
