------------------------------------------------------------------------ -- 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 Product open import Function.Definitions open 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 ≈₁ ≈₂ f inverseˡ⇒surjective ≈₂ invˡ y = (_ , invˡ) ------------------------------------------------------------------------ -- Inverseʳ inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f → Reflexive ≈₂ → Symmetric ≈₁ → Transitive ≈₁ → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f inverseʳ⇒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 ≈₁ ≈₂ f inverseᵇ⇒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 ≈₂ f surjective⇒strictlySurjective _ refl surj x = Product.map₂ (λ v → v refl) (surj x) strictlySurjective⇒surjective : Transitive ≈₂ → Congruent ≈₁ ≈₂ f → StrictlySurjective ≈₂ f → Surjective ≈₁ ≈₂ f strictlySurjective⇒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)