opposite of a Ring [clean version of pr #1900] (#1910)

CHANGELOG.md

@@ -1636,6 +1636,41 @@ Other minor changes
  moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
  ```
 
+* Added new functions and proofs to `Algebra.Construct.Flip.Op`:
+ ```agda
+ zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
+ distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
+ isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# →
+ IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1#
+ isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1#
+ isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# →
+ IsCommutativeSemiring + (flip *) 0# 1#
+ isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# →
+ IsCancellativeCommutativeSemiring + (flip *) 0# 1#
+ isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# →
+ IsIdempotentSemiring + (flip *) 0# 1#
+ isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1#
+ isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0#
+ isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# →
+ IsNonAssociativeRing + (flip *) - 0# 1#
+ isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
+ isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# -
+ isCommutativeRing : IsCommutativeRing + * - 0# 1# →
+ IsCommutativeRing + (flip *) - 0# 1#
+ semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ →
+ SemiringWithoutAnnihilatingZero a ℓ
+ commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ
+ cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ →
+ CancellativeCommutativeSemiring a ℓ
+ idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ
+ quasiring : Quasiring a ℓ → Quasiring a ℓ
+ ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ
+ nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ
+ nearring : Nearring a ℓ → Nearring a ℓ
+ ring : Ring a ℓ → Ring a ℓ
+ commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
+ ```
+
 * Added new definition to `Algebra.Definitions`:
  ```agda
  LeftDividesˡ : Op₂ A → Op₂ A → Set _