Some simple order/category theory

Preorders.agda

{-# OPTIONS --postfix-projections #-}
module Preorders where

open import Level
open import Data.Unit hiding (_≤_)
open import Data.Product hiding (map)
open import Function hiding (id)
open import Relation.Binary public using (Reflexive; Transitive; Symmetric; _=[_]⇒_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)


-- Preordered sets ("prosets"). Or, as I prefer to think about them,
-- lawless categories.
record Proset i j : Set (suc (i ⊔ j)) where
  constructor Proset:
  infix  2 Hom
  infixr 9 compo
  field Obj : Set i
  field Hom : (a b : Obj) -> Set j
  field ident : Reflexive Hom
  field compo : Transitive Hom

  -- Two objects are "equivalent" if each has a morphism to the other.
  equiv : (a b : Obj) -> Set j
  equiv a b = Hom a b × Hom b a

  -- Undirected paths between objects, which may take morphisms in either
  -- direction.
  data path : (a b : Obj) -> Set (i ⊔ j) where
    path-by : ∀{a b} -> Hom a b -> path a b
    path-flip : ∀{a b} -> path a b -> path b a
    path-compo : ∀{a b c} -> path a b -> path b c -> path a c

  module _ {k} (F : Obj -> Obj -> Set k)
           (hom→F : ∀{a b} -> Hom a b -> F a b)
           (F-symm : Symmetric F) (F-trans : Transitive F) where
    path-fold : ∀{a b} -> path a b -> F a b
    path-fold (path-by x) = hom→F x
    path-fold (path-flip p) = F-symm (path-fold p)
    path-fold (path-compo p q) = F-trans (path-fold p) (path-fold q)

open Proset public
open Proset {{...}} public using ()
  renaming (Hom to _≤_; ident to id; compo to _∙_; equiv to _↔_; path to _~_)

-- A monotone (preorder-preserving) map, or lawless functor.
record Fun {i j k l} (A : Proset i j) (B : Proset k l) : Set (i ⊔ j ⊔ k ⊔ l) where
  constructor Fun:
  field ap  : Obj A -> Obj B
  field map : Hom A =[ ap ]⇒ Hom B

open Fun public
pattern fun {F} f = Fun: F f
infixr 4 _⇒_; _⇒_ = Fun

infixr 9 _•_
_•_ : ∀{i j k l m n A B C} -> Fun {i}{j} A B -> Fun {k}{l}{m}{n} B C -> A ⇒ C
fun F • fun G = fun (G ∘ F)

sets : ∀ i -> Proset (suc i) i
sets i = Proset: (Set i) (λ A B -> A -> B) (λ x -> x) (λ f g -> g ∘ f)
instance -sets = λ {i} -> sets i

prosets : ∀ i j -> Proset (suc (i ⊔ j)) (i ⊔ j)
prosets i j = Proset: (Proset i j) Fun (fun id) _•_
instance -prosets = λ {i}{j} -> prosets i j

-- Equivalence relations, or lawless groupoids.
Equiv : ∀ i j -> Set (suc (i ⊔ j))
Equiv i j = Σ[ P ∈ Proset i j ] Symmetric (Hom P)

equivs : ∀ i j -> Proset (suc (i ⊔ j)) (i ⊔ j)
equivs i j = Proset: (Equiv i j) (λ a b → proj₁ a ⇒ proj₁ b) id _•_

-- Some forgetful functors.
equiv⇒proset : ∀{i j} -> equivs i j ⇒ prosets i j
proset⇒set : ∀{i j} -> prosets i j ⇒ sets i
equiv⇒set : ∀{i j} -> equivs i j ⇒ sets i
equiv⇒proset = fun id; proset⇒set = fun ap; equiv⇒set = fun ap


-- Okay, we've done the minimum requisite category theory.
-- Now let's start doing some order theory.

-- op flips the ordering on a proset.
op : ∀{i j} -> prosets i j ≤ prosets i j
ap op A = Proset: (Obj A) (λ a b → Hom A b a) (ident A) (λ f g → compo A g f)
map op (fun f) = fun f

-- equality is an equivalence relation, the "discrete" one.
disc : ∀{i} -> sets i ⇒ equivs i i
ap disc A = Proset: A _≡_ Eq.refl Eq.trans , Eq.sym
map disc f = fun (Eq.cong f)

-- "everything is equivalent" is an equivalence relation, the "indiscrete" one.
indisc : ∀{i j} -> sets i ⇒ equivs i j
ap indisc A = Proset: A (λ a b → Lift ⊤) _ _ , _
map indisc f = Fun: f _

-- core is the induced equivalence of a proset, ie:
-- (x ≤ y : core A) iff (x ≤ y ∧ y ≤ x : A).
core : ∀{i j} -> prosets i j ⇒ equivs i j
ap core A = Proset: (Obj A) _↔_ (id , id) (λ { (f₁ , g₂) (f₂ , g₁) → f₁ ∙ f₂ , g₁ ∙ g₂ })
          , swap
  where instance -a = A
map core (fun f) = fun (Data.Product.map f f)

-- loc is the equivalence closure of a proset, ie: the smallest equivalence
-- relation ≡ such that if x ≤ y then x ≡ y.
loc : ∀{i j} -> prosets i j ⇒ equivs i (i ⊔ j)
ap loc A = Proset: (Obj A) _~_ (path-by id) path-compo , path-flip
  where instance -a = A
map loc (fun f) = fun (path-fold _ _ (path-by ∘ f) path-flip path-compo)


-- We've now considered five functors: op, disc, indisc, core, and loc. The
-- domains and codomains of these functors at first seem disparate:
--
--   op           : prosets ⇒ prosets
--   disc, indisc : sets    ⇒ equivs
--   core, loc    : prosets ⇒ equivs
--
-- However, we may forget this and regard them all as operating on prosets:
--
--   op                                 : prosets ⇒ prosets
--   proset⇒set • disc • equiv⇒proset   : prosets ⇒ prosets
--   proset⇒set • indisc • equiv⇒proset : prosets ⇒ prosets
--   core • equiv⇒proset                : prosets ⇒ prosets
--   loc  • equiv⇒proset                : prosets ⇒ prosets

Disc : ∀{i j} -> prosets i j ⇒ prosets i i
Disc = proset⇒set • disc • equiv⇒proset

Indisc : ∀{i j k} -> prosets i j ⇒ prosets i k
Indisc = proset⇒set • indisc • equiv⇒proset

Core : ∀{i j} -> prosets i j ⇒ prosets i j
Core = core • equiv⇒proset

Loc : ∀{i j} -> prosets i j ⇒ prosets i (i ⊔ j)
Loc = loc • equiv⇒proset


-- Back to category theory: let's establish some "natural transformations"
-- between these functors. The diagram of the natural transformations we'll
-- establish is roughly:
--
--     disc ---> core ---> id ----> loc ---> indisc
--                   \            ↗
--                    \--> op ---/
--
--
-- As befits our wild, lawless Prosets and Funs, a "natural transformation" η
-- simply takes (f : A → B) and returns a diagonal (ηf : FA → GB) of the
-- assumed-to-be-commuting square:
--
--   FA --Ff-→ FB
--   |         |
--   ηA        ηB
--   ↓         ↓
--   GA --Gf-→ GB
--
-- To recover ηA, simply apply η to (id : A → A).
Transform : ∀{i j k l A B} (F G : Fun {i}{j}{k}{l} A B) -> Set _
Transform {A = A}{B = B} F G = ∀{a b} (f : Hom A a b) -> Hom B (ap F a) (ap G b)

funs : ∀ {i j k l} (A : Proset i j) (B : Proset k l) -> Proset _ _
funs A B .Obj = Fun A B
funs A B .Hom = Transform
funs A B .ident {F} = map F
funs A B .compo F≤G G≤H a≤b = compo B (F≤G (ident A)) (G≤H a≤b)
instance -funs = λ {i}{j}{k}{l}{A}{B} -> funs {i}{j}{k}{l} A B

disc→core : ∀{i} -> Disc {i} ≤ Core
disc→core {i}{A}{B} (Fun: F _) = Fun: F (λ { Eq.refl → ident B , ident B })

core→id : ∀{i j} -> Core {i}{j} ≤ id
core→id (fun f) = fun (proj₁ ∙ f)

core→op : ∀{i}{j} -> Core {i}{j} ≤ op
core→op (fun f) = fun (proj₂ ∙ f)

id→loc : ∀{i j} -> id ≤ Loc {i}{i ⊔ j}
id→loc (Fun: F f) = Fun: F (f ∙ path-by)

op→loc : ∀{i j} -> op ≤ Loc {i}{i ⊔ j}
op→loc (Fun: F f) = Fun: F (f ∙ path-by ∙ path-flip)

loc→indisc : ∀{i} -> Loc {i}{i} ≤ Indisc
loc→indisc (Fun: F _) = Fun: F (λ _ → lift tt)


-- More category theory: adjoint triples! As it turns out,
--
--     disc ⊣ equiv⇒set    ⊣ indisc
--     loc  ⊣ equiv⇒proset ⊣ core
--
-- Viewing {disc, indisc, loc, core} as functors prosets ⇒ prosets, this means
-- that disc & core are comonads, indisc & loc are monads, and moreover
-- (disc ⊣ indisc) and (loc ⊣ core).

-- "F ⊣ G" means "Fa ≤ b iff a ≤ Gb"; a Galois connection, or lawless
-- adjunction.
infix 4 _⊣_
record _⊣_ {i j k l A B} (F : Fun {i}{j}{k}{l} A B) (G : B ⇒ A) : Set (i ⊔ j ⊔ k ⊔ l) where
  constructor adjoint
  private instance -A = A; -B = B
  field l→r : ∀{a b} -> ap F a ≤ b → a ≤ ap G b
  field r→l : ∀{a b} -> a ≤ ap G b → ap F a ≤ b

  -- As usual, no coherence laws. We can construct the unit/counit, however:
  ε : G • F ≤ id; η : id ≤ F • G
  ε a≤b = r→l (map G a≤b); η a≤b = l→r (map F a≤b)

open _⊣_ public

-- Now let's show disc ⊣ forget ⊣ indisc. Since we're doing order theory, not
-- equivalence/groupoid theory, I'm going to consider {disc,indisc} as taking
-- sets ⇒ prosets rather than sets ⇒ equivs. This will be convenient later.
disc⊣forget : ∀{i} -> disc {i} • equiv⇒proset ⊣ proset⇒set
l→r disc⊣forget = ap
r→l disc⊣forget {A}{B} f = Fun: f (λ { Eq.refl → ident B })

forget⊣indisc : ∀{i j} -> proset⇒set ⊣ indisc {i}{j} • equiv⇒proset
forget⊣indisc = adjoint (λ f → Fun: f _) ap

-- Likewise, loc ⊣ forget ⊣ core.
loc⊣forget : ∀{j i} -> loc {i}{i ⊔ j} ⊣ equiv⇒proset
l→r loc⊣forget (fun f) = fun (path-by ∙ f)
r→l loc⊣forget {A} {B , Bs} (fun f) = fun (path-fold _ _ f Bs (compo B))

forget⊣core : ∀{i j} -> equiv⇒proset ⊣ core {i}{j}
l→r forget⊣core {A , A-sym} (fun f) = fun < f , A-sym ∙ f >
r→l forget⊣core (fun f) = fun (f ∙ proj₁)

-- Here's some general abstract nonsense we'll be making use of in a moment: An
-- adjoint triple gives rise to a pair of adjoint pairs.
module _ {i j k l} {A : Proset i j} {B : Proset k l}
         {F : A ⇒ B} {G : B ⇒ A} {H : A ⇒ B}
         (F⊣G : F ⊣ G) (G⊣H : G ⊣ H)
 where
  triple→pair-l : F • G ⊣ H • G
  l→r triple→pair-l = l→r F⊣G ∘ l→r G⊣H
  r→l triple→pair-l = r→l G⊣H ∘ r→l F⊣G

  triple→pair-r : G • F ⊣ G • H
  l→r triple→pair-r = l→r G⊣H ∘ l→r F⊣G
  r→l triple→pair-r = r→l F⊣G ∘ r→l G⊣H

-- Now, the adjunctions disc ⊣ indisc & loc ⊣ core fall out of the triple
-- adjunctions we've just proven. (This is why earlier, we treated {disc,indisc}
-- as sets ⇒ prosets, not sets ⇒ equivs; otherwise, this wouldn't typecheck.)
disc⊣indisc : ∀{i} -> Disc {i}{i} ⊣ Indisc {i}{i}
disc⊣indisc = triple→pair-r disc⊣forget forget⊣indisc

loc⊣core : ∀{j i} -> Loc {i}{i ⊔ j} ⊣ Core {i}{i ⊔ j}
loc⊣core {j} = triple→pair-l (loc⊣forget {j}) forget⊣core

-- Because of Agda Level nonsense, the type of disc⊣indisc isn't as general as
-- it could be. So, here are direct definitions of disc⊣indisc and loc⊣core.
-- Happily, these also give a bit of insight into what's really going on in
-- these adjunctions.
Disc⊣Indisc : ∀{i}{j} -> Disc {i}{j} ⊣ Indisc
l→r Disc⊣Indisc F = Fun: (ap F) _
r→l Disc⊣Indisc {A}{B} F = Fun: (ap F) (λ { Eq.refl → ident B })

-- This is probably the most interesting proof in this file.
Loc⊣Core : ∀{i j} -> Loc {i}{i ⊔ j} ⊣ Core {i}{i ⊔ j}
l→r Loc⊣Core F = fun (path-by ∙ < map F , path-flip ∙ map F >)
r→l Loc⊣Core {A}{B} (Fun: F f) = fun (proj₁ ∘ path-fold A (_≤_ on F) f swap _∙_)
  where instance Bcore = ap Core B