{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Function.Structures {a b ℓ₁ ℓ₂}
{A : Set a} (_≈₁_ : Rel A ℓ₁)
{B : Set b} (_≈₂_ : Rel B ℓ₂)
where
open import Data.Product using (∃; _×_; _,_)
open import Function.Base
open import Function.Definitions
open import Level using (_⊔_)
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
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
}
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)
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 cong₁)
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ʳ
}
inverse : Inverseᵇ _≈₁_ _≈₂_ to from
inverse = inverseˡ , inverseʳ
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)