Show Universal Property
[darcs-mirror-agda-free-groups.git] / GroupHom.agda
1 module GroupHom where
2
3 open import Algebra.Morphism
4 open import Algebra
5 open import Level
6 open import Relation.Binary
7 import Algebra.Props.Group as GroupP
8 import Relation.Binary.EqReasoning as EqR
9 open import Data.Product
10
11 record _-Group→_ {r₁ r₂ r₃ r₄}
12                 (From : Group r₁ r₂) (To : Group r₃ r₄) :
13                 Set (r₁ ⊔ r₂ ⊔ r₃ ⊔ r₄) where
14   private
15     module F = Group From
16     module T = Group To
17   open Definitions F.Carrier T.Carrier T._≈_
18
19   field
20     ⟦_⟧     : Morphism
21     ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
22     ∙-homo  : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
23
24   open EqR T.setoid
25
26   ε-homo :  Homomorphic₀ ⟦_⟧ F.ε T.ε
27   ε-homo = GroupP.left-identity-unique To ⟦ F.ε ⟧ ⟦ F.ε ⟧ (begin
28       T._∙_ ⟦ F.ε ⟧ ⟦ F.ε ⟧ ≈⟨ T.sym (∙-homo _ _) ⟩
29       ⟦ F._∙_ _ _ ⟧         ≈⟨ ⟦⟧-cong (proj₁ F.identity _) ⟩
30       ⟦ F.ε ⟧                ∎)
31
32   ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
33   ⁻¹-homo x = GroupP.left-inverse-unique To ⟦ F._⁻¹ x  ⟧ ⟦ x ⟧ (begin
34     T._∙_ ⟦ F._⁻¹ x ⟧ ⟦ x ⟧
35       ≈⟨ T.sym (∙-homo _ _) ⟩
36     ⟦ F._∙_ (F._⁻¹ x) x ⟧
37       ≈⟨ ⟦⟧-cong (proj₁ F.inverse _) ⟩
38     ⟦ F.ε ⟧
39       ≈⟨ ε-homo ⟩
40     T.ε
41     ∎)