    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Algebraic structures with an apartness relation
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Algebra.Core using (Op₁; Op₂)
    open import Relation.Binary.Core using (Rel)

    module Algebra.Apartness.Structures
      {c ℓ₁ ℓ₂} {Carrier : Set c}
      (_≈_ : Rel Carrier ℓ₁)
      (_#_ : Rel Carrier ℓ₂)
      (_+_ _*_ : Op₂ Carrier) (-_ : Op₁ Carrier) (0# 1# : Carrier)
      where

    open import Level using (_⊔_; suc)
    open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂)
    open import Algebra.Definitions _≈_ using (Invertible)
    open import Algebra.Structures _≈_ using (IsCommutativeRing)
    open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
    open import Relation.Binary.Definitions using (Tight)
    open import Relation.Nullary.Negation using (¬_)
    import Relation.Binary.Properties.ApartnessRelation as AR

    record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where

      field
        isCommutativeRing   : IsCommutativeRing _+_ _*_ -_ 0# 1#
        isApartnessRelation : IsApartnessRelation _≈_ _#_

      open IsCommutativeRing isCommutativeRing public
      open IsApartnessRelation isApartnessRelation public
        renaming
          ( irrefl  to #-irrefl
          ; sym     to #-sym
          ; cotrans to #-cotrans
          )

      field
        #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
        invertible⇒# : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y

      ¬#-isEquivalence : IsEquivalence _¬#_
      ¬#-isEquivalence = AR.¬#-isEquivalence refl isApartnessRelation

    record IsHeytingField : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where

      field
        isHeytingCommutativeRing : IsHeytingCommutativeRing
        tight                    : Tight _≈_ _#_

      open IsHeytingCommutativeRing isHeytingCommutativeRing public