↑ Top


Preliminaries for setoids

This is the Setoid.Overture.Preliminaries module of the agda-algebras library.

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


module Setoid.Overture.Preliminaries where

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

import Function.Base as Fun
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 = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
               ; cong = Fun._∘_ (cong f) (cong g)
               }


module _ {𝑨 : Setoid α ρᵃ} where
 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 }

 module _ {𝑩 : Setoid β ρᵇ} where
  open Setoid 𝑩 using ( sym ) renaming (Carrier to B; _≈_ to _≈₂_)

  -- This is sometimes known as `cong` (see e.g. `Function.Equality` in the agda-stdlib)
  -- preserves≈ : (A → B) → Type (α ⊔ ρᵃ ⊔ ρᵇ)
  -- preserves≈ f = ∀ {x y} → x ≈ₐ y → (f x) ≈₂ (f y)


↑ Setoid.Overture Setoid.Overture.Inverses →