Skip to content

Commit 9816023

Browse files
MatthewDaggittMatthewDaggitt
authored
Add bundles for morphisms over binary relations (#1464)
1 parent bc9c1b6 commit 9816023

File tree

9 files changed

+340
-90
lines changed

9 files changed

+340
-90
lines changed

‎CHANGELOG.md

Lines changed: 40 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,12 @@ Non-backwards compatible changes
5757
`rectangle`, `rectangleˡ`, `rectangleʳ`, `rectangleᶜ`) have been moved to
5858
`Data.String`.
5959

60+
* The new modules `Relation.Binary.Morphism.(Constant/Identity/Composition)` that
61+
were added in the last release no longer have module-level arguments. This is in order
62+
to allow proofs about newly added morphism bundles to be added to these files. This is
63+
only a breaking change if you were supplying the module arguments upon import, in which
64+
case you will have to change to supplying them upon application of the proofs.
65+
6066
Deprecated modules
6167
------------------
6268

@@ -201,6 +207,11 @@ New modules
201207
Data.Tree.Binary.Show
202208
```
203209

210+
* Bundles for binary relation morphisms
211+
```
212+
Relation.Binary.Morphism.Bundles
213+
```
214+
204215
Other minor additions
205216
---------------------
206217

@@ -938,8 +949,8 @@ Other minor additions
938949

939950
* Added new proofs to `Relation.Binary.Consequences`:
940951
```agda
941-
mono⇒cong : Symmetric _≈_ → _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ → f Preserves _≤_ ⟶ _≤_ → f Preserves _≈_ ⟶ _≈_
942-
antimono⇒cong : Symmetric _≈_ → _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ → f Preserves _≤_ ⟶ (flip _≤_) → f Preserves _≈_ ⟶ _≈_
952+
mono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → f Preserves ≤₁ ⟶ ≤₂ → f Preserves ≈₁ ⟶ ≈₂
953+
antimono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → f Preserves ≈₁ ⟶ ≈₂
943954
```
944955

945956
* Added new proofs to `Relation.Binary.Construct.Converse`:
@@ -948,6 +959,33 @@ Other minor additions
948959
isTotalPreorder : IsTotalPreorder ≈ ∼ → IsTotalPreorder ≈ (flip ∼)
949960
```
950961

