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