Skip to content

Commit cdffecb

Browse files
Add constructions over binary morphisms and deprecated old morphism code (#1328)
1 parent 4e16643 commit cdffecb

File tree

9 files changed

+289
-11
lines changed

9 files changed

+289
-11
lines changed

CHANGELOG.md

Lines changed: 35 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,14 @@ Highlights
99
Bug-fixes
1010
---------
1111

12-
* The example module `Maybe` in `Relation.Binary.Construct.Closure.Reflexive` was accidentally exposed publicly. It has been made private.
12+
* The example module `Maybe` in `Relation.Binary.Construct.Closure.Reflexive` was
13+
accidentally exposed publicly. It has been made private.
1314

14-
* Fixed the type of the proof `map-id` in `List.Relation.Unary.All.Properties`, which was incorrectly abstracted over
15-
unused module parameters.
15+
* Fixed the type of the proof `map-id` in `List.Relation.Unary.All.Properties`,
16+
which was incorrectly abstracted over unused module parameters.
17+
18+
* Fixed bug where `IsRelIsomorphism` in `Relation.Binary.Morphism.Structures` did not
19+
publicly re-export the contents of `IsRelMonomorphism`.
1620

1721
* The binary relation `_≉_` exposed by records in `Relation.Binary.Bundles` now has
1822
the correct infix precedence.
@@ -28,11 +32,31 @@ Non-backwards compatible changes
2832
Deprecated modules
2933
------------------
3034

31-
* The module `TransitiveClosure` in `Induction.WellFounded` has been deprecated. You should instead use the standard definition of transitive closure and the accompanying proof of well-foundness defined in `Relation.Binary.Construct.Closure.Transitive`.
35+
* The module `TransitiveClosure` in `Induction.WellFounded` has been deprecated.
36+
You should instead use the standard definition of transitive closure and the
37+
accompanying proof of well-foundness defined in `Relation.Binary.Construct.Closure.Transitive`.
38+
39+
* The module `Relation.Binary.OrderMorphism` has been deprecated, as the new
40+
`(Homo/Mono/Iso)morphism` infrastructure in `Algebra.Morphism.Structures` is now
41+
complete. The new definitions are parameterised by raw bundles instead of bundles
42+
meaning they are much more flexible to work with.
3243

3344
Deprecated names
3445
----------------
3546

47+
* The immediate contents of `Algebra.Morphism` have been deprecated, as the new
48+
`(Homo/Mono/Iso)morphism` infrastructure in `Algebra.Morphism.Structures` is now
49+
complete. The new definitions are parameterised by raw bundles instead of bundles
50+
meaning they are much more flexible to work with. The replacements are as following:
51+
```agda
52+
IsSemigroupMorphism ↦ IsSemigroupHomomorphism
53+
IsMonoidMorphism ↦ IsMonoidHomomorphism
54+
IsCommutativeMonoidMorphism ↦ IsMonoidHomomorphism
55+
IsIdempotentCommutativeMonoidMorphism ↦ IsMonoidHomomorphism
56+
IsGroupMorphism ↦ IsGroupHomomorphism
57+
IsAbelianGroupMorphism ↦ IsGroupHomomorphism
58+
```
59+
3660
* In `Relation.Binary.Construct.Closure.Reflexive`:
3761
```agda
3862
Refl ↦ ReflClosure
@@ -46,6 +70,13 @@ Deprecated names
4670
New modules
4771
-----------
4872

73+
* Added various generic morphism constructions for binary relations:
74+
```agda
75+
Relation.Binary.Morphism.Construct.Composition
76+
Relation.Binary.Morphism.Construct.Constant
77+
Relation.Binary.Morphism.Construct.Identity
78+
```
79+
4980
* Added `Reflection.Traversal` for generic de Bruijn-aware traversals of reflected terms.
5081
* Added `Reflection.DeBruijn` with weakening, strengthening and free variable operations
5182
on reflected terms.

src/Algebra/Morphism.agda

Lines changed: 35 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@
99
module Algebra.Morphism where
1010

1111
import Algebra.Morphism.Definitions as MorphismDefinitions
12-
open import Relation.Binary
1312
open import Algebra
1413
import Algebra.Properties.Group as GroupP
1514
open import Function hiding (Morphism)
1615
open import Level
16+
open import Relation.Binary
1717
import Relation.Binary.Reasoning.Setoid as EqR
1818

1919
private
@@ -23,15 +23,22 @@ private
2323
B : Set b
2424

2525
------------------------------------------------------------------------
26-
--
26+
-- Re-export
2727

2828
module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) where
2929
open MorphismDefinitions A B _≈_ public
3030

3131
open import Algebra.Morphism.Structures public
3232

33+
3334
------------------------------------------------------------------------
34-
-- Bundle homomorphisms
35+
-- DEPRECATED
36+
------------------------------------------------------------------------
37+
-- Please use the new definitions re-exported from
38+
-- `Algebra.Morphism.Structures` as continuing support for the below is
39+
-- no guaranteed.
40+
41+
-- Version 1.5
3542

3643
module _ {c₁ ℓ₁ c₂ ℓ₂}
3744
(From : Semigroup c₁ ℓ₁)
@@ -175,3 +182,28 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
175182

176183
IsRingMorphism-syntax = IsRingMorphism
177184
syntax IsRingMorphism-syntax From To F = F Is From -Ring⟶ To
185+
186+
{-# WARNING_ON_USAGE IsSemigroupMorphism
187+
"Warning: IsSemigroupMorphism was deprecated in v1.5.
188+
Please use IsSemigroupHomomorphism instead."
189+
#-}
190+
{-# WARNING_ON_USAGE IsMonoidMorphism
191+
"Warning: IsMonoidMorphism was deprecated in v1.5.
192+
Please use IsMonoidHomomorphism instead."
193+
#-}
194+
{-# WARNING_ON_USAGE IsCommutativeMonoidMorphism
195+
"Warning: IsCommutativeMonoidMorphism was deprecated in v1.5.
196+
Please use IsMonoidHomomorphism instead."
197+
#-}
198+
{-# WARNING_ON_USAGE IsIdempotentCommutativeMonoidMorphism
199+
"Warning: IsIdempotentCommutativeMonoidMorphism was deprecated in v1.5.
200+
Please use IsMonoidHomomorphism instead."
201+
#-}
202+
{-# WARNING_ON_USAGE IsGroupMorphism
203+
"Warning: IsGroupMorphism was deprecated in v1.5.
204+
Please use IsGroupHomomorphism instead."
205+
#-}
206+
{-# WARNING_ON_USAGE IsAbelianGroupMorphism
207+
"Warning: IsAbelianGroupMorphism was deprecated in v1.5.
208+
Please use IsGroupHomomorphism instead."
209+
#-}

src/Function/Endomorphism/Propositional.agda

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@
66

77
{-# OPTIONS --without-K --safe #-}
88

9+
-- Disabled to prevent warnings from deprecated names
10+
{-# OPTIONS --warn=noUserWarning #-}
11+
912
module Function.Endomorphism.Propositional {a} (A : Set a) where
1013

1114
open import Algebra

src/Function/Endomorphism/Setoid.agda

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@
66

77
{-# OPTIONS --without-K --safe #-}
88

9+
-- Disabled to prevent warnings from deprecated names
10+
{-# OPTIONS --warn=noUserWarning #-}
11+
912
open import Relation.Binary
1013

1114
module Function.Endomorphism.Setoid {c e} (S : Setoid c e) where
Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- The composition of morphisms between binary relations
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Data.Product using (_,_)
10+
open import Function.Base using (id; _∘_)
11+
open import Function.Definitions using (Congruent)
12+
open import Function.Construct.Composition using (surjective)
13+
open import Relation.Binary
14+
open import Relation.Binary.Morphism.Structures
15+
16+
module Relation.Binary.Morphism.Construct.Composition
17+
{a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
18+
{≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
19+
{f : A B} {g : B C} where
20+
21+
------------------------------------------------------------------------
22+
-- Relations
23+
------------------------------------------------------------------------
24+
25+
isRelHomomorphism : IsRelHomomorphism ≈₁ ≈₂ f
26+
IsRelHomomorphism ≈₂ ≈₃ g
27+
IsRelHomomorphism ≈₁ ≈₃ (g ∘ f)
28+
isRelHomomorphism m₁ m₂ = record
29+
{ cong = G.cong ∘ F.cong
30+
} where module F = IsRelHomomorphism m₁; module G = IsRelHomomorphism m₂
31+
32+
isRelMonomorphism : IsRelMonomorphism ≈₁ ≈₂ f
33+
IsRelMonomorphism ≈₂ ≈₃ g
34+
IsRelMonomorphism ≈₁ ≈₃ (g ∘ f)
35+
isRelMonomorphism m₁ m₂ = record
36+
{ isHomomorphism = isRelHomomorphism F.isHomomorphism G.isHomomorphism
37+
; injective = F.injective ∘ G.injective
38+
} where module F = IsRelMonomorphism m₁; module G = IsRelMonomorphism m₂
39+
40+
isRelIsomorphism : Transitive ≈₃
41+
IsRelIsomorphism ≈₁ ≈₂ f
42+
IsRelIsomorphism ≈₂ ≈₃ g
43+
IsRelIsomorphism ≈₁ ≈₃ (g ∘ f)
44+
isRelIsomorphism ≈₃-trans m₁ m₂ = record
45+
{ isMonomorphism = isRelMonomorphism F.isMonomorphism G.isMonomorphism
46+
; surjective = surjective ≈₁ ≈₂ ≈₃ ≈₃-trans G.cong F.surjective G.surjective
47+
} where module F = IsRelIsomorphism m₁; module G = IsRelIsomorphism m₂
48+
49+
------------------------------------------------------------------------
50+
-- Orders
51+
------------------------------------------------------------------------
52+
53+
module _ {ℓ₄ ℓ₅ ℓ₆} {∼₁ : Rel A ℓ₄} {∼₂ : Rel B ℓ₅} {∼₃ : Rel C ℓ₆} where
54+
55+
isOrderHomomorphism : IsOrderHomomorphism ≈₁ ≈₂ ∼₁ ∼₂ f
56+
IsOrderHomomorphism ≈₂ ≈₃ ∼₂ ∼₃ g
57+
IsOrderHomomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
58+
isOrderHomomorphism m₁ m₂ = record
59+
{ cong = G.cong ∘ F.cong
60+
; mono = G.mono ∘ F.mono
61+
} where module F = IsOrderHomomorphism m₁; module G = IsOrderHomomorphism m₂
62+
63+
isOrderMonomorphism : IsOrderMonomorphism ≈₁ ≈₂ ∼₁ ∼₂ f
64+
IsOrderMonomorphism ≈₂ ≈₃ ∼₂ ∼₃ g
65+
IsOrderMonomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
66+
isOrderMonomorphism m₁ m₂ = record
67+
{ isOrderHomomorphism = isOrderHomomorphism F.isOrderHomomorphism G.isOrderHomomorphism
68+
; injective = F.injective ∘ G.injective
69+
; cancel = F.cancel ∘ G.cancel
70+
} where module F = IsOrderMonomorphism m₁; module G = IsOrderMonomorphism m₂
71+
72+
isOrderIsomorphism : Transitive ≈₃
73+
IsOrderIsomorphism ≈₁ ≈₂ ∼₁ ∼₂ f
74+
IsOrderIsomorphism ≈₂ ≈₃ ∼₂ ∼₃ g
75+
IsOrderIsomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
76+
isOrderIsomorphism ≈₃-trans m₁ m₂ = record
77+
{ isOrderMonomorphism = isOrderMonomorphism F.isOrderMonomorphism G.isOrderMonomorphism
78+
; surjective = surjective ≈₁ ≈₂ ≈₃ ≈₃-trans G.cong F.surjective G.surjective
79+
} where module F = IsOrderIsomorphism m₁; module G = IsOrderIsomorphism m₂
Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Constant morphisms between binary relations
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Data.Product using (_,_)
10+
open import Function.Base using (const; _∘_)
11+
open import Function.Definitions using (Congruent)
12+
open import Function.Construct.Composition using (surjective)
13+
open import Relation.Binary
14+
open import Relation.Binary.Morphism.Structures
15+
16+
module Relation.Binary.Morphism.Construct.Constant
17+
{a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
18+
(≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈-refl : Reflexive ≈₂)
19+
where
20+
21+
------------------------------------------------------------------------
22+
-- Relations
23+
------------------------------------------------------------------------
24+
25+
isRelHomomorphism : x IsRelHomomorphism ≈₁ ≈₂ (const x)
26+
isRelHomomorphism x = record
27+
{ cong = const ≈-refl
28+
}
29+
30+
------------------------------------------------------------------------
31+
-- Orders
32+
------------------------------------------------------------------------
33+
34+
module _ {ℓ₃ ℓ₄} (∼₁ : Rel A ℓ₃) (∼₂ : Rel B ℓ₄) where
35+
36+
isOrderHomomorphism : Reflexive ∼₂
37+
x IsOrderHomomorphism ≈₁ ≈₂ ∼₁ ∼₂ (const x)
38+
isOrderHomomorphism ∼-refl x = record
39+
{ cong = const ≈-refl
40+
; mono = const ∼-refl
41+
}
Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- The identity morphism for binary relations
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Data.Product using (_,_)
10+
open import Function.Base using (id)
11+
open import Relation.Binary
12+
open import Relation.Binary.Morphism.Structures
13+
14+
module Relation.Binary.Morphism.Construct.Identity
15+
{a ℓ} {A : Set a} (≈ : Rel A ℓ) where
16+
17+
------------------------------------------------------------------------
18+
-- Relations
19+
------------------------------------------------------------------------
20+
21+
isRelHomomorphism : IsRelHomomorphism ≈ ≈ id
22+
isRelHomomorphism = record
23+
{ cong = id
24+
}
25+
26+
isRelMonomorphism : IsRelMonomorphism ≈ ≈ id
27+
isRelMonomorphism = record
28+
{ isHomomorphism = isRelHomomorphism
29+
; injective = id
30+
}
31+
32+
isRelIsomorphism : Reflexive ≈ IsRelIsomorphism ≈ ≈ id
33+
isRelIsomorphism refl = record
34+
{ isMonomorphism = isRelMonomorphism
35+
; surjective = λ y y , refl
36+
}
37+
38+
------------------------------------------------------------------------
39+
-- Orders
40+
------------------------------------------------------------------------
41+
42+
module _ {ℓ₂} (∼ : Rel A ℓ₂) where
43+
44+
isOrderHomomorphism : IsOrderHomomorphism ≈ ≈ ∼ ∼ id
45+
isOrderHomomorphism = record
46+
{ cong = id
47+
; mono = id
48+
}
49+
50+
isOrderMonomorphism : IsOrderMonomorphism ≈ ≈ ∼ ∼ id
51+
isOrderMonomorphism = record
52+
{ isOrderHomomorphism = isOrderHomomorphism
53+
; injective = id
54+
; cancel = id
55+
}
56+
57+
isOrderIsomorphism : Reflexive ≈ IsOrderIsomorphism ≈ ≈ ∼ ∼ id
58+
isOrderIsomorphism refl = record
59+
{ isOrderMonomorphism = isOrderMonomorphism
60+
; surjective = λ y y , refl
61+
}

src/Relation/Binary/Morphism/Structures.agda

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ private
2222
ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
2323

2424
------------------------------------------------------------------------
25-
-- Raw relations
25+
-- Relations
2626
------------------------------------------------------------------------
2727

2828
record IsRelHomomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
@@ -46,14 +46,14 @@ record IsRelIsomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
4646
isMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧
4747
surjective : Surjective _∼₁_ _∼₂_ ⟦_⟧
4848

49-
open IsRelMonomorphism isMonomorphism
49+
open IsRelMonomorphism isMonomorphism public
5050

5151
bijective : Bijective _∼₁_ _∼₂_ ⟦_⟧
5252
bijective = injective , surjective
5353

5454

5555
------------------------------------------------------------------------
56-
-- Raw orders
56+
-- Orders
5757
------------------------------------------------------------------------
5858

5959
record IsOrderHomomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)

0 commit comments

Comments
 (0)