------------------------------------------------------------------------ -- The Agda standard library -- -- Structures for types of functions ------------------------------------------------------------------------ -- 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 {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 Level using (_⊔_) ------------------------------------------------------------------------ -- One element structures ------------------------------------------------------------------------ record IsCongruent (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field cong : Congruent _≈₁_ _≈₂_ to isEquivalence₁ : IsEquivalence _≈₁_ isEquivalence₂ : IsEquivalence _≈₂_ module Eq₁ where setoid : Setoid a ℓ₁ setoid = record { isEquivalence = isEquivalence₁ } open Setoid setoid public module Eq₂ where setoid : Setoid b ℓ₂ setoid = record { isEquivalence = isEquivalence₂ } open Setoid setoid public record IsInjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isCongruent : IsCongruent to injective : Injective _≈₁_ _≈₂_ to open IsCongruent isCongruent public record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isCongruent : IsCongruent f surjective : Surjective _≈₁_ _≈₂_ f open IsCongruent isCongruent public strictlySurjective : StrictlySurjective _≈₂_ f strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x) record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isInjection : IsInjection f surjective : Surjective _≈₁_ _≈₂_ f open IsInjection isInjection public bijective : Bijective _≈₁_ _≈₂_ f bijective = injective , surjective isSurjection : IsSurjection f isSurjection = record { isCongruent = isCongruent ; surjective = surjective } open IsSurjection isSurjection public using (strictlySurjective) ------------------------------------------------------------------------ -- Two element structures ------------------------------------------------------------------------ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isCongruent : IsCongruent to from-cong : Congruent _≈₂_ _≈₁_ from inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from open IsCongruent isCongruent public renaming (cong to to-cong) strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from strictlyInverseˡ x = inverseˡ Eq₁.refl isSurjection : IsSurjection to isSurjection = record { isCongruent = isCongruent ; surjective = λ y → from y , inverseˡ } record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isCongruent : IsCongruent to from-cong : Congruent _≈₂_ _≈₁_ from inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from open IsCongruent isCongruent public renaming (cong to to-cong) strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from strictlyInverseʳ x = inverseʳ Eq₂.refl record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isLeftInverse : IsLeftInverse to from inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from open IsLeftInverse isLeftInverse public isRightInverse : IsRightInverse to from isRightInverse = record { isCongruent = isCongruent ; from-cong = from-cong ; inverseʳ = inverseʳ } open IsRightInverse isRightInverse public using (strictlyInverseʳ) inverse : Inverseᵇ _≈₁_ _≈₂_ to from inverse = inverseˡ , inverseʳ ------------------------------------------------------------------------ -- Three element structures ------------------------------------------------------------------------ record IsBiEquivalence (to : A → B) (from₁ : B → A) (from₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to-isCongruent : IsCongruent to from₁-cong : Congruent _≈₂_ _≈₁_ from₁ from₂-cong : Congruent _≈₂_ _≈₁_ from₂ open IsCongruent to-isCongruent public renaming (cong to to-cong₁) record IsBiInverse (to : A → B) (from₁ : B → A) (from₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to-isCongruent : IsCongruent to from₁-cong : Congruent _≈₂_ _≈₁_ from₁ from₂-cong : Congruent _≈₂_ _≈₁_ from₂ inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from₁ inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from₂ open IsCongruent to-isCongruent public renaming (cong to to-cong) ------------------------------------------------------------------------ -- Other ------------------------------------------------------------------------ -- See the comment on `SplitSurjection` in `Function.Bundles` for an -- explanation of (split) surjections. record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field from : B → A isLeftInverse : IsLeftInverse f from open IsLeftInverse isLeftInverse public