962+
963+
* Added new proofs to `Relation.Binary.Morphism.Construct.Constant`:
964+
```agda
965+
setoidHomomorphism : (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) → ∀ x → SetoidHomomorphism S T
966+
preorderHomomorphism : (P : Preorder a ℓ₁ ℓ₂) (Q : Preorder b ℓ₃ ℓ₄) → ∀ x → PreorderHomomorphism P Q
967+
```
968+
969+
* Added new proofs to `Relation.Binary.Morphism.Construct.Composition`:
970+
```agda
971+
setoidHomomorphism : SetoidHomomorphism S T → SetoidHomomorphism T U → SetoidHomomorphism S U
972+
setoidMonomorphism : SetoidMonomorphism S T → SetoidMonomorphism T U → SetoidMonomorphism S U
973+
setoidIsomorphism : SetoidIsomorphism S T → SetoidIsomorphism T U → SetoidIsomorphism S U
974+
975+
preorderHomomorphism : PreorderHomomorphism P Q → PreorderHomomorphism Q R → PreorderHomomorphism P R
976+
posetHomomorphism : PosetHomomorphism P Q → PosetHomomorphism Q R → PosetHomomorphism P R
977+
```
978+
979+
* Added new proofs to `Relation.Binary.Morphism.Construct.Identity`:
980+
```agda
981+
setoidHomomorphism : (S : Setoid a ℓ₁) → SetoidHomomorphism S S
982+
setoidMonomorphism : (S : Setoid a ℓ₁) → SetoidMonomorphism S S
983+
setoidIsomorphism : (S : Setoid a ℓ₁) → SetoidIsomorphism S S
984+
985+
preorderHomomorphism : (P : Preorder a ℓ₁ ℓ₂) → PreorderHomomorphism P P
986+
posetHomomorphism : (P : Poset a ℓ₁ ℓ₂) → PosetHomomorphism P P
987+
```
988+
951989
* Added new proofs to `Relation.Nullary.Negation`:
952990
```agda
953991
contradiction₂ : P ⊎ Q → ¬ P → ¬ Q → Whatever

‎src/Data/Rational/Unnormalised/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -317,10 +317,10 @@ p ≤? q = Dec.map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.*
317317
-- Other properties of _≤_
318318

319319
mono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → f Preserves _≃_ ⟶ _≃_
320-
mono⇒cong = BC.mono⇒cong _ ≃-sym ≤-reflexive ≤-antisym
320+
mono⇒cong = BC.mono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
321321

322322
antimono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → f Preserves _≃_ ⟶ _≃_
323-
antimono⇒cong = BC.antimono⇒cong _ ≃-sym ≤-reflexive ≤-antisym
323+
antimono⇒cong = BC.antimono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
324324

325325
------------------------------------------------------------------------
326326
-- Properties of _≤ᵇ_

‎src/Relation/Binary/Consequences.agda

Lines changed: 15 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,8 @@ open import Relation.Unary using (∁; Pred)
2222

2323
private
2424
variable
25-
a b ℓ ℓ₁ ℓ₂ p : Level
26-
A : Set a
27-
B : Set b
25+
a ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ p : Level
26+
A B : Set a
2827

2928
------------------------------------------------------------------------
3029
-- Substitutive properties
@@ -62,19 +61,19 @@ module _ {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} where
6261
... | inj₁ x≤y = yes x≤y
6362
... | inj₂ y≤x = map′ refl (flip antisym y≤x) (x ≟ y)
6463

65-
mono⇒cong : (_≈_ : Rel A ℓ₁) {_≤_ : Rel A ℓ₂} →
66-
Symmetric _≈_ → _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ →
67-
∀ {f} → f Preserves _≤_ ⟶ _≤_ → f Preserves _≈_ ⟶ _≈_
68-
mono⇒cong _ sym reflexive antisym mono x≈y = antisym
69-
(mono (reflexive x≈y))
70-
(mono (reflexive (sym x≈y)))
71-
72-
antimono⇒cong : (_≈_ : Rel A ℓ₁) {_≤_ : Rel A ℓ₂} →
73-
Symmetric _≈_ → _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ →
74-
∀ {f} → f Preserves _≤_ ⟶ (flip _≤_) → f Preserves _≈_ ⟶ _≈_
75-
antimono⇒cong _ sym reflexive antisym antimono p≈q = antisym
76-
(antimono (reflexive (sym p≈q)))
77-
(antimono (reflexive p≈q))
64+
module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃} {≤₂ : Rel B ℓ₄} where
65+
66+
mono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
67+
∀ {f} → f Preserves ≤₁ ⟶ ≤₂ → f Preserves ≈₁ ⟶ ≈₂
68+
mono⇒cong sym reflexive antisym mono x≈y = antisym
69+
(mono (reflexive x≈y))
70+
(mono (reflexive (sym x≈y)))
71+
72+
antimono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
73+
∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → f Preserves ≈₁ ⟶ ≈₂
74+
antimono⇒cong sym reflexive antisym antimono p≈q = antisym
75+
(antimono (reflexive (sym p≈q)))
76+
(antimono (reflexive p≈q))
7877

7978
------------------------------------------------------------------------
8079
-- Proofs for strict orders

‎src/Relation/Binary/Morphism.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,3 +15,4 @@ module Relation.Binary.Morphism where
1515

1616
open import Relation.Binary.Morphism.Definitions public
1717
open import Relation.Binary.Morphism.Structures public
18+
open import Relation.Binary.Morphism.Bundles public

‎src/Relation/Binary/Morphism/Bundles.agda

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Bundles for morphisms between binary relations
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
open import Level
10+
open import Relation.Binary.Core using (_Preserves_⟶_)
11+
open import Relation.Binary.Bundles
12+
open import Relation.Binary.Morphism.Structures
13+
open import Relation.Binary.Consequences using (mono⇒cong)
14+
15+
module Relation.Binary.Morphism.Bundles where
16+
17+
private
18+
variable
19+
ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level
20+
21+
------------------------------------------------------------------------
22+
-- Setoids
23+
------------------------------------------------------------------------
24+
25+
module _ (S₁ : Setoid ℓ₁ ℓ₂) (S₂ : Setoid ℓ₃ ℓ₄) where
26+
27+
record SetoidHomomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
28+
open Setoid
29+
field
30+
⟦_⟧ : Carrier S₁ → Carrier S₂
31+
isRelHomomorphism : IsRelHomomorphism (_≈_ S₁) (_≈_ S₂) ⟦_⟧
32+
33+
open IsRelHomomorphism isRelHomomorphism public
34+
35+
36+
record SetoidMonomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
37+
open Setoid
38+
field
39+
⟦_⟧ : Carrier S₁ → Carrier S₂
40+
isRelMonomorphism : IsRelMonomorphism (_≈_ S₁) (_≈_ S₂) ⟦_⟧
41+
42+
open IsRelMonomorphism isRelMonomorphism public
43+
44+
homomorphism : SetoidHomomorphism
45+
homomorphism = record { isRelHomomorphism = isHomomorphism }
46+
47+
48+
record SetoidIsomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
49+
open Setoid
50+
field
51+
⟦_⟧ : Carrier S₁ → Carrier S₂
52+
isRelIsomorphism : IsRelIsomorphism (_≈_ S₁) (_≈_ S₂) ⟦_⟧
53+
54+
open IsRelIsomorphism isRelIsomorphism public
55+
56+
monomorphism : SetoidMonomorphism
57+
monomorphism = record { isRelMonomorphism = isMonomorphism }
58+
59+
open SetoidMonomorphism monomorphism public
60+
using (homomorphism)
61+
62+
63+
------------------------------------------------------------------------
64+
-- Preorders
65+
------------------------------------------------------------------------
66+
67+
record PreorderHomomorphism (S₁ : Preorder ℓ₁ ℓ₂ ℓ₃)
68+
(S₂ : Preorder ℓ₄ ℓ₅ ℓ₆)
69+
: Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄ ⊔ ℓ₅ ⊔ ℓ₆) where
70+
open Preorder
71+
field
72+
⟦_⟧ : Carrier S₁ → Carrier S₂
73+
isOrderHomomorphism : IsOrderHomomorphism (_≈_ S₁) (_≈_ S₂) (_∼_ S₁) (_∼_ S₂) ⟦_⟧
74+
75+
open IsOrderHomomorphism isOrderHomomorphism public
76+
77+
------------------------------------------------------------------------
78+
-- Posets
79+
------------------------------------------------------------------------
80+
81+
module _ (P : Poset ℓ₁ ℓ₂ ℓ₃) (Q : Poset ℓ₄ ℓ₅ ℓ₆) where
82+
83+
private
84+
module P = Poset P
85+
module Q = Poset Q
86+
87+
record PosetHomomorphism : Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄ ⊔ ℓ₅ ⊔ ℓ₆) where
88+
field
89+
⟦_⟧ : P.Carrier → Q.Carrier
90+
isOrderHomomorphism : IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ ⟦_⟧
91+
92+
open IsOrderHomomorphism isOrderHomomorphism public
93+
94+
95+
-- Smart constructor that automatically constructs the congruence proof
96+
-- from the monotonicity proof
97+
mkPosetHomo : ∀ f → f Preserves P._≤_ ⟶ Q._≤_ → PosetHomomorphism
98+
mkPosetHomo f mono = record
99+
{ ⟦_⟧ = f
100+
; isOrderHomomorphism = record
101+
{ cong = mono⇒cong P._≈_ Q._≈_ P.Eq.sym P.reflexive Q.antisym mono
102+
; mono = mono
103+
}
104+
}

‎src/Relation/Binary/Morphism/Construct/Composition.agda

Lines changed: 87 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -6,21 +6,26 @@
66

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

9-
open import Data.Product using (_,_)
10-
open import Function.Base using (id; _∘_)
11-
open import Function.Definitions using (Congruent)
9+
open import Function.Base using (_∘_)
1210
open import Function.Construct.Composition using (surjective)
11+
open import Level using (Level)
1312
open import Relation.Binary
13+
open import Relation.Binary.Morphism.Bundles
1414
open import Relation.Binary.Morphism.Structures
1515

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
16+
module Relation.Binary.Morphism.Construct.Composition where
17+
18+
private
19+
variable
20+
a b c ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level
21+
A B C : Set a
22+
≈₁ ≈₂ ≈₃ ∼₁ ∼₂ ∼₃ : Rel A ℓ₁
23+
f g : A → B
2024

2125
------------------------------------------------------------------------
2226
-- Relations
2327
------------------------------------------------------------------------
28+
-- Structures
2429

2530
isRelHomomorphism : IsRelHomomorphism ≈₁ ≈₂ f →
2631
IsRelHomomorphism ≈₂ ≈₃ g →
@@ -41,39 +46,85 @@ isRelIsomorphism : Transitive ≈₃ →
4146
IsRelIsomorphism ≈₁ ≈₂ f →
4247
IsRelIsomorphism ≈₂ ≈₃ g →
4348
IsRelIsomorphism ≈₁ ≈₃ (g ∘ f)
44-
isRelIsomorphism ≈₃-trans m₁ m₂ = record
49+
isRelIsomorphism {≈₁ = ≈₁} ≈₃-trans m₁ m₂ = record
4550
{ isMonomorphism = isRelMonomorphism F.isMonomorphism G.isMonomorphism
46-
; surjective = surjective ≈₁ ≈₂ ≈₃ ≈₃-trans G.cong F.surjective G.surjective
51+
; surjective = surjective ≈₁ _ _ ≈₃-trans G.cong F.surjective G.surjective
4752
} where module F = IsRelIsomorphism m₁; module G = IsRelIsomorphism m₂
4853

54+
------------------------------------------------------------------------
55+
-- Bundles
56+
57+
module _ {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} {U : Setoid c ℓ₃} where
58+
59+
setoidHomomorphism : SetoidHomomorphism S T →
60+
SetoidHomomorphism T U →
61+
SetoidHomomorphism S U
62+
setoidHomomorphism ST TU = record
63+
{ isRelHomomorphism = isRelHomomorphism ST.isRelHomomorphism TU.isRelHomomorphism
64+
} where module ST = SetoidHomomorphism ST; module TU = SetoidHomomorphism TU
65+
66+
setoidMonomorphism : SetoidMonomorphism S T →
67+
SetoidMonomorphism T U →
68+
SetoidMonomorphism S U
69+
setoidMonomorphism ST TU = record
70+
{ isRelMonomorphism = isRelMonomorphism ST.isRelMonomorphism TU.isRelMonomorphism
71+
} where module ST = SetoidMonomorphism ST; module TU = SetoidMonomorphism TU
72+
73+
setoidIsomorphism : SetoidIsomorphism S T →
74+
SetoidIsomorphism T U →
75+
SetoidIsomorphism S U
76+
setoidIsomorphism ST TU = record
77+
{ isRelIsomorphism = isRelIsomorphism (Setoid.trans U) ST.isRelIsomorphism TU.isRelIsomorphism
78+
} where module ST = SetoidIsomorphism ST; module TU = SetoidIsomorphism TU
79+
4980
------------------------------------------------------------------------
5081
-- Orders
5182
------------------------------------------------------------------------
83+
-- Structures
84+
85+
isOrderHomomorphism : IsOrderHomomorphism ≈₁ ≈₂ ∼₁ ∼₂ f →
86+
IsOrderHomomorphism ≈₂ ≈₃ ∼₂ ∼₃ g →
87+
IsOrderHomomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
88+
isOrderHomomorphism m₁ m₂ = record
89+
{ cong = G.cong ∘ F.cong
90+
; mono = G.mono ∘ F.mono
91+
} where module F = IsOrderHomomorphism m₁; module G = IsOrderHomomorphism m₂
92+
93+
isOrderMonomorphism : IsOrderMonomorphism ≈₁ ≈₂ ∼₁ ∼₂ f →
94+
IsOrderMonomorphism ≈₂ ≈₃ ∼₂ ∼₃ g →
95+
IsOrderMonomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
96+
isOrderMonomorphism m₁ m₂ = record
97+
{ isOrderHomomorphism = isOrderHomomorphism F.isOrderHomomorphism G.isOrderHomomorphism
98+
; injective = F.injective ∘ G.injective
99+
; cancel = F.cancel ∘ G.cancel
100+
} where module F = IsOrderMonomorphism m₁; module G = IsOrderMonomorphism m₂
101+
102+
isOrderIsomorphism : Transitive ≈₃ →
103+
IsOrderIsomorphism ≈₁ ≈₂ ∼₁ ∼₂ f →
104+
IsOrderIsomorphism ≈₂ ≈₃ ∼₂ ∼₃ g →
105+
IsOrderIsomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
106+
isOrderIsomorphism {≈₁ = ≈₁} ≈₃-trans m₁ m₂ = record
107+
{ isOrderMonomorphism = isOrderMonomorphism F.isOrderMonomorphism G.isOrderMonomorphism
108+
; surjective = surjective ≈₁ _ _ ≈₃-trans G.cong F.surjective G.surjective
109+
} where module F = IsOrderIsomorphism m₁; module G = IsOrderIsomorphism m₂
110+
111+
------------------------------------------------------------------------
112+
-- Bundles
113+
114+
module _ {P : Preorder a ℓ₁ ℓ₂} {Q : Preorder b ℓ₃ ℓ₄} {R : Preorder c ℓ₅ ℓ₆} where
115+
116+
preorderHomomorphism : PreorderHomomorphism P Q →
117+
PreorderHomomorphism Q R →
118+
PreorderHomomorphism P R
119+
preorderHomomorphism PQ QR = record
120+
{ isOrderHomomorphism = isOrderHomomorphism PQ.isOrderHomomorphism QR.isOrderHomomorphism
121+
} where module PQ = PreorderHomomorphism PQ; module QR = PreorderHomomorphism QR
122+
123+
module _ {P : Poset a ℓ₁ ℓ₂} {Q : Poset b ℓ₃ ℓ₄} {R : Poset c ℓ₅ ℓ₆} where
52124

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₂
125+
posetHomomorphism : PosetHomomorphism P Q →
126+
PosetHomomorphism Q R →
127+
PosetHomomorphism P R
128+
posetHomomorphism PQ QR = record
129+
{ isOrderHomomorphism = isOrderHomomorphism PQ.isOrderHomomorphism QR.isOrderHomomorphism
130+
} where module PQ = PosetHomomorphism PQ; module QR = PosetHomomorphism QR

0 commit comments

Comments
 (0)