{-# 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 ℓ₁)
{B : Set b} (_≈₂_ : Rel B ℓ₂)
where
open import Data.Product.Base as 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
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)
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ʳ
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)
record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
from : B → A
isLeftInverse : IsLeftInverse f from
open IsLeftInverse isLeftInverse public