Structures.agda

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