{-# 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