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 category of rings
module ring-theory.category-of-rings where
Imports
open import category-theory.categories open import category-theory.large-categories open import foundation.universe-levels open import ring-theory.isomorphisms-rings open import ring-theory.precategory-of-rings
Idea
The large category Ring-Category of
rings is the large category consistsing of rings and
ring homomorphisms.
Definitions
The large category of rings
is-large-category-Ring-Large-Category : is-large-category-Large-Precategory Ring-Large-Precategory is-large-category-Ring-Large-Category = is-equiv-iso-eq-Ring Ring-Large-Category : Large-Category lsuc (_⊔_) large-precategory-Large-Category Ring-Large-Category = Ring-Large-Precategory is-large-category-Large-Category Ring-Large-Category = is-large-category-Ring-Large-Category
The small categories of rings
Ring-Category : (l : Level) → Category (lsuc l) l Ring-Category = category-Large-Category Ring-Large-Category