Normal submonoids of commutative monoids

module group-theory.normal-submonoids-commutative-monoids where

open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.equivalence-relations
open import foundation.equivalences
open import foundation.functions
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.retractions
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.commutative-monoids
open import group-theory.congruence-relations-commutative-monoids
open import group-theory.monoids
open import group-theory.saturated-congruence-relations-commutative-monoids
open import group-theory.semigroups
open import group-theory.submonoids-commutative-monoids
open import group-theory.subsets-commutative-monoids

Idea

A normal submonoid N of of a commutative monoid M is a submonoid that corresponds uniquely to a saturated congruence relation ~ on M consisting of the elements congruent to 1. This is the case if and only if for all x : M and u : N we have

  xu ∈ N → x ∈ N

Definitions

Normal submonoids of commutative monoids

module _
  {l1 l2 : Level} (M : Commutative-Monoid l1) (N : Commutative-Submonoid l2 M)
  where

  is-normal-commutative-submonoid-Prop : Prop (l1 ⊔ l2)
  is-normal-commutative-submonoid-Prop =
    Π-Prop
      ( type-Commutative-Monoid M)
      ( λ x →
        Π-Prop
          ( type-Commutative-Monoid M)
          ( λ u →
            function-Prop
              ( is-in-Commutative-Submonoid M N u)
              ( function-Prop
                ( is-in-Commutative-Submonoid M N
                  ( mul-Commutative-Monoid M x u))
                ( subset-Commutative-Submonoid M N x))))

  is-normal-Commutative-Submonoid : UU (l1 ⊔ l2)
  is-normal-Commutative-Submonoid =
    type-Prop is-normal-commutative-submonoid-Prop

  is-prop-is-normal-Commutative-Submonoid :
    is-prop is-normal-Commutative-Submonoid
  is-prop-is-normal-Commutative-Submonoid =
    is-prop-type-Prop is-normal-commutative-submonoid-Prop

Normal-Commutative-Submonoid :
  {l1 : Level} (l2 : Level) → Commutative-Monoid l1 → UU (l1 ⊔ lsuc l2)
Normal-Commutative-Submonoid l2 M =
  Σ (Commutative-Submonoid l2 M) (is-normal-Commutative-Submonoid M)

