------------------------------------------------------------------------
-- The Agda standard library
--
-- Constant morphisms between binary relations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Morphism.Construct.Constant where
open import Function.Base using (const)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid; Preorder)
open import Relation.Binary.Definitions using (Reflexive)
open import Relation.Binary.Morphism.Structures
using (IsRelHomomorphism; IsOrderHomomorphism)
open import Relation.Binary.Morphism.Bundles
using (SetoidHomomorphism; PreorderHomomorphism)
private
variable
a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
A B : Set a
------------------------------------------------------------------------
-- Relations
------------------------------------------------------------------------
module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) where
isRelHomomorphism : Reflexive ≈₂ →
∀ x → IsRelHomomorphism ≈₁ ≈₂ (const x)
isRelHomomorphism refl x = record
{ cong = const refl
}
module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where
setoidHomomorphism : ∀ x → SetoidHomomorphism S T
setoidHomomorphism x = record
{ isRelHomomorphism = isRelHomomorphism _ _ T.refl x
} where module T = Setoid T
------------------------------------------------------------------------
-- Orders
------------------------------------------------------------------------
module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (∼₁ : Rel A ℓ₃) (∼₂ : Rel B ℓ₄) where
isOrderHomomorphism : Reflexive ≈₂ → Reflexive ∼₂ →
∀ x → IsOrderHomomorphism ≈₁ ≈₂ ∼₁ ∼₂ (const x)
isOrderHomomorphism ≈-refl ∼-refl x = record
{ cong = const ≈-refl
; mono = const ∼-refl
}
module _ (P : Preorder a ℓ₁ ℓ₂) (Q : Preorder b ℓ₃ ℓ₄) where
preorderHomomorphism : ∀ x → PreorderHomomorphism P Q
preorderHomomorphism x = record
{ isOrderHomomorphism = isOrderHomomorphism _ _ _ _ Q.Eq.refl Q.refl x
} where module Q = Preorder Q
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