agda-stdlib/src/Algebra/Morphism/Construct/Terminal.agda at 337b722ba5b03c0450f51d1761d037ed5b05433b · agda/agda-stdlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
------------------------------------------------------------------------
-- 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
  using(IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism
        ; IsNearSemiringHomomorphism; IsSemiringHomomorphism
        ; IsRingHomomorphism)
open import Data.Product.Base using (_,_)
open import Function.Definitions using (StrictlySurjective)

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 = λ _ → _
  }