module _
  {l1 l2 : Level} (M : Commutative-Monoid l1)
  (N : Normal-Commutative-Submonoid l2 M)
  where

  submonoid-Normal-Commutative-Submonoid : Commutative-Submonoid l2 M
  submonoid-Normal-Commutative-Submonoid = pr1 N

  is-normal-Normal-Commutative-Submonoid :
    is-normal-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid
  is-normal-Normal-Commutative-Submonoid = pr2 N

  subset-Normal-Commutative-Submonoid : subtype l2 (type-Commutative-Monoid M)
  subset-Normal-Commutative-Submonoid =
    subset-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  is-submonoid-Normal-Commutative-Submonoid :
    is-submonoid-Commutative-Monoid M subset-Normal-Commutative-Submonoid
  is-submonoid-Normal-Commutative-Submonoid =
    is-submonoid-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  is-in-Normal-Commutative-Submonoid : type-Commutative-Monoid M → UU l2
  is-in-Normal-Commutative-Submonoid =
    is-in-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  is-prop-is-in-Normal-Commutative-Submonoid :
    (x : type-Commutative-Monoid M) →
    is-prop (is-in-Normal-Commutative-Submonoid x)
  is-prop-is-in-Normal-Commutative-Submonoid =
    is-prop-is-in-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

  is-closed-under-eq-Normal-Commutative-Submonoid :
    {x y : type-Commutative-Monoid M} →
    is-in-Normal-Commutative-Submonoid x → (x ＝ y) →
    is-in-Normal-Commutative-Submonoid y
  is-closed-under-eq-Normal-Commutative-Submonoid =
    is-closed-under-eq-subtype subset-Normal-Commutative-Submonoid

  is-closed-under-eq-Normal-Commutative-Submonoid' :
    {x y : type-Commutative-Monoid M} → is-in-Normal-Commutative-Submonoid y →
    (x ＝ y) → is-in-Normal-Commutative-Submonoid x
  is-closed-under-eq-Normal-Commutative-Submonoid' =
    is-closed-under-eq-subtype' subset-Normal-Commutative-Submonoid

  type-Normal-Commutative-Submonoid : UU (l1 ⊔ l2)
  type-Normal-Commutative-Submonoid =
    type-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  is-set-type-Normal-Commutative-Submonoid :
    is-set type-Normal-Commutative-Submonoid
  is-set-type-Normal-Commutative-Submonoid =
    is-set-type-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  set-Normal-Commutative-Submonoid : Set (l1 ⊔ l2)
  set-Normal-Commutative-Submonoid =
    set-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  inclusion-Normal-Commutative-Submonoid :
    type-Normal-Commutative-Submonoid → type-Commutative-Monoid M
  inclusion-Normal-Commutative-Submonoid =
    inclusion-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  ap-inclusion-Normal-Commutative-Submonoid :
    (x y : type-Normal-Commutative-Submonoid) → x ＝ y →
    inclusion-Normal-Commutative-Submonoid x ＝
    inclusion-Normal-Commutative-Submonoid y
  ap-inclusion-Normal-Commutative-Submonoid =
    ap-inclusion-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  is-in-submonoid-inclusion-Normal-Commutative-Submonoid :
    (x : type-Normal-Commutative-Submonoid) →
    is-in-Normal-Commutative-Submonoid
      ( inclusion-Normal-Commutative-Submonoid x)
  is-in-submonoid-inclusion-Normal-Commutative-Submonoid =
    is-in-submonoid-inclusion-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

  contains-unit-Normal-Commutative-Submonoid :
    is-in-Normal-Commutative-Submonoid (unit-Commutative-Monoid M)
  contains-unit-Normal-Commutative-Submonoid =
    contains-unit-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  unit-Normal-Commutative-Submonoid : type-Normal-Commutative-Submonoid
  unit-Normal-Commutative-Submonoid =
    unit-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  is-closed-under-mul-Normal-Commutative-Submonoid :
    {x y : type-Commutative-Monoid M} →
    is-in-Normal-Commutative-Submonoid x →
    is-in-Normal-Commutative-Submonoid y →
    is-in-Normal-Commutative-Submonoid (mul-Commutative-Monoid M x y)
  is-closed-under-mul-Normal-Commutative-Submonoid =
    is-closed-under-mul-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

  mul-Normal-Commutative-Submonoid :
    (x y : type-Normal-Commutative-Submonoid) →
    type-Normal-Commutative-Submonoid
  mul-Normal-Commutative-Submonoid =
    mul-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  associative-mul-Normal-Commutative-Submonoid :
    (x y z : type-Normal-Commutative-Submonoid) →
    ( mul-Normal-Commutative-Submonoid
      ( mul-Normal-Commutative-Submonoid x y)
      ( z)) ＝
    ( mul-Normal-Commutative-Submonoid x
      ( mul-Normal-Commutative-Submonoid y z))
  associative-mul-Normal-Commutative-Submonoid =
    associative-mul-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

  semigroup-Normal-Commutative-Submonoid : Semigroup (l1 ⊔ l2)
  semigroup-Normal-Commutative-Submonoid =
    semigroup-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  left-unit-law-mul-Normal-Commutative-Submonoid :
    (x : type-Normal-Commutative-Submonoid) →
    mul-Normal-Commutative-Submonoid unit-Normal-Commutative-Submonoid x ＝ x
  left-unit-law-mul-Normal-Commutative-Submonoid =
    left-unit-law-mul-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

  right-unit-law-mul-Normal-Commutative-Submonoid :
    (x : type-Normal-Commutative-Submonoid) →
    mul-Normal-Commutative-Submonoid x unit-Normal-Commutative-Submonoid ＝ x
  right-unit-law-mul-Normal-Commutative-Submonoid =
    right-unit-law-mul-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

  commutative-mul-Normal-Commutative-Submonoid :
    (x y : type-Normal-Commutative-Submonoid) →
    mul-Normal-Commutative-Submonoid x y ＝
    mul-Normal-Commutative-Submonoid y x
  commutative-mul-Normal-Commutative-Submonoid =
    commutative-mul-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

  monoid-Normal-Commutative-Submonoid : Monoid (l1 ⊔ l2)
  monoid-Normal-Commutative-Submonoid =
    monoid-Commutative-Submonoid M submonoid-Normal-Commutative-Submonoid

  commutative-monoid-Normal-Commutative-Submonoid :
    Commutative-Monoid (l1 ⊔ l2)
  commutative-monoid-Normal-Commutative-Submonoid =
    commutative-monoid-Commutative-Submonoid M
      submonoid-Normal-Commutative-Submonoid

