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 (x≀y)∧(y≀x)(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

  private
    _~_ : 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 x≀yx \le y and y≀xy \le x, we have equalities (x≀a)=(y≀a)(x \le a) = (y \le a) and (x≀a)=(y≀a)(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) (el (C.Hom x a) (C.Hom-is-prop x a)) (el (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) (el (C.Hom a x) (C.Hom-is-prop a x)) (el (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↦(x≀y)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 β†’ el (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) (Ξ» _ β†’ C.id)

  transβ€² : βˆ€ x y z β†’ ∣ Homβ€² x y ∣ β†’ ∣ Homβ€² y z ∣ β†’ ∣ Homβ€² x z ∣
  transβ€² = Coeq-elim-prop₃
    (Ξ» x _ z β†’ hlevel!)
    (Ξ» _ _ _ 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β€²)

EmbeddingπŸ”—

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}}.

Complete-is-fully-faithful
  : βˆ€ {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:X→YF : \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))
  where

  private
    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 β†’ hlevel!)
      (Ξ» _ _ β†’ F₁ F)

    abstract
      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′₁-∘ =
        Coeq-elim-prop₃
          (Ξ» x y z β†’ hlevel!)
          Ξ» 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