diff --git a/CHANGELOG.md b/CHANGELOG.md index 51966c2176..d63315374c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -751,8 +751,10 @@ Non-backwards compatible changes - The records in `Function.Structures` and `Function.Bundles` export proofs of these under the names `strictlySurjective`, `strictlyInverseˡ` and `strictlyInverseʳ`, - - Conversion functions have been added in both directions to - `Function.Consequences(.Propositional/Setoid)`. + - Conversion functions for the definitions have been added in both directions + to `Function.Consequences(.Propositional/Setoid)`. + - Conversion functions for structures have been added in + `Function.Structures.Biased`. ### New `Function.Strict` diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index c0c6994e3f..ee6d548fdb 100644 --- a/src/Algebra/Structures/Biased.agda +++ b/src/Algebra/Structures/Biased.agda @@ -2,7 +2,7 @@ -- The Agda standard library -- -- Ways to give instances of certain structures where some fields can --- be given in terms of others +-- be given in terms of others. Re-exported via `Algebra`. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index 04cb6a7097..48fdff0af9 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -185,7 +185,7 @@ module _ where (∀ {x} → A x ↠ B (to I↠J x)) → Σ I A ↠ Σ J B Σ-↠ {I = I} {J = J} {A = A} {B = B} I↠J A↠B = - mk↠ (strictlySurjective⇒surjective strictlySurjective′) + mk↠ₛ strictlySurjective′ where to′ : Σ I A → Σ J B to′ = map (to I↠J) (to A↠B) diff --git a/src/Function.agda b/src/Function.agda index 1d45b05901..b4155ef8ef 100644 --- a/src/Function.agda +++ b/src/Function.agda @@ -13,4 +13,5 @@ open import Function.Base public open import Function.Strict public open import Function.Definitions public open import Function.Structures public +open import Function.Structures.Biased public open import Function.Bundles public diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index 834ee0d4fa..5506f93dd4 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -108,7 +108,7 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {f : A → B} {f⁻¹ : isLeftInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsLeftInverse ≈₂ ≈₁ f⁻¹ f isLeftInverse inv = record { isCongruent = isCongruent F.isCongruent F.from-cong - ; from-cong = F.cong₁ + ; from-cong = F.to-cong ; inverseˡ = inverseˡ ≈₁ ≈₂ F.inverseʳ } where module F = IsRightInverse inv diff --git a/src/Function/Structures.agda b/src/Function/Structures.agda index ae34203fe0..9533cfb179 100644 --- a/src/Function/Structures.agda +++ b/src/Function/Structures.agda @@ -120,7 +120,7 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from open IsCongruent isCongruent public - renaming (cong to cong₁) + renaming (cong to to-cong) strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from strictlyInverseʳ x = inverseʳ Eq₂.refl diff --git a/src/Function/Structures/Biased.agda b/src/Function/Structures/Biased.agda new file mode 100644 index 0000000000..e25c4970c9 --- /dev/null +++ b/src/Function/Structures/Biased.agda @@ -0,0 +1,127 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Ways to give instances of certain structures where some fields can +-- be given in terms of others. +-- The contents of this file should usually be accessed from `Function`. +------------------------------------------------------------------------ + + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) + +module Function.Structures.Biased {a b ℓ₁ ℓ₂} + {A : Set a} (_≈₁_ : Rel A ℓ₁) -- Equality over the domain + {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain + where + +open import Data.Product.Base as Product using (∃; _×_; _,_) +open import Function.Base +open import Function.Definitions +open import Function.Structures _≈₁_ _≈₂_ +open import Function.Consequences.Setoid +open import Level using (_⊔_) + +------------------------------------------------------------------------ +-- Surjection +------------------------------------------------------------------------ + +record IsStrictSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isCongruent : IsCongruent f + strictlySurjective : StrictlySurjective _≈₂_ f + + open IsCongruent isCongruent public + + isSurjection : IsSurjection f + isSurjection = record + { isCongruent = isCongruent + ; surjective = strictlySurjective⇒surjective + Eq₁.setoid Eq₂.setoid cong strictlySurjective + } + +open IsStrictSurjection public + using () renaming (isSurjection to isStrictSurjection) + +------------------------------------------------------------------------ +-- Bijection +------------------------------------------------------------------------ + +record IsStrictBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isInjection : IsInjection f + strictlySurjective : StrictlySurjective _≈₂_ f + + isBijection : IsBijection f + isBijection = record + { isInjection = isInjection + ; surjective = strictlySurjective⇒surjective + Eq₁.setoid Eq₂.setoid cong strictlySurjective + } where open IsInjection isInjection + +open IsStrictBijection public + using () renaming (isBijection to isStrictBijection) + +------------------------------------------------------------------------ +-- Left inverse +------------------------------------------------------------------------ + +record IsStrictLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isCongruent : IsCongruent to + from-cong : Congruent _≈₂_ _≈₁_ from + strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from + + isLeftInverse : IsLeftInverse to from + isLeftInverse = record + { isCongruent = isCongruent + ; from-cong = from-cong + ; inverseˡ = strictlyInverseˡ⇒inverseˡ + Eq₁.setoid Eq₂.setoid cong strictlyInverseˡ + } where open IsCongruent isCongruent + +open IsStrictLeftInverse public + using () renaming (isLeftInverse to isStrictLeftInverse) + +------------------------------------------------------------------------ +-- Right inverse +------------------------------------------------------------------------ + +record IsStrictRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isCongruent : IsCongruent to + from-cong : Congruent _≈₂_ _≈₁_ from + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from + + isRightInverse : IsRightInverse to from + isRightInverse = record + { isCongruent = isCongruent + ; from-cong = from-cong + ; inverseʳ = strictlyInverseʳ⇒inverseʳ + Eq₁.setoid Eq₂.setoid from-cong strictlyInverseʳ + } where open IsCongruent isCongruent + +open IsStrictRightInverse public + using () renaming (isRightInverse to isStrictRightInverse) + +------------------------------------------------------------------------ +-- Inverse +------------------------------------------------------------------------ + +record IsStrictInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isLeftInverse : IsLeftInverse to from + strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from + + isInverse : IsInverse to from + isInverse = record + { isLeftInverse = isLeftInverse + ; inverseʳ = strictlyInverseʳ⇒inverseʳ + Eq₁.setoid Eq₂.setoid from-cong strictlyInverseʳ + } where open IsLeftInverse isLeftInverse + +open IsStrictInverse public + using () renaming (isInverse to isStrictInverse) diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 7ba3825e31..6c2eb19bed 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -135,4 +135,3 @@ isPropositional = Irrelevant Please use Relation.Nullary.Irrelevant instead. " #-} -