Properties

Extensionality of the type of all normal submonoids

module _
  {l1 l2 : Level} (M : Commutative-Monoid l1)
  (N : Normal-Commutative-Submonoid l2 M)
  where

  has-same-elements-Normal-Commutative-Submonoid :
    {l3 : Level} → Normal-Commutative-Submonoid l3 M → UU (l1 ⊔ l2 ⊔ l3)
  has-same-elements-Normal-Commutative-Submonoid K =
    has-same-elements-Commutative-Submonoid M
      ( submonoid-Normal-Commutative-Submonoid M N)
      ( submonoid-Normal-Commutative-Submonoid M K)

  extensionality-Normal-Commutative-Submonoid :
    (K : Normal-Commutative-Submonoid l2 M) →
    (N ＝ K) ≃ has-same-elements-Normal-Commutative-Submonoid K
  extensionality-Normal-Commutative-Submonoid =
    extensionality-type-subtype
      ( is-normal-commutative-submonoid-Prop M)
      ( is-normal-Normal-Commutative-Submonoid M N)
      ( λ x → (id , id))
      ( extensionality-Commutative-Submonoid M
        ( submonoid-Normal-Commutative-Submonoid M N))

  eq-has-same-elements-Normal-Commutative-Submonoid :
    (K : Normal-Commutative-Submonoid l2 M) →
    has-same-elements-Normal-Commutative-Submonoid K → N ＝ K
  eq-has-same-elements-Normal-Commutative-Submonoid K =
    map-inv-equiv (extensionality-Normal-Commutative-Submonoid K)

The congruence relation of a normal submonoid

