Skip to content

Setoid.Functions.Basic

Setoid functions

This is the Setoid.Functions.Basic module of the Agda Universal Algebra Library.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Functions.Basic where

-- Imports from Agda and the Agda Standard Library -----------------------
open import Function         using ( id ; _∘_ ) renaming ( Func to _⟢_ )
open import Level            using ( Level ; Lift ; _βŠ”_ )
open import Relation.Binary  using ( Setoid )

private variable Ξ± ρᡃ Ξ² ρᡇ Ξ³ ρᢜ : Level

𝑖𝑑 : {A : Setoid Ξ± ρᡃ} β†’ A ⟢ A
𝑖𝑑 {A} = record { to = id ; cong = id }

open _⟢_ renaming ( to to _⟨$⟩_ )

_βŠ™_ :  {A : Setoid Ξ± ρᡃ}{B : Setoid Ξ² ρᡇ}{C : Setoid Ξ³ ρᢜ}
  β†’     B ⟢ C β†’ A ⟢ B β†’ A ⟢ C
f βŠ™ g = record { to = (_⟨$⟩_ f) ∘ (_⟨$⟩_ g); cong = (cong f) ∘ (cong g) }

module _ {𝑨 : Setoid Ξ± ρᡃ} where
  open Lift ; open Level ; open Setoid using (_β‰ˆ_)
  open Setoid 𝑨 using ( sym ; trans ) renaming (Carrier to A ; _β‰ˆ_ to _β‰ˆβ‚_ ; refl to reflₐ)

  𝑙𝑖𝑓𝑑 : βˆ€ β„“ β†’ Setoid (Ξ± βŠ” β„“) ρᡃ
  𝑙𝑖𝑓𝑑 β„“ = record  { Carrier = Lift β„“ A
                 ; _β‰ˆ_ = Ξ» x y β†’ (lower x) β‰ˆβ‚ (lower y)
                 ; isEquivalence = record { refl = reflₐ ; sym = sym ; trans = trans }
                 }

  lift∼lower : (a : Lift Ξ² A) β†’ (_β‰ˆ_ (𝑙𝑖𝑓𝑑 Ξ²)) (lift (lower a)) a
  lift∼lower a = reflₐ

  lower∼lift : βˆ€ a β†’ (lower {Ξ±}{Ξ²}) (lift a) β‰ˆβ‚ a
  lower∼lift _ = reflₐ

  liftFunc : {β„“ : Level} β†’ 𝑨 ⟢ 𝑙𝑖𝑓𝑑 β„“
  liftFunc = record { to = lift ; cong = id }