[ new ] symmetric core of a binary relation

CHANGELOG.md

@@ -51,6 +51,13 @@ New modules
  Relation.Binary.Construct.Interior.Symmetric
  ```
 
+* `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
+
+* Nagata's construction of the "idealization of a module":
+ ```agda
+ Algebra.Module.Construct.Idealization
+ ```
+
 Additions to existing modules
 -----------------------------
 
@@ -166,7 +173,42 @@ Additions to existing modules
  map : (Char → Char) → String → String
  ```
 
-* Added new definitions in `Relation.Binary.Definitions`:
+* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
+ be used infix.
+
+* Added new definitions in `Relation.Binary.Definitions`
+ ```
+ Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
+ Empty _∼_ = ∀ {x y} → x ∼ y → ⊥
+ ```
+
+* Added new definitions in `Relation.Nullary`
+ ```
+ Recomputable : Set _
+ WeaklyDecidable : Set _
+ ```
+
+* Added new definitions in `Relation.Unary`
+ ```
+ Stable : Pred A ℓ → Set _
+ WeaklyDecidable : Pred A ℓ → Set _
+ ```
+
+* Added new proof in `Relation.Nullary.Decidable`:
+ ```agda
+ ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+ ```
+
+* Added module `Data.Vec.Functional.Relation.Binary.Permutation`:
+ ```agda
+ _↭_ : IRel (Vector A) _
+ ```
+
+* Added new file `Data.Vec.Functional.Relation.Binary.Permutation.Properties`:
  ```agda
- Empty _∼_ = ∀ {x y} → x ∼ y → ⊥
+ ↭-refl : Reflexive (Vector A) _↭_
+ ↭-reflexive : xs ≡ ys → xs ↭ ys
+ ↭-sym : Symmetric (Vector A) _↭_
+ ↭-trans : Transitive (Vector A) _↭_
+>>>>>>> master
  ```

src/Relation/Binary/Bundles.agda

@@ -76,15 +76,6 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
 -- Preorders
 ------------------------------------------------------------------------
 
-record Proset c ℓ : Set (suc (c ⊔ ℓ)) where
- infix 4 _≤_
- field
- Carrier : Set c
- _≤_ : Rel Carrier ℓ
- refl : Reflexive _≤_
- trans : Transitive _≤_
-
-
 record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≲_
  field

src/Relation/Binary/Construct/Interior/Symmetric.agda

@@ -16,9 +16,7 @@ private
  variable
  a b c ℓ r s t : Level
  A : Set a
- R : Rel A r
- S : Rel A s
- T : Rel A t
+ R S T : Rel A r
 
 ------------------------------------------------------------------------
 -- Definition
@@ -28,6 +26,7 @@ record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where
  field
  lhs≤rhs : R x y
  rhs≤lhs : R y x
+
 open SymInterior public
 
 ------------------------------------------------------------------------
@@ -60,25 +59,25 @@ 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 : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} →
- Reflexive ≤ → Transitive ≤ → IsEquivalence (SymInterior ≤)
-isEquivalence ≤-refl ≤-trans = record
- { refl = reflexive ≤-refl
+isEquivalence : Reflexive R → Transitive R → IsEquivalence (SymInterior R)
+isEquivalence refl trans = record
+ { refl = reflexive refl
  ; sym = symmetric
- ; trans = transitive ≤-trans
+ ; trans = transitive trans
  }
 
-isPartialOrder : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} →
- Reflexive ≤ → Transitive ≤ → IsPartialOrder (SymInterior ≤) ≤
-isPartialOrder ≤-refl ≤-trans = record
+isPartialOrder : Reflexive R → Transitive R → IsPartialOrder (SymInterior R) R
+isPartialOrder refl trans = record
  { isPreorder = record
- { isEquivalence = isEquivalence ≤-refl ≤-trans
+ { isEquivalence = isEquivalence refl trans
  ; reflexive = lhs≤rhs
- ; trans = ≤-trans
+ ; trans = trans
  }
  ; antisym = _,_
  }
 
-poset : Proset c ℓ → Poset c ℓ ℓ
-poset record { _≤_ = ≤; refl = refl; trans = trans } =
- record { _≤_ = ≤; isPartialOrder = isPartialOrder refl trans }
+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
+ }