open import Cat.Instances.StrictCat
open import Cat.Instances.Functor
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 $\ca{C}$, written $\widehat{\ca{C}}$, will have an underlying set of objects $\widehat{\ca{C}}_0$ given by a quotient of $\ca{C}_0$ by the relation $(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 $\ca{C}$ to its completion $\widehat{\ca{C}}$ is much harder than it should be. We start by showing that, assuming that $x \le y$ and $y \le x$, we have equalities $(x \le a) = (y \le a)$ and $(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 \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) (Ξ» _ β C.id)

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β²)


## Embeddingπ

There is a functor between the underlying category of a proset $\ca{C}$ and the underlying category of its completion $\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 $\ca{C}$ as a full subproset of $\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 : \ca{X} \to \ca{Y}$ lifts to a functor $\widehat{F} : \widehat{\ca{X}} \to \widehat{\ca{Y}}$ between the respective poset completions. The hardest part of the construction is showing that $F_0$, i.e.Β the action of $F$ on the objects of $\ca{X}$, respects the quotient which defines $\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 < y$ and $y < x$, then $f(x) < f(y)$ and $f(y) < f(x)$. But this is immediate by monotonicity of $F$.

    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 $F$ 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)

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 β
Ξ -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 $\ca{X}$ and $\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