module _
  {l1 l2 : Level}
  (M : Commutative-Monoid l1) (N : Normal-Commutative-Submonoid l2 M)
  where

  rel-congruence-Normal-Commutative-Submonoid :
    Rel-Prop (l1 ⊔ l2) (type-Commutative-Monoid M)
  rel-congruence-Normal-Commutative-Submonoid x y =
    Π-Prop
      ( type-Commutative-Monoid M)
      ( λ u →
        iff-Prop
          ( subset-Normal-Commutative-Submonoid M N
            ( mul-Commutative-Monoid M u x))
          ( subset-Normal-Commutative-Submonoid M N
            ( mul-Commutative-Monoid M u y)))

  sim-congruence-Normal-Commutative-Submonoid :
    (x y : type-Commutative-Monoid M) → UU (l1 ⊔ l2)
  sim-congruence-Normal-Commutative-Submonoid x y =
    type-Prop (rel-congruence-Normal-Commutative-Submonoid x y)

  refl-congruence-Normal-Commutative-Submonoid :
    is-reflexive-Rel-Prop rel-congruence-Normal-Commutative-Submonoid
  pr1 (refl-congruence-Normal-Commutative-Submonoid u) = id
  pr2 (refl-congruence-Normal-Commutative-Submonoid u) = id

  symmetric-congruence-Normal-Commutative-Submonoid :
    is-symmetric-Rel-Prop rel-congruence-Normal-Commutative-Submonoid
  pr1 (symmetric-congruence-Normal-Commutative-Submonoid H u) = pr2 (H u)
  pr2 (symmetric-congruence-Normal-Commutative-Submonoid H u) = pr1 (H u)

  transitive-congruence-Normal-Commutative-Submonoid :
    is-transitive-Rel-Prop rel-congruence-Normal-Commutative-Submonoid
  transitive-congruence-Normal-Commutative-Submonoid H K u = (K u) ∘iff (H u)

  eq-rel-congruence-Normal-Commutative-Submonoid :
    Eq-Rel (l1 ⊔ l2) (type-Commutative-Monoid M)
  pr1 eq-rel-congruence-Normal-Commutative-Submonoid =
    rel-congruence-Normal-Commutative-Submonoid
  pr1 (pr2 eq-rel-congruence-Normal-Commutative-Submonoid) =
    refl-congruence-Normal-Commutative-Submonoid
  pr1 (pr2 (pr2 eq-rel-congruence-Normal-Commutative-Submonoid)) =
    symmetric-congruence-Normal-Commutative-Submonoid
  pr2 (pr2 (pr2 eq-rel-congruence-Normal-Commutative-Submonoid)) =
    transitive-congruence-Normal-Commutative-Submonoid

  is-congruence-congruence-Normal-Commutative-Submonoid :
    is-congruence-Commutative-Monoid M
      eq-rel-congruence-Normal-Commutative-Submonoid
  pr1
    ( is-congruence-congruence-Normal-Commutative-Submonoid
      {x} {x'} {y} {y'} H K u)
    ( L) =
    is-closed-under-eq-Normal-Commutative-Submonoid M N
      ( forward-implication
        ( K (mul-Commutative-Monoid M u x'))
        ( is-closed-under-eq-Normal-Commutative-Submonoid M N
          ( forward-implication
            ( H (mul-Commutative-Monoid M u y))
            ( is-closed-under-eq-Normal-Commutative-Submonoid M N L
              ( ( inv (associative-mul-Commutative-Monoid M u x y)) ∙
                ( right-swap-mul-Commutative-Monoid M u x y))))
          ( right-swap-mul-Commutative-Monoid M u y x')))
      ( associative-mul-Commutative-Monoid M u x' y')
  pr2
    ( is-congruence-congruence-Normal-Commutative-Submonoid
      {x} {x'} {y} {y'} H K u)
    ( L) =
    is-closed-under-eq-Normal-Commutative-Submonoid M N
      ( backward-implication
        ( K (mul-Commutative-Monoid M u x))
        ( is-closed-under-eq-Normal-Commutative-Submonoid M N
          ( backward-implication
            ( H (mul-Commutative-Monoid M u y'))
            ( is-closed-under-eq-Normal-Commutative-Submonoid M N L
              ( ( inv (associative-mul-Commutative-Monoid M u x' y')) ∙
                ( right-swap-mul-Commutative-Monoid M u x' y'))))
          ( right-swap-mul-Commutative-Monoid M u y' x)))
      ( associative-mul-Commutative-Monoid M u x y)

  congruence-Normal-Commutative-Submonoid :
    congruence-Commutative-Monoid (l1 ⊔ l2) M
  pr1 congruence-Normal-Commutative-Submonoid =
    eq-rel-congruence-Normal-Commutative-Submonoid
  pr2 congruence-Normal-Commutative-Submonoid =
    is-congruence-congruence-Normal-Commutative-Submonoid

The normal submonoid obtained from a congruence relation

module _
  {l1 l2 : Level} (M : Commutative-Monoid l1)
  (R : congruence-Commutative-Monoid l2 M)
  where

  subset-normal-submonoid-congruence-Commutative-Monoid :
    subtype l2 (type-Commutative-Monoid M)
  subset-normal-submonoid-congruence-Commutative-Monoid x =
    prop-congruence-Commutative-Monoid M R x (unit-Commutative-Monoid M)

  is-in-normal-submonoid-congruence-Commutative-Monoid :
    type-Commutative-Monoid M → UU l2
  is-in-normal-submonoid-congruence-Commutative-Monoid =
    is-in-subtype subset-normal-submonoid-congruence-Commutative-Monoid

  contains-unit-normal-submonoid-congruence-Commutative-Monoid :
    is-in-normal-submonoid-congruence-Commutative-Monoid
      ( unit-Commutative-Monoid M)
  contains-unit-normal-submonoid-congruence-Commutative-Monoid =
    refl-congruence-Commutative-Monoid M R

  is-closed-under-multiplication-normal-submonoid-congruence-Commutative-Monoid :
    is-closed-under-multiplication-subset-Commutative-Monoid M
      subset-normal-submonoid-congruence-Commutative-Monoid
  is-closed-under-multiplication-normal-submonoid-congruence-Commutative-Monoid
    x y H K =
    concatenate-sim-eq-congruence-Commutative-Monoid M R
      ( mul-congruence-Commutative-Monoid M R H K)
      ( left-unit-law-mul-Commutative-Monoid M (unit-Commutative-Monoid M))

  submonoid-congruence-Commutative-Monoid : Commutative-Submonoid l2 M
  pr1 submonoid-congruence-Commutative-Monoid =
    subset-normal-submonoid-congruence-Commutative-Monoid
  pr1 (pr2 submonoid-congruence-Commutative-Monoid) =
    contains-unit-normal-submonoid-congruence-Commutative-Monoid
  pr2 (pr2 submonoid-congruence-Commutative-Monoid) =
    is-closed-under-multiplication-normal-submonoid-congruence-Commutative-Monoid

  is-normal-submonoid-congruence-Commutative-Monoid :
    is-normal-Commutative-Submonoid M submonoid-congruence-Commutative-Monoid
  is-normal-submonoid-congruence-Commutative-Monoid x u H =
    trans-congruence-Commutative-Monoid M R
      ( symm-congruence-Commutative-Monoid M R
        ( concatenate-sim-eq-congruence-Commutative-Monoid M R
          ( mul-congruence-Commutative-Monoid M R
            ( refl-congruence-Commutative-Monoid M R)
            ( H))
          ( right-unit-law-mul-Commutative-Monoid M x)))

  normal-submonoid-congruence-Commutative-Monoid :
    Normal-Commutative-Submonoid l2 M
  pr1 normal-submonoid-congruence-Commutative-Monoid =
    submonoid-congruence-Commutative-Monoid
  pr2 normal-submonoid-congruence-Commutative-Monoid =
    is-normal-submonoid-congruence-Commutative-Monoid

The normal submonoid obtained from the congruence relation of a normal submonoid has the same elements as the original normal submonoid

module _
  {l1 l2 : Level}
  (M : Commutative-Monoid l1) (N : Normal-Commutative-Submonoid l2 M)
  where

  has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid :
    has-same-elements-Normal-Commutative-Submonoid M
      ( normal-submonoid-congruence-Commutative-Monoid M
        ( congruence-Normal-Commutative-Submonoid M N))
      ( N)
  pr1
    ( has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid
      x)
    ( H) =
    is-closed-under-eq-Normal-Commutative-Submonoid M N
      ( backward-implication
        ( H (unit-Commutative-Monoid M))
        ( is-closed-under-eq-Normal-Commutative-Submonoid' M N
          ( contains-unit-Normal-Commutative-Submonoid M N)
          ( left-unit-law-mul-Commutative-Monoid M
            ( unit-Commutative-Monoid M))))
      ( left-unit-law-mul-Commutative-Monoid M x)
  pr1
    ( pr2
      ( has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid
        ( x))
      ( H)
      ( u))
    ( K)=
    is-closed-under-eq-Normal-Commutative-Submonoid' M N
      ( is-normal-Normal-Commutative-Submonoid M N u x H K)
      ( right-unit-law-mul-Commutative-Monoid M u)
  pr2
    ( pr2
      ( has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid
        ( x))
      ( H)
      ( u))
    ( K) =
    is-closed-under-mul-Normal-Commutative-Submonoid M N
      ( is-closed-under-eq-Normal-Commutative-Submonoid M N K
        ( right-unit-law-mul-Commutative-Monoid M u))
      ( H)

The congruence relation of a normal submonoid is saturated

module _
  {l1 l2 : Level}
  (M : Commutative-Monoid l1) (N : Normal-Commutative-Submonoid l2 M)
  where

  is-saturated-congruence-Normal-Commutative-Submonoid :
    is-saturated-congruence-Commutative-Monoid M
      ( congruence-Normal-Commutative-Submonoid M N)
  is-saturated-congruence-Normal-Commutative-Submonoid x y H u =
    ( ( has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid
        ( M)
        ( N)
        ( mul-Commutative-Monoid M u y)) ∘iff
      ( H u)) ∘iff
    ( inv-iff
      ( has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid
        ( M)
        ( N)
        ( mul-Commutative-Monoid M u x)))

  saturated-congruence-Normal-Commutative-Submonoid :
    saturated-congruence-Commutative-Monoid (l1 ⊔ l2) M
  pr1 saturated-congruence-Normal-Commutative-Submonoid =
    congruence-Normal-Commutative-Submonoid M N
  pr2 saturated-congruence-Normal-Commutative-Submonoid =
    is-saturated-congruence-Normal-Commutative-Submonoid

The congruence relation of the normal submonoid associated to a congruence relation relates the same elements as the original congruence relation

module _
  {l1 l2 : Level}
  (M : Commutative-Monoid l1) (R : saturated-congruence-Commutative-Monoid l2 M)
  where

  normal-submonoid-saturated-congruence-Commutative-Monoid :
    Normal-Commutative-Submonoid l2 M
  normal-submonoid-saturated-congruence-Commutative-Monoid =
    normal-submonoid-congruence-Commutative-Monoid M
      ( congruence-saturated-congruence-Commutative-Monoid M R)

  relate-same-elements-congruence-normal-submonoid-saturated-congruence-Commutative-Monoid :
    relate-same-elements-saturated-congruence-Commutative-Monoid M
      ( saturated-congruence-Normal-Commutative-Submonoid M
        ( normal-submonoid-saturated-congruence-Commutative-Monoid))
      ( R)
  pr1
    ( relate-same-elements-congruence-normal-submonoid-saturated-congruence-Commutative-Monoid
      ( x)
      ( y))
    ( H) =
    is-saturated-saturated-congruence-Commutative-Monoid M R x y H
  pr1
    ( pr2
      ( relate-same-elements-congruence-normal-submonoid-saturated-congruence-Commutative-Monoid
        ( x)
        ( y))
      ( H)
      ( u)) =
    trans-saturated-congruence-Commutative-Monoid M R
      ( mul-saturated-congruence-Commutative-Monoid M R
        ( refl-saturated-congruence-Commutative-Monoid M R)
        ( symm-saturated-congruence-Commutative-Monoid M R H))
  pr2
    ( pr2
      ( relate-same-elements-congruence-normal-submonoid-saturated-congruence-Commutative-Monoid
        ( x)
        ( y))
      ( H)
      ( u)) =
    trans-saturated-congruence-Commutative-Monoid M R
      ( mul-saturated-congruence-Commutative-Monoid M R
        ( refl-saturated-congruence-Commutative-Monoid M R)
        ( H))

The type of normal submonoids of M is a retract of the type of congruence relations of M

issec-congruence-Normal-Commutative-Submonoid :
  {l1 : Level} (l2 : Level) (M : Commutative-Monoid l1)
  (N : Normal-Commutative-Submonoid (l1 ⊔ l2) M) →
  ( normal-submonoid-congruence-Commutative-Monoid M
    ( congruence-Normal-Commutative-Submonoid M N)) ＝
  ( N)
issec-congruence-Normal-Commutative-Submonoid l2 M N =
  eq-has-same-elements-Normal-Commutative-Submonoid M
    ( normal-submonoid-congruence-Commutative-Monoid M
      ( congruence-Normal-Commutative-Submonoid M N))
    ( N)
    ( has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid
      M N)

normal-submonoid-retract-of-congruence-Commutative-Monoid :
  {l1 : Level} (l2 : Level) (M : Commutative-Monoid l1) →
  ( Normal-Commutative-Submonoid (l1 ⊔ l2) M) retract-of
  ( congruence-Commutative-Monoid (l1 ⊔ l2) M)
pr1 (normal-submonoid-retract-of-congruence-Commutative-Monoid l2 M) =
  congruence-Normal-Commutative-Submonoid M
pr1 (pr2 (normal-submonoid-retract-of-congruence-Commutative-Monoid l2 M)) =
  normal-submonoid-congruence-Commutative-Monoid M
pr2 (pr2 (normal-submonoid-retract-of-congruence-Commutative-Monoid l2 M)) =
  issec-congruence-Normal-Commutative-Submonoid l2 M

The type of normal submonoids of M is equivalent to the type of saturated congruence relations on M

issec-saturated-congruence-Normal-Commutative-Submonoid :
  {l1 : Level} (l2 : Level) (M : Commutative-Monoid l1)
  (N : Normal-Commutative-Submonoid (l1 ⊔ l2) M) →
  ( normal-submonoid-saturated-congruence-Commutative-Monoid M
    ( saturated-congruence-Normal-Commutative-Submonoid M N)) ＝
  ( N)
issec-saturated-congruence-Normal-Commutative-Submonoid l2 M N =
  eq-has-same-elements-Normal-Commutative-Submonoid M
    ( normal-submonoid-saturated-congruence-Commutative-Monoid M
      ( saturated-congruence-Normal-Commutative-Submonoid M N))
    ( N)
    ( has-same-elements-normal-submonoid-congruence-Normal-Commutative-Submonoid
      M N)

isretr-saturated-congruence-Normal-Commutative-Submonoid :
  {l1 : Level} (l2 : Level) (M : Commutative-Monoid l1)
  (R : saturated-congruence-Commutative-Monoid (l1 ⊔ l2) M) →
  ( saturated-congruence-Normal-Commutative-Submonoid M
    ( normal-submonoid-saturated-congruence-Commutative-Monoid M R)) ＝
  ( R)
isretr-saturated-congruence-Normal-Commutative-Submonoid l2 M R =
  eq-relate-same-elements-saturated-congruence-Commutative-Monoid M
    ( saturated-congruence-Normal-Commutative-Submonoid M
      ( normal-submonoid-saturated-congruence-Commutative-Monoid M R))
    ( R)
    ( relate-same-elements-congruence-normal-submonoid-saturated-congruence-Commutative-Monoid
      ( M)
      ( R))

is-equiv-normal-submonoid-saturated-congruence-Commutative-Monoid :
  {l1 : Level} (l2 : Level) (M : Commutative-Monoid l1) →
  is-equiv
    ( normal-submonoid-saturated-congruence-Commutative-Monoid {l2 = l1 ⊔ l2} M)
is-equiv-normal-submonoid-saturated-congruence-Commutative-Monoid l2 M =
  is-equiv-has-inverse
    ( saturated-congruence-Normal-Commutative-Submonoid M)
    ( issec-saturated-congruence-Normal-Commutative-Submonoid l2 M)
    ( isretr-saturated-congruence-Normal-Commutative-Submonoid l2 M)

equiv-normal-submonoid-saturated-congruence-Commutative-Monoid :
  {l1 : Level} (l2 : Level) (M : Commutative-Monoid l1) →
  saturated-congruence-Commutative-Monoid (l1 ⊔ l2) M ≃
  Normal-Commutative-Submonoid (l1 ⊔ l2) M
pr1 (equiv-normal-submonoid-saturated-congruence-Commutative-Monoid l2 M) =
  normal-submonoid-saturated-congruence-Commutative-Monoid M
pr2 (equiv-normal-submonoid-saturated-congruence-Commutative-Monoid l2 M) =
  is-equiv-normal-submonoid-saturated-congruence-Commutative-Monoid l2 M