{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Construct.Flip.Op where
open import Algebra.Core
open import Algebra.Bundles
import Algebra.Definitions as Def
import Algebra.Structures as Str
import Algebra.Consequences.Setoid as Consequences
import Data.Product as Prod
import Data.Sum as Sum
open import Function.Base using (flip)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
open import Relation.Binary.Definitions using (Symmetric)
private
variable
a ℓ : Level
A : Set a
≈ : Rel A ℓ
ε : A
⁻¹ : Op₁ A
∙ : Op₂ A
preserves₂ : (∼ ≈ ≋ : Rel A ℓ) →
∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋
preserves₂ _ _ _ pres = flip pres
module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where
open Def ≈
associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙)
associative sym assoc x y z = sym (assoc z y x)
identity : Identity ε ∙ → Identity ε (flip ∙)
identity id = Prod.swap id
commutative : Commutative ∙ → Commutative (flip ∙)
commutative comm = flip comm
selective : Selective ∙ → Selective (flip ∙)
selective sel x y = Sum.swap (sel y x)
idempotent : Idempotent ∙ → Idempotent (flip ∙)
idempotent idem = idem
inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙)
inverse inv = Prod.swap inv
zero : Zero ε ∙ → Zero ε (flip ∙)
zero zer = Prod.swap zer
module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where
open Def ≈
distributes : * DistributesOver + → (flip *) DistributesOver +
distributes distrib = Prod.swap distrib
module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where
open Def ≈
open Str ≈
open ∙-Properties ≈ ∙
isMagma : IsMagma ∙ → IsMagma (flip ∙)
isMagma m = record
{ isEquivalence = isEquivalence
; ∙-cong = preserves₂ ≈ ≈ ≈ ∙-cong
}
where open IsMagma m
isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙)
isSelectiveMagma m = record
{ isMagma = isMagma m.isMagma
; sel = selective m.sel
}
where module m = IsSelectiveMagma m
isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙)
isCommutativeMagma m = record
{ isMagma = isMagma m.isMagma
; comm = commutative m.comm
}
where module m = IsCommutativeMagma m
isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙)
isSemigroup s = record
{ isMagma = isMagma s.isMagma
; assoc = associative s.sym s.assoc
}
where module s = IsSemigroup s
isBand : IsBand ∙ → IsBand (flip ∙)
isBand b = record
{ isSemigroup = isSemigroup b.isSemigroup
; idem = b.idem
}
where module b = IsBand b
isCommutativeSemigroup : IsCommutativeSemigroup ∙ →
IsCommutativeSemigroup (flip ∙)
isCommutativeSemigroup s = record
{ isSemigroup = isSemigroup s.isSemigroup
; comm = commutative s.comm
}
where module s = IsCommutativeSemigroup s
isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε
isUnitalMagma m = record
{ isMagma = isMagma m.isMagma
; identity = identity m.identity
}
where module m = IsUnitalMagma m
isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε
isMonoid m = record
{ isSemigroup = isSemigroup m.isSemigroup
; identity = identity m.identity
}
where module m = IsMonoid m
isCommutativeMonoid : IsCommutativeMonoid ∙ ε →
IsCommutativeMonoid (flip ∙) ε
isCommutativeMonoid m = record
{ isMonoid = isMonoid m.isMonoid
; comm = commutative m.comm
}
where module m = IsCommutativeMonoid m
isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε →
IsIdempotentCommutativeMonoid (flip ∙) ε
isIdempotentCommutativeMonoid m = record
{ isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
; idem = idempotent m.idem
}
where module m = IsIdempotentCommutativeMonoid m
isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ →
IsInvertibleMagma (flip ∙) ε ⁻¹
isInvertibleMagma m = record
{ isMagma = isMagma m.isMagma
; inverse = inverse m.inverse
; ⁻¹-cong = m.⁻¹-cong
}
where module m = IsInvertibleMagma m
isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ →
IsInvertibleUnitalMagma (flip ∙) ε ⁻¹
isInvertibleUnitalMagma m = record
{ isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
; identity = identity m.identity
}
where module m = IsInvertibleUnitalMagma m
isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹
isGroup g = record
{ isMonoid = isMonoid g.isMonoid
; inverse = inverse g.inverse
; ⁻¹-cong = g.⁻¹-cong
}
where module g = IsGroup g
isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹
isAbelianGroup g = record
{ isGroup = isGroup g.isGroup
; comm = commutative g.comm
}
where module g = IsAbelianGroup g
module _ {≈ : Rel A ℓ} {+ * : Op₂ A} {0# 1# : A} where
open Str ≈
open ∙-Properties ≈ *
open *-Properties ≈ * +
isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# →
IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1#
isSemiringWithoutAnnihilatingZero r = record
{ +-isCommutativeMonoid = r.+-isCommutativeMonoid
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; *-identity = identity r.*-identity
; distrib = distributes r.distrib
}
where module r = IsSemiringWithoutAnnihilatingZero r
isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1#
isSemiring r = record
{ isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero
; zero = zero r.zero
}
where module r = IsSemiring r
isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# →
IsCommutativeSemiring + (flip *) 0# 1#
isCommutativeSemiring r = record
{ isSemiring = isSemiring r.isSemiring
; *-comm = commutative r.*-comm
}
where module r = IsCommutativeSemiring r
isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# →
IsCancellativeCommutativeSemiring + (flip *) 0# 1#
isCancellativeCommutativeSemiring r = record
{ isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring
; *-cancelˡ-nonZero = Consequences.comm+almostCancelˡ⇒almostCancelʳ r.setoid r.*-comm r.*-cancelˡ-nonZero
}
where module r = IsCancellativeCommutativeSemiring r
isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# →
IsIdempotentSemiring + (flip *) 0# 1#
isIdempotentSemiring r = record
{ isSemiring = isSemiring r.isSemiring
; +-idem = r.+-idem
}
where module r = IsIdempotentSemiring r
isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1#
isQuasiring r = record
{ +-isMonoid = r.+-isMonoid
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; *-identity = identity r.*-identity
; distrib = distributes r.distrib
; zero = zero r.zero
}
where module r = IsQuasiring r
module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# : A} where
open Str ≈
open ∙-Properties ≈ *
open *-Properties ≈ * +
isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0#
isRingWithoutOne r = record
{ +-isAbelianGroup = r.+-isAbelianGroup
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; distrib = distributes r.distrib
; zero = zero r.zero
}
where module r = IsRingWithoutOne r
module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where
open Str ≈
open ∙-Properties ≈ *
open *-Properties ≈ * +
isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# →
IsNonAssociativeRing + (flip *) - 0# 1#
isNonAssociativeRing r = record
{ +-isAbelianGroup = r.+-isAbelianGroup
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; identity = identity r.identity
; distrib = distributes r.distrib
; zero = zero r.zero
}
where module r = IsNonAssociativeRing r
isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# -
isNearring r = record
{ isQuasiring = isQuasiring r.isQuasiring
; +-inverse = r.+-inverse
; ⁻¹-cong = r.⁻¹-cong
}
where module r = IsNearring r
isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1#
isRing r = record
{ +-isAbelianGroup = r.+-isAbelianGroup
; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
; *-assoc = associative r.sym r.*-assoc
; *-identity = identity r.*-identity
; distrib = distributes r.distrib
; zero = zero r.zero
}
where module r = IsRing r
isCommutativeRing : IsCommutativeRing + * - 0# 1# →
IsCommutativeRing + (flip *) - 0# 1#
isCommutativeRing r = record
{ isRing = isRing r.isRing
; *-comm = commutative r.*-comm
}
where module r = IsCommutativeRing r
magma : Magma a ℓ → Magma a ℓ
magma m = record { isMagma = isMagma m.isMagma }
where module m = Magma m
commutativeMagma : CommutativeMagma a ℓ → CommutativeMagma a ℓ
commutativeMagma m = record
{ isCommutativeMagma = isCommutativeMagma m.isCommutativeMagma
}
where module m = CommutativeMagma m
selectiveMagma : SelectiveMagma a ℓ → SelectiveMagma a ℓ
selectiveMagma m = record
{ isSelectiveMagma = isSelectiveMagma m.isSelectiveMagma
}
where module m = SelectiveMagma m
semigroup : Semigroup a ℓ → Semigroup a ℓ
semigroup s = record { isSemigroup = isSemigroup s.isSemigroup }
where module s = Semigroup s
band : Band a ℓ → Band a ℓ
band b = record { isBand = isBand b.isBand }
where module b = Band b
commutativeSemigroup : CommutativeSemigroup a ℓ → CommutativeSemigroup a ℓ
commutativeSemigroup s = record
{ isCommutativeSemigroup = isCommutativeSemigroup s.isCommutativeSemigroup
}
where module s = CommutativeSemigroup s
unitalMagma : UnitalMagma a ℓ → UnitalMagma a ℓ
unitalMagma m = record
{ isUnitalMagma = isUnitalMagma m.isUnitalMagma
}
where module m = UnitalMagma m
monoid : Monoid a ℓ → Monoid a ℓ
monoid m = record { isMonoid = isMonoid m.isMonoid }
where module m = Monoid m
commutativeMonoid : CommutativeMonoid a ℓ → CommutativeMonoid a ℓ
commutativeMonoid m = record
{ isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
}
where module m = CommutativeMonoid m
idempotentCommutativeMonoid : IdempotentCommutativeMonoid a ℓ →
IdempotentCommutativeMonoid a ℓ
idempotentCommutativeMonoid m = record
{ isIdempotentCommutativeMonoid =
isIdempotentCommutativeMonoid m.isIdempotentCommutativeMonoid
}
where module m = IdempotentCommutativeMonoid m
invertibleMagma : InvertibleMagma a ℓ → InvertibleMagma a ℓ
invertibleMagma m = record
{ isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
}
where module m = InvertibleMagma m
invertibleUnitalMagma : InvertibleUnitalMagma a ℓ → InvertibleUnitalMagma a ℓ
invertibleUnitalMagma m = record
{ isInvertibleUnitalMagma = isInvertibleUnitalMagma m.isInvertibleUnitalMagma
}
where module m = InvertibleUnitalMagma m
group : Group a ℓ → Group a ℓ
group g = record { isGroup = isGroup g.isGroup }
where module g = Group g
abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ
abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup }
where module g = AbelianGroup g
semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ →
SemiringWithoutAnnihilatingZero a ℓ
semiringWithoutAnnihilatingZero r = record
{ isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero }
where module r = SemiringWithoutAnnihilatingZero r
semiring : Semiring a ℓ → Semiring a ℓ
semiring r = record { isSemiring = isSemiring r.isSemiring }
where module r = Semiring r
commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ
commutativeSemiring r = record
{ isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring }
where module r = CommutativeSemiring r
cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ →
CancellativeCommutativeSemiring a ℓ
cancellativeCommutativeSemiring r = record
{ isCancellativeCommutativeSemiring = isCancellativeCommutativeSemiring r.isCancellativeCommutativeSemiring }
where module r = CancellativeCommutativeSemiring r
idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ
idempotentSemiring r = record
{ isIdempotentSemiring = isIdempotentSemiring r.isIdempotentSemiring }
where module r = IdempotentSemiring r
quasiring : Quasiring a ℓ → Quasiring a ℓ
quasiring r = record { isQuasiring = isQuasiring r.isQuasiring }
where module r = Quasiring r
ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ
ringWithoutOne r = record { isRingWithoutOne = isRingWithoutOne r.isRingWithoutOne }
where module r = RingWithoutOne r
nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ
nonAssociativeRing r = record
{ isNonAssociativeRing = isNonAssociativeRing r.isNonAssociativeRing }
where module r = NonAssociativeRing r
nearring : Nearring a ℓ → Nearring a ℓ
nearring r = record { isNearring = isNearring r.isNearring }
where module r = Nearring r
ring : Ring a ℓ → Ring a ℓ
ring r = record { isRing = isRing r.isRing }
where module r = Ring r
commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing }
where module r = CommutativeRing r