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 which is both reflexive and transitive, but not necessarily antisymmetric. A poset augments this with the requirement that is antisymmetric: Itβs a univalent thin category.
The construction is conceptually straightforward: The poset completion of , written , will have an underlying set of objects given by a quotient of by the relation . 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 from the proset to its completion is much harder than it should be. We start by showing that, assuming that and , we have equalities and . 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 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 and the underlying category of its completion , 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 as a full subproset of .
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 lifts to a functor between the respective poset completions. The hardest part of the construction is showing that , i.e.Β the action of on the objects of , respects the quotient which defines .
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 and , then and . But this is immediate by monotonicity of .
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 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 and :
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