-
Notifications
You must be signed in to change notification settings - Fork 242
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[ new ] symmetric core of a binary relation (#2071)
* [ new ] symmetric core of a binary relation * [ fix ] name clashes * [ more ] respond to McKinna's comments * [ rename ] fields to lhs≤rhs and rhs≤lhs * [ more ] incorporate parts of McKinna's review * [ minor ] remove implicit argument application from transitive * [ edit ] pull out isEquivalence and do some renaming * [ minor ] respond to easy comments * [ refactor ] remove IsProset, and move Proset to main hierarchy * Eliminate Proset * Fixed CHANGELOG typo --------- Co-authored-by: MatthewDaggitt <[email protected]>
- Loading branch information
1 parent
b601831
commit 6c925fa
Showing
6 changed files
with
102 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,83 @@ | ||
------------------------------------------------------------------------ | ||
-- The Agda standard library | ||
-- | ||
-- Symmetric interior of a binary relation | ||
------------------------------------------------------------------------ | ||
|
||
{-# OPTIONS --cubical-compatible --safe #-} | ||
|
||
module Relation.Binary.Construct.Interior.Symmetric where | ||
|
||
open import Function.Base using (flip) | ||
open import Level | ||
open import Relation.Binary | ||
|
||
private | ||
variable | ||
a b c ℓ r s t : Level | ||
A : Set a | ||
R S T : Rel A r | ||
|
||
------------------------------------------------------------------------ | ||
-- Definition | ||
|
||
record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where | ||
constructor _,_ | ||
field | ||
lhs≤rhs : R x y | ||
rhs≤lhs : R y x | ||
|
||
open SymInterior public | ||
|
||
------------------------------------------------------------------------ | ||
-- Properties | ||
|
||
-- The symmetric interior is symmetric. | ||
symmetric : Symmetric (SymInterior R) | ||
symmetric (r , r′) = r′ , r | ||
|
||
-- The symmetric interior of R is greater than (or equal to) any other symmetric | ||
-- relation contained by R. | ||
unfold : Symmetric S → S ⇒ R → S ⇒ SymInterior R | ||
unfold sym f s = f s , f (sym s) | ||
|
||
-- SymInterior preserves various properties. | ||
reflexive : Reflexive R → Reflexive (SymInterior R) | ||
reflexive refl = refl , refl | ||
|
||
trans : Trans R S T → Trans S R T → | ||
Trans (SymInterior R) (SymInterior S) (SymInterior T) | ||
trans trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′ | ||
|
||
transitive : Transitive R → Transitive (SymInterior R) | ||
transitive tr = trans tr tr | ||
|
||
-- The symmetric interior of a strict relation is empty. | ||
asymmetric⇒empty : Asymmetric R → Empty (SymInterior R) | ||
asymmetric⇒empty asym (r , r′) = asym r r′ | ||
|
||
-- A reflexive transitive relation _≤_ gives rise to a poset in which the | ||
-- equivalence relation is SymInterior _≤_. | ||
|
||
isEquivalence : Reflexive R → Transitive R → IsEquivalence (SymInterior R) | ||
isEquivalence refl trans = record | ||
{ refl = reflexive refl | ||
; sym = symmetric | ||
; trans = transitive trans | ||
} | ||
|
||
isPartialOrder : Reflexive R → Transitive R → IsPartialOrder (SymInterior R) R | ||
isPartialOrder refl trans = record | ||
{ isPreorder = record | ||
{ isEquivalence = isEquivalence refl trans | ||
; reflexive = lhs≤rhs | ||
; trans = trans | ||
} | ||
; antisym = _,_ | ||
} | ||
|
||
poset : ∀ {a} {A : Set a} {R : Rel A ℓ} → Reflexive R → Transitive R → Poset a ℓ ℓ | ||
poset {R = R} refl trans = record | ||
{ _≤_ = R | ||
; isPartialOrder = isPartialOrder refl trans | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters