------------------------------------------------------------------------ -- The Agda standard library -- -- Relationships between properties of functions where the equality -- over both the domain and codomain is assumed to be _≡_ ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Consequences.Propositional {a b} {A : Set a} {B : Set b} where open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong) open import Relation.Binary.PropositionalEquality.Properties using (setoid) open import Function.Definitions using (StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Inverseˡ ; Inverseʳ; Surjective) open import Relation.Nullary.Negation.Core using (contraposition) import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid ------------------------------------------------------------------------ -- Re-export setoid properties open Setoid public hiding ( strictlySurjective⇒surjective ; strictlyInverseˡ⇒inverseˡ ; strictlyInverseʳ⇒inverseʳ ) ------------------------------------------------------------------------ -- Properties that rely on congruence private variable f : A → B f⁻¹ : B → A strictlySurjective⇒surjective : StrictlySurjective _≡_ f → Surjective _≡_ _≡_ f strictlySurjective⇒surjective = Setoid.strictlySurjective⇒surjective (cong _) strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ → Inverseˡ _≡_ _≡_ f f⁻¹ strictlyInverseˡ⇒inverseˡ f = Setoid.strictlyInverseˡ⇒inverseˡ (cong _) strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ → Inverseʳ _≡_ _≡_ f f⁻¹ strictlyInverseʳ⇒inverseʳ f = Setoid.strictlyInverseʳ⇒inverseʳ (cong _)