Mercurial > hg > Members > kono > Proof > category

annotate src/Category/Ring.agda @ 1110:45de2b31bf02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add original library and fix for safe mode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 07 Oct 2023 19:43:31 +0900
parents
children 5620d4a85069
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 {-# OPTIONS --universe-polymorphism #-}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 module Category.Ring where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Algebra
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Algebra.Structures
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Algebra.Morphism
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 import Relation.Binary.EqReasoning as EqR
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Relation.Binary.Core
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Level
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Product
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 RingObj : ∀{c ℓ} → Set (suc (c ⊔ ℓ))
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 RingObj {c} {ℓ} = Ring c ℓ
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 RingHom : ∀{c ℓ} → Set (suc (c ⊔ ℓ))
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 RingHom {c} {ℓ} = {R₁ R₂ : Ring c ℓ} → R₁ -Ring⟶ R₂
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 RingId : ∀{c ℓ} {R : Ring c ℓ} → R -Ring⟶ R
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 RingId {R = R} = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; +-homo = +-homo
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 ; *-homo = *-homo ; 1-homo = 1-homo
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 open Algebra.Ring R
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 open Definitions Carrier Carrier _≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 ⟦_⟧ : Morphism
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 ⟦_⟧ = λ x → x
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 ⟦⟧-cong : ⟦_⟧ Preserves _≈_ ⟶ _≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 ⟦⟧-cong = λ x → x
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 +-homo : Homomorphic₂ ⟦_⟧ _+_ _+_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 +-homo x y = IsEquivalence.refl isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 *-homo : Homomorphic₂ ⟦_⟧ _*_ _*_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 *-homo x y = IsEquivalence.refl isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 1-homo : Homomorphic₀ ⟦_⟧ 1# 1#
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 1-homo = IsEquivalence.refl isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 [_]_ : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} → R₁ -Ring⟶ R₂ → Ring.Carrier R₁ → Ring.Carrier R₂
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 [ f ] x = _-Ring⟶_.⟦_⟧ f x
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 _∘_ : ∀{c₁ ℓ₁ c₂ ℓ₂ c₃ ℓ₃} {R₁ : Ring c₁ ℓ₁} {R₂ : Ring c₂ ℓ₂} {R₃ : Ring c₃ ℓ₃}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 → R₂ -Ring⟶ R₃ → R₁ -Ring⟶ R₂ → R₁ -Ring⟶ R₃
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 _∘_ {R₁ = R₁} {R₂} {R₃} g f =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; +-homo = +-homo
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 ; *-homo = *-homo ; 1-homo = 1-homo
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 module F = Ring R₁
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 module M = Ring R₂
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 module T = Ring R₃
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 module homo = _-Ring⟶_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 open Definitions F.Carrier T.Carrier T._≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 ⟦_⟧ : Morphism
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 ⟦ x ⟧ = [ g ] ([ f ] x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 ⟦⟧-cong x = homo.⟦⟧-cong g (homo.⟦⟧-cong f x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 +-homo x y =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 ⟦ F._+_ x y ⟧ ≈⟨ homo.⟦⟧-cong g (homo.+-homo f x y) ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 [ g ] ( M._+_ ([ f ] x) ([ f ] y) ) ≈⟨ homo.+-homo g ([ f ] x) ([ f ] y) ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 T._+_ ⟦ x ⟧ ⟦ y ⟧
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 ∎
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 open EqR T.setoid
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 *-homo x y =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 ⟦ F._*_ x y ⟧ ≈⟨ homo.⟦⟧-cong g (homo.*-homo f x y) ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 [ g ] ( M._*_ ([ f ] x) ([ f ] y) ) ≈⟨ homo.*-homo g ([ f ] x) ([ f ] y) ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 T._*_ ⟦ x ⟧ ⟦ y ⟧
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 ∎
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 open EqR T.setoid
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 1-homo : Homomorphic₀ ⟦_⟧ F.1# T.1#
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 1-homo =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 ⟦ F.1# ⟧ ≈⟨ homo.⟦⟧-cong g (homo.1-homo f) ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 [ g ] M.1# ≈⟨ homo.1-homo g ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 T.1#
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 ∎
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 open EqR T.setoid
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 _≈_ : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} → Rel (R₁ -Ring⟶ R₂) (ℓ′ ⊔ c)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 _≈_ {R₁ = R₁} {R₂} φ ψ = ∀(x : F.Carrier) → T._≈_ ([ φ ] x) ([ ψ ] x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 module F = Ring R₁
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 module T = Ring R₂
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 ≈-refl : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} {F : R₁ -Ring⟶ R₂} → F ≈ F
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 ≈-refl {R₁ = R₁} {F = F} _ = _-Ring⟶_.⟦⟧-cong F (IsEquivalence.refl (Ring.isEquivalence R₁))
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 ≈-sym : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} {F G : R₁ -Ring⟶ R₂} → F ≈ G → G ≈ F
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 ≈-sym {R₁ = R₁} {R₂} {F} {G} F≈G x = IsEquivalence.sym (Ring.isEquivalence R₂)(F≈G x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 ≈-trans : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′} {F G H : R₁ -Ring⟶ R₂}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 → F ≈ G → G ≈ H → F ≈ H
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 ≈-trans {R₁ = R₁} {R₂} {F} {G} F≈G G≈H x = IsEquivalence.trans (Ring.isEquivalence R₂) (F≈G x) (G≈H x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 ≈-isEquivalence : ∀{c ℓ c′ ℓ′} {R₁ : Ring c ℓ} {R₂ : Ring c′ ℓ′}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 → IsEquivalence {A = R₁ -Ring⟶ R₂} _≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 ≈-isEquivalence {R₁ = R₁} {R₂} = record { refl = λ {F} → ≈-refl {R₁ = R₁} {R₂} {F}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ; sym = λ{F} {G} → ≈-sym {R₁ = R₁} {R₂} {F} {G}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 ; trans = λ{F} {G} {H} → ≈-trans {R₁ = R₁} {R₂} {F} {G} {H}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 RingCat : ∀{c ℓ} → Category _ _ _
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 RingCat {c} {ℓ} =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 record { Obj = Ring c ℓ
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 ; Hom = _-Ring⟶_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 ; Id = RingId
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 ; _o_ = _∘_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 ; _≈_ = _≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 ; isCategory = isCategory
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 isCategory : IsCategory (Ring c ℓ) _-Ring⟶_ _≈_ _∘_ RingId
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 isCategory =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 record { isEquivalence = ≈-isEquivalence {c} {ℓ} {c} {ℓ}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 ; identityL = λ {R₁ R₂ f} → identityL {R₁} {R₂} {f}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 ; identityR = λ {R₁ R₂ f} → identityR {R₁} {R₂} {f}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 ; o-resp-≈ = λ {A} {B} {C} {f} {g} {h} {i} → o-resp-≈ {A} {B} {C} {f} {g} {h} {i}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 ; associative = λ {R₁} {R₂} {R₃} {R₄} {f} {g} {h} → associative {R₁} {R₂} {R₃} {R₄} {f} {g} {h}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 identityL : {R₁ R₂ : Ring c ℓ} {f : R₁ -Ring⟶ R₂} → (RingId ∘ f) ≈ f
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 identityL {f = f} = ≈-refl {F = f}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 identityR : {R₁ R₂ : Ring c ℓ} {f : R₁ -Ring⟶ R₂} → (f ∘ RingId) ≈ f
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 identityR {f = f} = ≈-refl {F = f}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 o-resp-≈ : {R₁ R₂ R₃ : Ring c ℓ} {f g : R₁ -Ring⟶ R₂} {h i : R₂ -Ring⟶ R₃}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 → f ≈ g → h ≈ i → (h ∘ f) ≈ (i ∘ g)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 o-resp-≈ {R₃ = R₃} {f} {g} {h} {i} f≈g h≈i x =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 ([ h ∘ f ] x) ≈⟨ h≈i ([ f ] x) ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 ([ i ∘ f ] x) ≈⟨ _-Ring⟶_.⟦⟧-cong i (f≈g x) ⟩
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 ([ i ∘ g ] x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 ∎
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 module T = Ring R₃
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 open EqR T.setoid
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 associative : {R₁ R₂ R₃ R₄ : Ring c ℓ} {f : R₃ -Ring⟶ R₄} {g : R₂ -Ring⟶ R₃} {h : R₁ -Ring⟶ R₂}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 → (f ∘ (g ∘ h)) ≈ ((f ∘ g) ∘ h)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 associative {f = f} {g} {h} = ≈-refl {F = f ∘ (g ∘ h)}
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150