The precategory of semirings

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-06.

module ring-theory.precategory-of-semirings where

Imports
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

open import ring-theory.homomorphisms-semirings
open import ring-theory.semirings


Idea

The {{#concet "precategory of semirings" Agda=Semiring-Large-Precategory}} consists of semirings and homomorphisms of semirings.

Definitions

The large precategory of semirings

Semiring-Large-Precategory : Large-Precategory lsuc (_⊔_)
Semiring-Large-Precategory =
make-Large-Precategory
( Semiring)
( hom-set-Semiring)
( λ {l1} {l2} {l3} {R} {S} {T} → comp-hom-Semiring R S T)
( λ {l} {R} → id-hom-Semiring R)
( λ {l1} {l2} {l3} {l4} {R} {S} {T} {U} →
associative-comp-hom-Semiring R S T U)
( λ {l1} {l2} {R} {S} → left-unit-law-comp-hom-Semiring R S)
( λ {l1} {l2} {R} {S} → right-unit-law-comp-hom-Semiring R S)


The precategory of small semirings

Semiring-Precategory : (l : Level) → Precategory (lsuc l) l
Semiring-Precategory = precategory-Large-Precategory Semiring-Large-Precategory