------------------------------------------------------------------------ -- The Agda standard library -- -- Order morphisms ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel) module Relation.Binary.Morphism.Structures {a b} {A : Set a} {B : Set b} where open import Data.Product.Base using (_,_) open import Function.Definitions using (Injective; Surjective; Bijective) open import Level using (Level; _⊔_) open import Relation.Binary.Morphism.Definitions A B private variable ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level ------------------------------------------------------------------------ -- Relations ------------------------------------------------------------------------ record IsRelHomomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂) (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field cong : Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧ record IsRelMonomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂) (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isHomomorphism : IsRelHomomorphism _∼₁_ _∼₂_ ⟦_⟧ injective : Injective _∼₁_ _∼₂_ ⟦_⟧ open IsRelHomomorphism isHomomorphism public record IsRelIsomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂) (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧ surjective : Surjective _∼₁_ _∼₂_ ⟦_⟧ open IsRelMonomorphism isMonomorphism public bijective : Bijective _∼₁_ _∼₂_ ⟦_⟧ bijective = injective , surjective ------------------------------------------------------------------------ -- Orders ------------------------------------------------------------------------ record IsOrderHomomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄) (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where field cong : Homomorphic₂ _≈₁_ _≈₂_ ⟦_⟧ mono : Homomorphic₂ _≲₁_ _≲₂_ ⟦_⟧ module Eq where isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ isRelHomomorphism = record { cong = cong } isRelHomomorphism : IsRelHomomorphism _≲₁_ _≲₂_ ⟦_⟧ isRelHomomorphism = record { cong = mono } record IsOrderMonomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄) (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where field isOrderHomomorphism : IsOrderHomomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧ injective : Injective _≈₁_ _≈₂_ ⟦_⟧ cancel : Injective _≲₁_ _≲₂_ ⟦_⟧ open IsOrderHomomorphism isOrderHomomorphism public hiding (module Eq) module Eq where isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧ isRelMonomorphism = record { isHomomorphism = IsOrderHomomorphism.Eq.isRelHomomorphism isOrderHomomorphism ; injective = injective } isRelMonomorphism : IsRelMonomorphism _≲₁_ _≲₂_ ⟦_⟧ isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = cancel } record IsOrderIsomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄) (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where field isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧ surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ open IsOrderMonomorphism isOrderMonomorphism public hiding (module Eq) module Eq where isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧ isRelIsomorphism = record { isMonomorphism = IsOrderMonomorphism.Eq.isRelMonomorphism isOrderMonomorphism ; surjective = surjective }