learning-agda/MonoidLawTransfer.agda at main · sseefried/learning-agda · 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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
{-# OPTIONS --without-K --safe #-}

module MonoidLawTransfer where

open import Data.Product
open import Level using (Level)

private
  variable
    a b : Level
    A : Set a
    B : Set b

open import Algebra.Core using (Op₂)

record RawMonoid (A : Set) : Set₁ where
   infixr 29 _∙_
   field
      _∙_ : Op₂ A
      ε   : A

open RawMonoid ⦃ … ⦄ public

record MonoidHomomorphism (⟦_⟧ : A → B) (_≈₂_ : B → B → Set)
                          (monoidA : RawMonoid A) (monoidB : RawMonoid B) : Set where
  instance
    _ : RawMonoid A
    _ = monoidA
    _ : RawMonoid B
    _ = monoidB

  field
    ε-homo : ⟦ ε ⟧ ≈₂ ε
    homo : ∀ x y → ⟦ x ∙ y ⟧ ≈₂ ⟦ x ⟧ ∙ ⟦ y ⟧

  open import Algebra.Definitions
  open import Algebra.Structures
  open IsMonoid ⦃ … ⦄ public
  open Level
  open import Relation.Binary

  _≈₁_ : A → A → Set
  a ≈₁ b = ⟦ a ⟧ ≈₂ ⟦ b ⟧

  is-monoid-via-homomorphism : IsMonoid _≈₂_ _∙_ ε → IsMonoid _≈₁_ _∙_ ε
  is-monoid-via-homomorphism is-monoid₂ =
    record
      { isSemigroup =
          record
            { isMagma =
                record
                  { isEquivalence = record { refl = refl; sym = sym; trans = trans }
                  ; ∙-cong = ∙-congruent
                  }
            ; assoc = ∙-assoc
            }
      ; identity = ∙-identityˡ , ∙-identityʳ
      }
    where
      instance
        _ : IsMonoid _≈₂_ _∙_ ε
        _ = is-monoid₂

      open import Relation.Binary.Reasoning.Setoid (setoid)

      ∙-congruent : Congruent₂ _≈₁_ _∙_
      ∙-congruent {x} {y} {u} {v} x≈₁y u≈₁v =
        begin
          ⟦ x ∙ u ⟧
        ≈⟨ homo x u ⟩
          ⟦ x ⟧ ∙ ⟦ u ⟧
        ≈⟨ ∙-cong x≈₁y u≈₁v ⟩
          ⟦ y ⟧ ∙ ⟦ v ⟧
        ≈⟨ sym (homo y v) ⟩
          ⟦ y ∙ v ⟧
        ∎

      ∙-identityˡ : LeftIdentity _≈₁_ ε _∙_
      ∙-identityˡ x =
        begin
          ⟦ ε ∙ x ⟧
        ≈⟨ homo ε x  ⟩
          ⟦ ε ⟧ ∙ ⟦ x ⟧
        ≈⟨ ∙-congʳ ε-homo ⟩
          ε ∙ ⟦ x ⟧
        ≈⟨ identityˡ ⟦ x ⟧ ⟩
          ⟦ x ⟧
        ∎

      ∙-identityʳ : RightIdentity _≈₁_ ε _∙_
      ∙-identityʳ x =
        begin
          ⟦ x ∙ ε ⟧
        ≈⟨ homo x ε ⟩
          ⟦ x ⟧ ∙ ⟦ ε ⟧
        ≈⟨ ∙-congˡ ε-homo ⟩
          ⟦ x ⟧ ∙ ε
        ≈⟨ identityʳ ⟦ x ⟧ ⟩
          ⟦ x ⟧
        ∎

      ∙-assoc : Associative _≈₁_ _∙_
      ∙-assoc x y z =
        begin
          ⟦ (x ∙ y) ∙ z ⟧
        ≈⟨ homo (x ∙ y) z ⟩
          ⟦ x ∙ y ⟧ ∙ ⟦ z ⟧
        ≈⟨ ∙-congʳ (homo x y) ⟩
          (⟦ x ⟧ ∙ ⟦ y ⟧) ∙ ⟦ z ⟧
        ≈⟨ assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
          ⟦ x ⟧ ∙ (⟦ y ⟧ ∙ ⟦ z ⟧)
        ≈⟨ sym  (∙-congˡ (homo y z)) ⟩
          ⟦ x ⟧ ∙ ⟦ y ∙ z ⟧
        ≈⟨ sym (homo x (y ∙ z)) ⟩
          ⟦ x ∙ (y ∙ z) ⟧
        ∎