------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles for local algebraic structures
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Apartness.Bundles where
open import Level using (_⊔_; suc)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (ApartnessRelation)
open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Bundles using (CommutativeRing)
open import Algebra.Apartness.Structures using (IsHeytingCommutativeRing; IsHeytingField)
record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_ _#_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_#_ : Rel Carrier ℓ₂
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
-_ : Op₁ Carrier
0# : Carrier
1# : Carrier
isHeytingCommutativeRing : IsHeytingCommutativeRing _≈_ _#_ _+_ _*_ -_ 0# 1#
open IsHeytingCommutativeRing isHeytingCommutativeRing public
commutativeRing : CommutativeRing c ℓ₁
commutativeRing = record { isCommutativeRing = isCommutativeRing }
apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
apartnessRelation = record { isApartnessRelation = isApartnessRelation }
record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 8 -_
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_ _#_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_#_ : Rel Carrier ℓ₂
_+_ : Op₂ Carrier
_*_ : Op₂ Carrier
-_ : Op₁ Carrier
0# : Carrier
1# : Carrier
isHeytingField : IsHeytingField _≈_ _#_ _+_ _*_ -_ 0# 1#
open IsHeytingField isHeytingField public
heytingCommutativeRing : HeytingCommutativeRing c ℓ₁ ℓ₂
heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing }
apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
apartnessRelation = record { isApartnessRelation = isApartnessRelation }
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4