------------------------------------------------------------------------
-- The Agda standard library
--
-- The unique morphism to the terminal object,
-- for each of the relevant categories. Since
-- each terminal algebra builds on `Monoid`,
-- possibly with additional (trivial) operations,
-- satisfying additional properties, it suffices to
-- define the morphism on the underlying `RawMonoid`
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Level using (Level)

module Algebra.Morphism.Construct.Terminal {c ℓ : Level} where

open import Algebra.Bundles.Raw
  using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
open import Algebra.Morphism.Structures

open import Data.Product.Base using (_,_)
open import Function.Definitions using (StrictlySurjective)
import Relation.Binary.Morphism.Definitions as Rel
open import Relation.Binary.Morphism.Structures

open import Algebra.Construct.Terminal {c} {ℓ}

private
  variable
    a ℓa : Level
    A : Set a

------------------------------------------------------------------------
-- The unique morphism

one : A → 𝕆ne.Carrier
one _ = _

------------------------------------------------------------------------
-- Basic properties

strictlySurjective : A → StrictlySurjective 𝕆ne._≈_ one
strictlySurjective x _ = x , _

------------------------------------------------------------------------
-- Homomorphisms

isMagmaHomomorphism : (M : RawMagma a ℓa) →
                      IsMagmaHomomorphism M rawMagma one
isMagmaHomomorphism M = record
  { isRelHomomorphism = record { cong = _ }
  ; homo = _
  }

isMonoidHomomorphism : (M : RawMonoid a ℓa) →
                       IsMonoidHomomorphism M rawMonoid one
isMonoidHomomorphism M = record
  { isMagmaHomomorphism = isMagmaHomomorphism (RawMonoid.rawMagma M)
  ; ε-homo = _
  }

isGroupHomomorphism : (G : RawGroup a ℓa) →
                      IsGroupHomomorphism G rawGroup one
isGroupHomomorphism G = record
  { isMonoidHomomorphism = isMonoidHomomorphism (RawGroup.rawMonoid G)
  ; ⁻¹-homo = λ _ → _
  }

isNearSemiringHomomorphism : (N : RawNearSemiring a ℓa) →
                             IsNearSemiringHomomorphism N rawNearSemiring one
isNearSemiringHomomorphism N = record
  { +-isMonoidHomomorphism = isMonoidHomomorphism (RawNearSemiring.+-rawMonoid N)
  ; *-homo = λ _ _ → _
  }

isSemiringHomomorphism : (S : RawSemiring a ℓa) →
                         IsSemiringHomomorphism S rawSemiring one
isSemiringHomomorphism S = record
  { isNearSemiringHomomorphism = isNearSemiringHomomorphism (RawSemiring.rawNearSemiring S)
  ; 1#-homo = _
  }

isRingHomomorphism : (R : RawRing a ℓa) → IsRingHomomorphism R rawRing one
isRingHomomorphism R = record
  { isSemiringHomomorphism = isSemiringHomomorphism (RawRing.rawSemiring R)
  ; -‿homo = λ _ → _
  }