Skip to content

Order.Iso

Order isomorphisms

This is the Order.Iso module of the Agda Universal Algebra Library.

An order isomorphism between two ordered objects is a pair of monotone maps that are mutually inverse up to the respective equivalences. Because both maps are monotone and the round trips are the identity up to the equivalence, an order isomorphism transports every existing infimum and supremum, so isomorphic posets carry the same lattice (indeed, complete-lattice) structure; this is why no separate preservation clauses for meet and join are needed.

OrderIso states this for raw relations rather than for a bundle, so it applies uniformly to setoid-valued and propositionally-valued orders. That generality is what the library's two motivating instances need: the congruence poset (Con 𝑨 , ≑ , βŠ†) of Setoid.Congruences.Lattice carries an equivalence of mutual containment rather than propositional equality, while a classical lattice carries its meet order from Classical.Properties.Lattice.

(The standard library's IsOrderIsomorphism packages one map with surjectivity instead of an explicit inverse; the two presentations are interconvertible, and the inverse-pair form is the convenient one for transporting structure.)

The record was introduced in FLRP.Problem, next to its first use, with a note that it should migrate here once the group-theoretic side of the library needed it. Classical.Structures.Group.Congruences is that consumer β€” the correspondence between normal subgroups and congruences is ordinary group theory, below the FLRP tree β€” so the record now lives in Order/ and FLRP.Problem re-exports it.

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

module Order.Iso where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Level            using ( Level ; _βŠ”_ )
open import Relation.Binary  using () renaming ( Rel to BinaryRel )

The record

record OrderIso
  {a b ℓ₁ β„“β‚‚ m₁ mβ‚‚ : Level}
  {A : Type a} {B : Type b}
  (_β‰ˆβ‚_ : BinaryRel A ℓ₁) (_≀₁_ : BinaryRel A β„“β‚‚)
  (_β‰ˆβ‚‚_ : BinaryRel B m₁) (_≀₂_ : BinaryRel B mβ‚‚) : Type (a βŠ” b βŠ” ℓ₁ βŠ” β„“β‚‚ βŠ” m₁ βŠ” mβ‚‚) where
  field
    to         : A β†’ B
    from       : B β†’ A
    to-mono    : βˆ€ {x y} β†’ x ≀₁ y β†’ to x ≀₂ to y
    from-mono  : βˆ€ {u v} β†’ u ≀₂ v β†’ from u ≀₁ from v
    to∘from    : βˆ€ u β†’ to (from u) β‰ˆβ‚‚ u
    from∘to    : βˆ€ x β†’ from (to x) β‰ˆβ‚ x