123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114-------------------------------------------------------------------------- The Agda standard library---- Relationships between properties of functions. See-- `Function.Consequences.Propositional` for specialisations to-- propositional equality.------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Consequences where open import Data.Product.Base as Productopen import Function.Definitionsopen import Level using (Level)open import Relation.Binary.Core using (Rel)open import Relation.Binary.Bundles using (Setoid)open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)open import Relation.Nullary.Negation.Core using (¬_; contraposition) private variable a b ℓ₁ ℓ₂ : Level A B : Set a ≈₁ ≈₂ : Rel A ℓ₁ f f⁻¹ : A → B -------------------------------------------------------------------------- Injective contraInjective : ∀ (≈₂ : Rel B ℓ₂) → Injective ≈₁ ≈₂ f → ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))contraInjective _ inj p = contraposition inj p -------------------------------------------------------------------------- Inverseˡ inverseˡ⇒surjective : ∀ (≈₂ : Rel B ℓ₂) → Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ finverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ) -------------------------------------------------------------------------- Inverseʳ inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f → Reflexive ≈₂ → Symmetric ≈₁ → Transitive ≈₁ → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ finverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy = trans (sym (invʳ refl)) (invʳ fx≈fy) -------------------------------------------------------------------------- Inverseᵇ inverseᵇ⇒bijective : ∀ (≈₂ : Rel B ℓ₂) → Reflexive ≈₂ → Symmetric ≈₁ → Transitive ≈₁ → Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ finverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) = (inverseʳ⇒injective ≈₂ f refl sym trans invʳ , inverseˡ⇒surjective ≈₂ invˡ) -------------------------------------------------------------------------- StrictlySurjective surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) → Reflexive ≈₁ → Surjective ≈₁ ≈₂ f → StrictlySurjective ≈₂ fsurjective⇒strictlySurjective _ refl surj x = Product.map₂ (λ v → v refl) (surj x) strictlySurjective⇒surjective : Transitive ≈₂ → Congruent ≈₁ ≈₂ f → StrictlySurjective ≈₂ f → Surjective ≈₁ ≈₂ fstrictlySurjective⇒surjective trans cong surj x = Product.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x) -------------------------------------------------------------------------- StrictlyInverseˡ inverseˡ⇒strictlyInverseˡ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) → Reflexive ≈₁ → Inverseˡ ≈₁ ≈₂ f f⁻¹ → StrictlyInverseˡ ≈₂ f f⁻¹inverseˡ⇒strictlyInverseˡ _ _ refl sinv x = sinv refl strictlyInverseˡ⇒inverseˡ : Transitive ≈₂ → Congruent ≈₁ ≈₂ f → StrictlyInverseˡ ≈₂ f f⁻¹ → Inverseˡ ≈₁ ≈₂ f f⁻¹strictlyInverseˡ⇒inverseˡ trans cong sinv {x} y≈f⁻¹x = trans (cong y≈f⁻¹x) (sinv x) -------------------------------------------------------------------------- StrictlyInverseʳ inverseʳ⇒strictlyInverseʳ : ∀ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) → Reflexive ≈₂ → Inverseʳ ≈₁ ≈₂ f f⁻¹ → StrictlyInverseʳ ≈₁ f f⁻¹inverseʳ⇒strictlyInverseʳ _ _ refl sinv x = sinv refl strictlyInverseʳ⇒inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ → StrictlyInverseʳ ≈₁ f f⁻¹ → Inverseʳ ≈₁ ≈₂ f f⁻¹strictlyInverseʳ⇒inverseʳ trans cong sinv {x} y≈f⁻¹x = trans (cong y≈f⁻¹x) (sinv x)