This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The precategory of rings

module ring-theory.precategory-of-rings where
Imports 
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

open import ring-theory.homomorphisms-rings
open import ring-theory.rings

Idea

The (large) precategory of rings consists of rings and ring homomorphisms.

Definitions

The large precategory of rings

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

The precategory or rings of universe level l

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