Skip to content

Setoid.Functions.Basic

Setoid functions

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

A setoid function A ⟢ B is the standard library's Func: a map on carriers together with a proof that the map respects the equalities of A and B. Carrying that proof along with the function is what the whole Setoid/ tree rests on, but it is worth being precise about what it does.

cong says that one map sends related arguments to related results; it says nothing about when two maps are the same. Where two functions do have to be compared, the library never asks for propositional equality of functions, but instead uses an explicitly pointwise relation: function-equality of Setoid.Relations.Discrete, and _≋_ of Setoid.Categories.Algebra for homomorphisms. The two devices together are what keep the development extensionality-free.

This module holds the primitives everything else is built from, and nothing deeper: the identity setoid function, composition, and the universe lifting of a setoid. They are gathered here so that the lifting lemmas in particular exist in one place, rather than being re-derived wherever a level has to change.

{-# 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

Because a setoid function carries its own congruence proof, identity and composition need no side conditions: each simply does to the proofs what it does to the maps.

  • 𝑖𝑑 is the identity, whose congruence proof is itself the identity.
  • _βŠ™_ is composition, taking the composite of the two maps and the composite of the two congruence proofs. It is written right to left, so f βŠ™ g applies g first.

The remaining items lift a setoid to a higher universe level, which Agda's universe non-cumulativity makes necessary.

  • 𝑙𝑖𝑓𝑑 β„“ raises the level of the carrier and leaves the equality alone, relating two lifted elements exactly when the elements underneath them were related;
  • liftFunc is the setoid function into the lift;
  • lift∼lower and lower∼lift say that lifting and lowering are mutually inverse; both are proved by reflexivity alone, which is the point: the lifted equality is the original equality read through lower, so there is nothing to transport.
𝑖𝑑 : {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 }