Mercurial > hg > Members > kono > Proof > category

annotate src/Category/Ring.agda @ 1115:5620d4a85069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe rewriting nearly finished
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Jul 2024 11:44:58 +0900
parents 45de2b31bf02
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
1110
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
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
6 open import Algebra.Morphism
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
7 import Relation.Binary.Reasoning.Setoid as EqR
1110
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
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
16
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
17 -- open import Algebra.Morphism.Definitions
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
18
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
19 record _-Ring⟶_ {c ℓ c' ℓ' : Level } (From : RingObj {c} {ℓ}) (To : RingObj {c'} {ℓ'}) : Set ((c ⊔ ℓ ⊔ c' ⊔ ℓ')) where
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
20 module F = Ring From
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
21 module T = Ring To
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
22 open Definitions (F.Carrier) (T.Carrier) T._≈_
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
23 field
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
24 ⟦_⟧ : Ring.Carrier From → Ring.Carrier To
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
25 ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
26 +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
27 *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
28 1-homo : Homomorphic₀ ⟦_⟧ F.1# T.1#
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
29
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
30 infixr 5 _-Ring⟶_
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
31
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 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
33 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
34
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 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
36 RingId {R = R} = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; +-homo = +-homo
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
37 ; *-homo = *-homo ; 1-homo = 1-homo
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
38 }
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 open Algebra.Ring R
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 open Definitions Carrier Carrier _≈_
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1110
diff changeset
42 ⟦_⟧ : Carrier → Carrier
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 ⟦_⟧ = λ x → x
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 ⟦⟧-cong : ⟦_⟧ Preserves _≈_ ⟶ _≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 ⟦⟧-cong = λ x → x
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 +-homo : Homomorphic₂ ⟦_⟧ _+_ _+_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 +-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
48 *-homo : Homomorphic₂ ⟦_⟧ _*_ _*_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 *-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
50 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
51 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
52
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 [_]_ : ∀{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
54 [ 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
55
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 _∘_ : ∀{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
57 → 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
58 _∘_ {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
59 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
60 ; *-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
61 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 module F = Ring R₁
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 module M = Ring R₂
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 module T = Ring R₃
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 module homo = _-Ring⟶_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 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
68 ⟦_⟧ : Morphism
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 ⟦ x ⟧ = [ g ] ([ f ] x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ⟦⟧-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
72 +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 +-homo x y =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 ⟦ 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
76 [ 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
77 T._+_ ⟦ x ⟧ ⟦ y ⟧
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 ∎
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 open EqR T.setoid
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 *-homo x y =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 ⟦ 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
86 [ 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
87 T._*_ ⟦ x ⟧ ⟦ y ⟧
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 ∎
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 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 open EqR T.setoid
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 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
93 1-homo =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ⟦ 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
96 [ 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
97 T.1#
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 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 open EqR T.setoid
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 _≈_ : ∀{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
104 _≈_ {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
105 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 module F = Ring R₁
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 module T = Ring R₂
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 ≈-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
110 ≈-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
111
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 ≈-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
113 ≈-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
114
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 ≈-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
116 → 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
117 ≈-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
118
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 ≈-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
120 → 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
121 ≈-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
122 ; 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
123 ; 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
124 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 RingCat : ∀{c ℓ} → Category _ _ _
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 RingCat {c} {ℓ} =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 record { Obj = Ring c ℓ
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 ; Hom = _-Ring⟶_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 ; Id = RingId
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 ; _o_ = _∘_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 ; _≈_ = _≈_
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 ; isCategory = isCategory
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 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
138 isCategory =
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 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
140 ; 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
141 ; 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
142 ; 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
143 ; 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
144 }
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 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
147 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
148 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
149 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
150 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
151 → 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
152 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
153 begin
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 ([ 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
155 ([ 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
156 ([ i ∘ g ] x)
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 ∎
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 where
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 module T = Ring R₃
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 open IsEquivalence T.isEquivalence
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 open EqR T.setoid
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 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
163 → (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
164 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
165
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166