------------------------------------------------------------------------
-- The Agda standard library
--
-- The identity morphism for binary relations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Morphism.Construct.Identity where
open import Data.Product.Base using (_,_)
open import Function.Base using (id)
import Function.Construct.Identity as Id
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
open import Relation.Binary.Definitions using (Reflexive)
open import Relation.Binary.Morphism.Structures
using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism
; IsOrderHomomorphism; IsOrderMonomorphism; IsOrderIsomorphism)
open import Relation.Binary.Morphism.Bundles
using (SetoidHomomorphism; SetoidMonomorphism; SetoidIsomorphism
; PreorderHomomorphism; PosetHomomorphism)
private
variable
a ℓ₁ ℓ₂ : Level
A : Set a
------------------------------------------------------------------------
-- Relations
------------------------------------------------------------------------
-- Structures
module _ (≈ : Rel A ℓ₁) where
isRelHomomorphism : IsRelHomomorphism ≈ ≈ id
isRelHomomorphism = record
{ cong = Id.congruent ≈
}
isRelMonomorphism : IsRelMonomorphism ≈ ≈ id
isRelMonomorphism = record
{ isHomomorphism = isRelHomomorphism
; injective = Id.injective ≈
}
isRelIsomorphism : Reflexive ≈ → IsRelIsomorphism ≈ ≈ id
isRelIsomorphism refl = record
{ isMonomorphism = isRelMonomorphism
; surjective = Id.surjective ≈
}
------------------------------------------------------------------------
-- Bundles
module _ (S : Setoid a ℓ₁) where
open Setoid S
setoidHomomorphism : SetoidHomomorphism S S
setoidHomomorphism = record { isRelHomomorphism = isRelHomomorphism _≈_ }
setoidMonomorphism : SetoidMonomorphism S S
setoidMonomorphism = record { isRelMonomorphism = isRelMonomorphism _≈_ }
setoidIsomorphism : SetoidIsomorphism S S
setoidIsomorphism = record { isRelIsomorphism = isRelIsomorphism _ refl }
------------------------------------------------------------------------
-- Orders
------------------------------------------------------------------------
-- Structures
module _ (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) where
isOrderHomomorphism : IsOrderHomomorphism ≈ ≈ ∼ ∼ id
isOrderHomomorphism = record
{ cong = id
; mono = id
}
isOrderMonomorphism : IsOrderMonomorphism ≈ ≈ ∼ ∼ id
isOrderMonomorphism = record
{ isOrderHomomorphism = isOrderHomomorphism
; injective = Id.injective ≈
; cancel = id
}
isOrderIsomorphism : Reflexive ≈ → IsOrderIsomorphism ≈ ≈ ∼ ∼ id
isOrderIsomorphism refl = record
{ isOrderMonomorphism = isOrderMonomorphism
; surjective = Id.surjective ≈
}
------------------------------------------------------------------------
-- Bundles
module _ (P : Preorder a ℓ₁ ℓ₂) where
preorderHomomorphism : PreorderHomomorphism P P
preorderHomomorphism = record { isOrderHomomorphism = isOrderHomomorphism _ _ }
module _ (P : Poset a ℓ₁ ℓ₂) where
posetHomomorphism : PosetHomomorphism P P
posetHomomorphism = record { isOrderHomomorphism = isOrderHomomorphism _ _ }
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