------------------------------------------------------------------------
-- 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)
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 using (_∘_; id)
open import Function.Definitions using(StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Congruent)
open import Function.Consequences.Setoid
using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ
; strictlyInverseʳ⇒inverseʳ)
open import Level using (_⊔_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
open import Function.Structures _≈₁_ _≈₂_
------------------------------------------------------------------------
-- 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)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4