------------------------------------------------------------------------ -- The Agda standard library -- -- The identity function ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Function.Construct.Identity where open import Data.Product using (_,_) open import Function.Base using (id) open import Function.Bundles import Function.Definitions as Definitions import Function.Structures as Structures open import Level open import Relation.Binary as B hiding (_⇔_; IsEquivalence) open import Relation.Binary.PropositionalEquality 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 : Reflexive _≈_ Surjective id surjective refl x = x , refl bijective : Reflexive _≈_ Bijective id bijective refl = injective , surjective refl inverseˡ : Reflexive _≈_ Inverseˡ id id inverseˡ refl x = refl inverseʳ : Reflexive _≈_ Inverseʳ id id inverseʳ refl x = refl inverseᵇ : Reflexive _≈_ Inverseᵇ id id inverseᵇ refl = inverseˡ refl , inverseʳ refl ------------------------------------------------------------------------ -- 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 _≈_ refl } isBijection : IsBijection id isBijection = record { isInjection = isInjection ; surjective = surjective _≈_ refl } isLeftInverse : IsLeftInverse id id isLeftInverse = record { isCongruent = isCongruent ; cong₂ = id ; inverseˡ = inverseˡ _≈_ refl } isRightInverse : IsRightInverse id id isRightInverse = record { isCongruent = isCongruent ; cong₂ = id ; inverseʳ = inverseʳ _≈_ refl } isInverse : IsInverse id id isInverse = record { isLeftInverse = isLeftInverse ; inverseʳ = inverseʳ _≈_ refl } ------------------------------------------------------------------------ -- Setoid bundles module _ (S : Setoid a ) where open Setoid S function : Func S S function = record { f = id ; cong = id } injection : Injection S S injection = record { f = id ; cong = id ; injective = injective _≈_ } surjection : Surjection S S surjection = record { f = id ; cong = id ; surjective = surjective _≈_ refl } bijection : Bijection S S bijection = record { f = id ; cong = id ; bijective = bijective _≈_ refl } equivalence : Equivalence S S equivalence = record { f = id ; g = id ; cong₁ = id ; cong₂ = id } leftInverse : LeftInverse S S leftInverse = record { f = id ; g = id ; cong₁ = id ; cong₂ = id ; inverseˡ = inverseˡ _≈_ refl } rightInverse : RightInverse S S rightInverse = record { f = id ; g = id ; cong₁ = id ; cong₂ = id ; inverseʳ = inverseʳ _≈_ refl } inverse : Inverse S S inverse = record { f = id ; f⁻¹ = id ; cong₁ = id ; cong₂ = id ; inverse = inverseᵇ _≈_ refl } ------------------------------------------------------------------------ -- 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)