↑ Top


Discrete Relations on Setoids

This is the Setoid.Relations.Discrete module of the Agda Universal Algebra Library.

{-# OPTIONS --without-K --exact-split --safe #-}

module Setoid.Relations.Discrete where

-- Imports from Agda and the Agda Standard Library ----------------------------------------------
open import Agda.Primitive        using ( _⊔_ ; lsuc ) renaming ( Set to Type )
open import Data.Product          using ( _,_ ; _×_ )
open import Function.Bundles      using () renaming ( Func to _⟶_ )
open import Function.Base         using ( _∘_ )
open import Level                 using ( Level ; Lift )
open import Relation.Binary       using ( IsEquivalence ; Setoid )
open import Relation.Binary.Core  using ( _⇒_ ; _=[_]⇒_ ) renaming ( REL to BinREL ; Rel to BinRel )
open import Relation.Binary.Definitions
                                  using ( Reflexive ; Transitive )
open import Relation.Unary        using ( _∈_; Pred )
open import Relation.Binary.PropositionalEquality
                                  using ( _≡_ )

-- Imports from agda-algebras -------------------------------------------------------------------
open import Base.Overture.Preliminaries using ( Π-syntax )

private variable α β ρᵃ ρᵇ  𝓥 : Level

Here is a function that is useful for defining poitwise equality of functions wrt a given equality.

open _⟶_ renaming ( f to _⟨$⟩_ )
module _ {𝐴 : Setoid α ρᵃ}{𝐵 : Setoid β ρᵇ} where
 open Setoid 𝐴 using () renaming ( Carrier to A ; _≈_ to _≈₁_ )
 open Setoid 𝐵 using () renaming ( Carrier to B ; _≈_ to _≈₂_ )

 function-equality : BinRel (𝐴  𝐵) (α  ρᵇ)
 function-equality f g =  x  f ⟨$⟩ x ≈₂ g ⟨$⟩ x

Here is useful notation for asserting that the image of a function (the first argument) is contained in a predicate, the second argument (a “subset” of the codomain).

 Im_⊆_ : (𝐴  𝐵)  Pred B   Type (α  )
 Im f  S =  x  f ⟨$⟩ x  S

Kernels on setoids

Given setoids 𝐴 and 𝐵 (with carriers A and B, resp), the kernel of a function f : 𝐴 ⟶ 𝐵 is defined informally by {(x , y) ∈ A × A : f ⟨$⟩ x ≈₂ f ⟨$⟩ y}.

 fker : (𝐴  𝐵)  BinRel A ρᵇ
 fker g x y = g ⟨$⟩ x ≈₂ g ⟨$⟩ y

 fkerPred : (𝐴  𝐵)  Pred (A × A) ρᵇ
 fkerPred g (x , y) = g ⟨$⟩ x ≈₂ g ⟨$⟩ y

 open IsEquivalence

 fkerlift : (𝐴  𝐵)  ( : Level)  BinRel A (  ρᵇ)
 fkerlift g  x y = Lift  (g ⟨$⟩ x ≈₂ g ⟨$⟩ y)

 -- The *identity relation* (equivalently, the kernel of a 1-to-1 function)
 0rel : { : Level}  BinRel A (ρᵃ  )
 0rel {} = λ x y  Lift  (x ≈₁ y)



↑ Setoid.Relations Setoid.Relations.Quotients →