open import Cat.Instances.StrictCat
open import Cat.Instances.Functor
open import Cat.Functor.Adjoint
open import Cat.Functor.Base
open import Cat.Prelude
open import Cat.Thin

open import Data.Set.Coequaliser

module Cat.Thin.Completion where

Poset completion🔗

We construct a universal completion of a proset to a poset. Initially, recall the terms. A proset (which is how we refer to strict, thin categories) is a set equipped with a relation - \le - which is both reflexive and transitive, but not necessarily antisymmetric. A poset augments this with the requirement that \le is antisymmetric: It’s a univalent thin category.

The construction is conceptually straightforward: The poset completion of C\ca{C}, written C^\widehat{\ca{C}}, will have an underlying set of objects C^0\widehat{\ca{C}}_0 given by a quotient of C0\ca{C}_0 by the relation (xy)(yx)(x \le y) \land (y \le x). Essentially, we will forcibly “throw in” all of the missing antisymmetries.

module Poset-completion {o h} (C : Proset o h) where
  module C = Proset C

    _~_ : C.Ob  C.Ob  Type _
    x ~ y = C.Hom x y × C.Hom y x

  Ob′ : Type (o  h)
  Ob′ = C.Ob / _~_

However, showing that we can lift \le from the proset C\ca{C} to its completion C^\widehat{\ca{C}} is much harder than it should be. We start by showing that, assuming that xyx \le y and yxy \le x, we have equalities (xa)=(ya)(x \le a) = (y \le a) and (xa)=(ya)(x \le a) = (y \le a). These are given by propositional extensionality and pre/post composition with the assumed inequalities:

  private abstract
    p1 : (a : C.Ob) ((x , y , r) : Σ[ x  C.Ob ] Σ[ y  C.Ob ] x ~ y)
       Path (Prop h) (C.Hom x a , C.Hom-is-prop x a) (C.Hom y a , C.Hom-is-prop y a)
    p1 a (x , y , f , g) =
      n-ua (prop-ext (C.Hom-is-prop _ _) (C.Hom-is-prop _ _)  h  h C.∘ g)  h  h C.∘ f))

    p2 : (a : C.Ob) ((x , y , r) : Σ[ x  C.Ob ] Σ[ y  C.Ob ] x ~ y)
       Path (Prop h) (C.Hom a x , C.Hom-is-prop a x) (C.Hom a y , C.Hom-is-prop a y)
    p2 a (x , y , f , g) =
      n-ua (prop-ext (C.Hom-is-prop _ _) (C.Hom-is-prop _ _)  h  f C.∘ h)  h  g C.∘ h))

We can then eliminate from our quotient to the type of propositions. This is because we’re trying to define a type which is a proposition, but we can’t directly eliminate into Type, since set-quotients only let you eliminate into sets. By the equalities above, the map x,y(xy)x, y \mapsto (x \le y) respects the quotient, hence Hom′ below exists:

  Hom′ : Ob′  Ob′  Prop _
  Hom′ = Coeq-rec₂ (n-Type-is-hlevel 1)  x y  C.Hom x y , C.Hom-is-prop x y) p1 p2

  Hom′-prop :  (x y : Ob′) (f g :  Hom′ x y )  f  g
  Hom′-prop x y f g = Hom′ x y .is-tr f g

We can now prove that Hom′ is reflexive, transitive and antisymmetric. We get these by elimination on the domains/codomains of the map:

  id′ :  x   Hom′ x x 
  id′ = Coeq-elim-prop  x  Hom′ x x .is-tr)  _

  trans′ :  x y z   Hom′ x y    Hom′ y z    Hom′ x z 
  trans′ = Coeq-elim-prop₃
     x _ z  fun-is-hlevel 1 (fun-is-hlevel 1 (Hom′ x z .is-tr)))
     _ _ _ f g  g C.∘ f)

  antisym′ :  x y   Hom′ x y    Hom′ y x   x  y
  antisym′ = Coeq-elim-prop₂
     x y  hlevel 1)
     x y f g  quot (f , g))

