------------------------------------------------------------------------
-- 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
using (Congruent; Injective; Surjective; Bijective; Inverseʳ; Inverseˡ
; Inverseᵇ)
import Function.Structures as Structures
using (IsCongruent; IsInjection; IsSurjection; IsBijection; IsLeftInverse
; IsRightInverse; IsInverse)
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."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4