Fields Continued…

We now define objects of the field family, as we did for groups and rings before.

``````open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)

open import Types.product
open import Types.relations
open import Types.equality

open import Algebra.order
open import Algebra.groups
open import Algebra.groups2
open import Algebra.rings
open import Algebra.rings2
open import Algebra.fields

module Algebra.fields2 where``````

Fields

``````record Field c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix  9 ÷_
infix  8 -_
infixl 7 _*_
infixl 6 _+_
infix  4 _≈_
field
Data     : Set c
_≈_      : Rel Data ℓ
_+_      : ★ Data
_*_      : ★ Data
-_       : ♠ Data
÷_       : ♠ Data
0#       : Data
1#       : Data
isField  : IsField _≈_ _+_ _*_ -_ ÷_ 0# 1#

open IsField isField public

ring : Ring _ _
ring = record { isRing = isRing }

open Ring ring public
using
( +-magma; +-semigroup; +-abelianGroup
; *-magma; *-semigroup
; +-monoid ; +-commutativeMonoid
; *-monoid
; nearSemiring; semiringWithoutOne; semiring
; semiringWithoutAnnihilatingZero
)``````

Ordered Fields

``````record OrderedField c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix  9 ÷_
infix  8 -_
infixl 7 _*_
infixl 6 _+_
infix  4 _≈_
field
Data            : Set c
_≈_             : Rel Data ℓ
_≤_             : Rel Data ℓ
_+_             : ★ Data
_*_             : ★ Data
-_              : ♠ Data
÷_              : ♠ Data
0#              : Data
1#              : Data
isOrderedField  : IsOrderedField _≈_ _+_ _*_ -_ ÷_ _≤_ 0# 1#

open IsOrderedField isOrderedField public

ring : Ring _ _
ring = record { isRing = isRing }

open Ring ring public
using
( +-magma; +-semigroup; +-abelianGroup
; *-magma; *-semigroup
; +-monoid ; +-commutativeMonoid
; *-monoid
; nearSemiring; semiringWithoutOne; semiring
; semiringWithoutAnnihilatingZero
)``````

Numbers