------------------------------------------------------------------------
-- The Agda standard library
--
-- The projection morphisms for relational structures arising from the
-- non-dependent product construction
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Relation.Binary.Morphism.Construct.Product where
import Data.Product.Base as Product using (<_,_>; proj₁; proj₂)
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
using (Pointwise)
open import Level using (Level)
open import Relation.Binary.Bundles.Raw using (RawSetoid)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism)
private
variable
a b c ℓ₁ ℓ₂ ℓ : Level
A : Set a
B : Set b
C : Set c
------------------------------------------------------------------------
-- definitions
module _ (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) where
private
_≈_ = Pointwise _≈₁_ _≈₂_
module Proj₁ where
isRelHomomorphism : IsRelHomomorphism _≈_ _≈₁_ Product.proj₁
isRelHomomorphism = record { cong = Product.proj₁ }
module Proj₂ where
isRelHomomorphism : IsRelHomomorphism _≈_ _≈₂_ Product.proj₂
isRelHomomorphism = record { cong = Product.proj₂ }
module Pair (_≈′_ : Rel C ℓ) where
isRelHomomorphism : ∀ {h k} →
IsRelHomomorphism _≈′_ _≈₁_ h →
IsRelHomomorphism _≈′_ _≈₂_ k →
IsRelHomomorphism _≈′_ _≈_ Product.< h , k >
isRelHomomorphism H K = record { cong = Product.< H.cong , K.cong > }
where
module H = IsRelHomomorphism H
module K = IsRelHomomorphism K
------------------------------------------------------------------------
-- package up for export
module _ {M : RawSetoid a ℓ₁} {N : RawSetoid b ℓ₂} where
private
module M = RawSetoid M
module N = RawSetoid N
proj₁ = Proj₁.isRelHomomorphism M._≈_ N._≈_
proj₂ = Proj₂.isRelHomomorphism M._≈_ N._≈_
module _ {P : RawSetoid c ℓ} where
private
module P = RawSetoid P
<_,_> = Pair.isRelHomomorphism M._≈_ N._≈_ P._≈_
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