------------------------------------------------------------------------
-- 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)