The precategory of rings

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-06.
Last modified on 2024-03-11.

module ring-theory.precategory-of-rings where
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


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


The large precategory of rings

Ring-Large-Precategory : Large-Precategory (lsuc) (_⊔_)
Ring-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

Recent changes