↑ Top


Setoid functions

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

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

module Setoid.Functions.Basic where

-- Imports from Agda and the Agda Standard Library -----------------------
open import Agda.Primitive   using ()  renaming ( Set to Type )
open import Function         using ( id )   renaming ( Func to _⟶_ ; _∘_ to _□_ )
open import Level            using ( Level ; Lift ; _⊔_ )
open import Relation.Binary  using ( Setoid )

private variable α ρᵃ β ρᵇ γ ρᶜ : Level

𝑖𝑑 : {A : Setoid α ρᵃ}  A  A
𝑖𝑑 {A} = record { f = id ; cong = id }

open _⟶_ renaming ( f to _⟨$⟩_ )

_∘_ :  {A : Setoid α ρᵃ}{B : Setoid β ρᵇ}{C : Setoid γ ρᶜ}
      B  C  A  B  A  C
f  g = record { f = (_⟨$⟩_ 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 { f = lift ; cong = id }


↑ Setoid.Overture Setoid.Overture.Inverses →