```------------------------------------------------------------------------
-- 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

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
```