Add biased versions of Function structures (#2210)

Author: MatthewDaggitt

CHANGELOG.md

@@ -755,8 +755,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`
 

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 #-}

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)

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

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
 

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

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)

src/Relation/Binary/PropositionalEquality.agda

@@ -135,4 +135,3 @@ isPropositional = Irrelevant
 Please use Relation.Nullary.Irrelevant instead. "
 #-}
 
-