------------------------------------------------------------------------ -- The Agda standard library -- -- Structures for types of functions ------------------------------------------------------------------------ -- The contents of this file should usually be accessed from `Function`. {-# OPTIONS --without-K --safe #-} open import Relation.Binary 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 using (; _×_; _,_) open import Function.Base open import Function.Definitions open import Level using (_⊔_) ------------------------------------------------------------------------ -- One element structures ------------------------------------------------------------------------ record IsCongruent (f : A B) : Set (a b ℓ₁ ℓ₂) where field cong : Congruent _≈₁_ _≈₂_ f 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 (f : A B) : Set (a b ℓ₁ ℓ₂) where field isCongruent : IsCongruent f injective : Injective _≈₁_ _≈₂_ f open IsCongruent isCongruent public record IsSurjection (f : A B) : Set (a b ℓ₁ ℓ₂) where field isCongruent : IsCongruent f surjective : Surjective _≈₁_ _≈₂_ f open IsCongruent isCongruent public 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 } ------------------------------------------------------------------------ -- Two element structures ------------------------------------------------------------------------ record IsLeftInverse (f : A B) (g : B A) : Set (a b ℓ₁ ℓ₂) where field isCongruent : IsCongruent f cong₂ : Congruent _≈₂_ _≈₁_ g inverseˡ : Inverseˡ _≈₁_ _≈₂_ f g open IsCongruent isCongruent public renaming (cong to cong₁) record IsRightInverse (f : A B) (g : B A) : Set (a b ℓ₁ ℓ₂) where field isCongruent : IsCongruent f cong₂ : Congruent _≈₂_ _≈₁_ g inverseʳ : Inverseʳ _≈₁_ _≈₂_ f g open IsCongruent isCongruent public renaming (cong to cong₁) record IsInverse (f : A B) (g : B A) : Set (a b ℓ₁ ℓ₂) where field isLeftInverse : IsLeftInverse f g inverseʳ : Inverseʳ _≈₁_ _≈₂_ f g open IsLeftInverse isLeftInverse public isRightInverse : IsRightInverse f g isRightInverse = record { isCongruent = isCongruent ; cong₂ = cong₂ ; inverseʳ = inverseʳ } inverse : Inverseᵇ _≈₁_ _≈₂_ f g inverse = inverseˡ , inverseʳ ------------------------------------------------------------------------ -- Three element structures ------------------------------------------------------------------------ record IsBiEquivalence (f : A B) (g₁ : B A) (g₂ : B A) : Set (a b ℓ₁ ℓ₂) where field f-isCongruent : IsCongruent f cong₂ : Congruent _≈₂_ _≈₁_ g₁ cong₃ : Congruent _≈₂_ _≈₁_ g₂ open IsCongruent f-isCongruent public renaming (cong to cong₁) record IsBiInverse (f : A B) (g₁ : B A) (g₂ : B A) : Set (a b ℓ₁ ℓ₂) where field f-isCongruent : IsCongruent f cong₂ : Congruent _≈₂_ _≈₁_ g₁ inverseˡ : Inverseˡ _≈₁_ _≈₂_ f g₁ cong₃ : Congruent _≈₂_ _≈₁_ g₂ inverseʳ : Inverseʳ _≈₁_ _≈₂_ f g₂ open IsCongruent f-isCongruent public renaming (cong to cong₁)