The data above cleanly defines a Poset, so we’re done!

  completed : Poset (o  h) h
  completed = make-poset {A = Ob′} {R = λ x y   Hom′ x y }
       {x}  id′ x)
       {x} {y} {z}  trans′ x y z)
       {x} {y}  antisym′ x y)
       {x} {y}  Hom′ x y .is-tr)

open Poset-completion
  renaming (completed to Poset-completion)
  hiding (Ob′ ; Hom′ ; Hom′-prop ; trans′ ; antisym′ ; id′)


There is a functor between the underlying category of a proset C\ca{C} and the underlying category of its completion C^\widehat{\ca{C}}, with object part given by the quotient map inc.

Complete :  {o h} {X : Proset o h}
          Functor (X .underlying) (Poset-completion X .underlying)
Complete .F₀ = inc
Complete .F₁ x = x
Complete .F-id = refl
Complete .F-∘ f g = refl

This functor has morphism part given by the identity function, so it’s fully faithful. It exhibits C\ca{C} as a full subproset of C^\widehat{\ca{C}}.

  :  {o h} {X : Proset o h}  is-fully-faithful (Complete {X = X})
Complete-is-fully-faithful = id-equiv

Lifting functors🔗

We prove that any functor F:XYF : \ca{X} \to \ca{Y} lifts to a functor F^:X^Y^\widehat{F} : \widehat{\ca{X}} \to \widehat{\ca{Y}} between the respective poset completions. The hardest part of the construction is showing that F0F_0, i.e. the action of FF on the objects of X\ca{X}, respects the quotient which defines X^\widehat{\ca{X}}.

module _
  {o h} (X Y : Proset o h)
  (F : Functor (X .underlying) (Y .underlying))

    module X′ = Poset (Poset-completion X)
    module Y′ = Poset (Poset-completion Y)

Fortunately, even this is not very hard: It suffices to show that if x<yx < y and y<xy < x, then f(x)<f(y)f(x) < f(y) and f(y)<f(x)f(y) < f(x). But this is immediate by monotonicity of FF.

    F′₀ : X′.Ob  Y′.Ob
    F′₀ = Coeq-rec Y′.Ob-is-set
       x  inc (F₀ F x))
       (_ , _ , f , g)  quot (F₁ F f , F₁ F g))

The rest of the data of a functor is immediate by induction on quotients. It’s given by lifting the functor data from FF to the quotient, but it is quite annoying to convince Agda that this is a legal move.

    F′₁ : (a b : X′.Ob)  X′.Hom a b  Y′.Hom (F′₀ a) (F′₀ b)
    F′₁ = Coeq-elim-prop₂
       a b  fun-is-hlevel 1 (Y′.Hom-is-prop (F′₀ a) (F′₀ b)))
       _ _  F₁ F)

      F′₁-id :  (a : X′.Ob)  F′₁ a a (X′.id {a})  Y′.id {F′₀ a}
      F′₁-id = Coeq-elim-prop
         a  Y′.Hom-set (F′₀ a) (F′₀ a) _ _)
         a  F-id F)

      F′₁-∘ :  (x y z : X′.Ob) (f : X′.Hom y z) (g : X′.Hom x y)
             F′₁ x z (X′._∘_ {x} {y} {z} f g)
             Y′._∘_ {F′₀ x} {F′₀ y} {F′₀ z} (F′₁ y z f) (F′₁ x y g)
      F′₁-∘ =
           x y z 
            Π-is-hlevel 1 λ f 
            Π-is-hlevel 1 λ g 
            Y′.Hom-set (F′₀ x) (F′₀ z) _ _)
          λ x y z f g  F-∘ F f g

This defines a map between the completions of X\ca{X} and Y\ca{Y}:

  Poset-completion-embedding : Functor X′.underlying Y′.underlying
  Poset-completion-embedding .F₀               = F′₀
  Poset-completion-embedding .F₁   {x} {y}     = F′₁ x y
  Poset-completion-embedding .F-id {x}         = F′₁-id x
  Poset-completion-embedding .F-∘  {x} {y} {z} = F′₁-∘ x y z