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

Initial rings

module ring-theory.initial-rings where

open import category-theory.initial-objects-large-categories

open import foundation.universe-levels

open import ring-theory.category-of-rings
open import ring-theory.rings

Idea

The initial ring is a ring R that satisfies the universal property that for any ring S, the type

  hom-Ring R S

of ring homomorphisms from R to S is contractible.

In elementary-number-theory.ring-of-integers we will show that ℤ is the initial ring.

Definitions

module _
  {l : Level} (R : Ring l)
  where

  is-initial-Ring : UUω
  is-initial-Ring = is-initial-obj-Large-Category Ring-Large-Category R