↑ 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 →