{-# 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
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ʳ
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ʳ _≈_
}
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ᵇ _≈_
}
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)
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."
#-}