------------------------------------------------------------------------ -- The Agda standard library -- -- The identity function ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Construct.Identity where open import Data.Product.Base using (_,_) open import Function.Base using (id) open import Function.Bundles import Function.Definitions as Definitions import Function.Structures as Structures open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Structures as B hiding (IsEquivalence) open import Relation.Binary.Definitions using (Reflexive) open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Relation.Binary.PropositionalEquality.Properties using (setoid) private variable a ℓ : Level A : Set a ------------------------------------------------------------------------ -- Properties module _ (_≈_ : Rel A ℓ) where open Definitions congruent : Congruent _≈_ _≈_ id congruent = id injective : Injective _≈_ _≈_ id injective = id surjective : Surjective _≈_ _≈_ id surjective x = x , id bijective : Bijective _≈_ _≈_ id bijective = injective , surjective inverseˡ : Inverseˡ _≈_ _≈_ id id inverseˡ = id inverseʳ : Inverseʳ _≈_ _≈_ id id inverseʳ = id inverseᵇ : Inverseᵇ _≈_ _≈_ id id inverseᵇ = inverseˡ , inverseʳ ------------------------------------------------------------------------ -- Structures module _ {_≈_ : Rel A ℓ} (isEq : B.IsEquivalence _≈_) where open Structures _≈_ _≈_ open B.IsEquivalence isEq isCongruent : IsCongruent id isCongruent = record { cong = id ; isEquivalence₁ = isEq ; isEquivalence₂ = isEq } isInjection : IsInjection id isInjection = record { isCongruent = isCongruent ; injective = injective _≈_ } isSurjection : IsSurjection id isSurjection = record { isCongruent = isCongruent ; surjective = surjective _≈_ } isBijection : IsBijection id isBijection = record { isInjection = isInjection ; surjective = surjective _≈_ } isLeftInverse : IsLeftInverse id id isLeftInverse = record { isCongruent = isCongruent ; from-cong = id ; inverseˡ = inverseˡ _≈_ } isRightInverse : IsRightInverse id id isRightInverse = record { isCongruent = isCongruent ; from-cong = id ; inverseʳ = inverseʳ _≈_ } isInverse : IsInverse id id isInverse = record { isLeftInverse = isLeftInverse ; inverseʳ = inverseʳ _≈_ } ------------------------------------------------------------------------ -- Setoid bundles module _ (S : Setoid a ℓ) where open Setoid S function : Func S S function = record { to = id ; cong = id } injection : Injection S S injection = record { to = id ; cong = id ; injective = injective _≈_ } surjection : Surjection S S surjection = record { to = id ; cong = id ; surjective = surjective _≈_ } bijection : Bijection S S bijection = record { to = id ; cong = id ; bijective = bijective _≈_ } equivalence : Equivalence S S equivalence = record { to = id ; from = id ; to-cong = id ; from-cong = id } leftInverse : LeftInverse S S leftInverse = record { to = id ; from = id ; to-cong = id ; from-cong = id ; inverseˡ = inverseˡ _≈_ } rightInverse : RightInverse S S rightInverse = record { to = id ; from = id ; to-cong = id ; from-cong = id ; inverseʳ = inverseʳ _≈_ } inverse : Inverse S S inverse = record { to = id ; from = id ; to-cong = id ; from-cong = id ; inverse = inverseᵇ _≈_ } ------------------------------------------------------------------------ -- Propositional bundles module _ (A : Set a) where ⟶-id : A ⟶ A ⟶-id = function (setoid A) ↣-id : A ↣ A ↣-id = injection (setoid A) ↠-id : A ↠ A ↠-id = surjection (setoid A) ⤖-id : A ⤖ A ⤖-id = bijection (setoid A) ⇔-id : A ⇔ A ⇔-id = equivalence (setoid A) ↩-id : A ↩ A ↩-id = leftInverse (setoid A) ↪-id : A ↪ A ↪-id = rightInverse (setoid A) ↔-id : A ↔ A ↔-id = inverse (setoid A) ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version v2.0 id-⟶ = ⟶-id {-# WARNING_ON_USAGE id-⟶ "Warning: id-⟶ was deprecated in v2.0. Please use ⟶-id instead." #-} id-↣ = ↣-id {-# WARNING_ON_USAGE id-↣ "Warning: id-↣ was deprecated in v2.0. Please use ↣-id instead." #-} id-↠ = ↠-id {-# WARNING_ON_USAGE id-↠ "Warning: id-↠ was deprecated in v2.0. Please use ↠-id instead." #-} id-⤖ = ⤖-id {-# WARNING_ON_USAGE id-⤖ "Warning: id-⤖ was deprecated in v2.0. Please use ⤖-id instead." #-} id-⇔ = ⇔-id {-# WARNING_ON_USAGE id-⇔ "Warning: id-⇔ was deprecated in v2.0. Please use ⇔-id instead." #-} id-↩ = ↩-id {-# WARNING_ON_USAGE id-↩ "Warning: id-↩ was deprecated in v2.0. Please use ↩-id instead." #-} id-↪ = ↪-id {-# WARNING_ON_USAGE id-↪ "Warning: id-↪ was deprecated in v2.0. Please use ↪-id instead." #-} id-↔ = ↔-id {-# WARNING_ON_USAGE id-↔ "Warning: id-↔ was deprecated in v2.0. Please use ↔-id instead." #-}