open import Cat.Instances.StrictCat
open import Cat.Instances.Functor
open import Cat.Prelude

open import Data.Set.Coequaliser

import Cat.Reasoning
import Cat.Univalent

module Cat.Thin where


# Thin categories🔗

A category is called thin if all of its hom-sets are propositions rather than sets. Furthermore, we require that the space of objects be a set; In other words, a thin category is necessarily strict.

record is-thin (C : Precategory o h) : Type (o ⊔ h) where
no-eta-equality
open Precategory C
field
Ob-is-set : is-set Ob
Hom-is-prop : ∀ A B → is-prop (Hom A B)


To avoid Agda record weirdness, we package is-thin into a convenient packaged record together with the underlying category.

record Proset (o h : Level) : Type (lsuc (o ⊔ h)) where
no-eta-equality
field
{underlying} : Precategory o h
has-is-thin  : is-thin underlying

open import Cat.Reasoning underlying public
open is-thin has-is-thin public

_≤_ : Ob → Ob → Type h
_≤_ = Hom


The collection of all thin categories assembles into a subcategory of Strict-Cat, which we call Proset.

Prosets : ∀ o h → Precategory (lsuc (o ⊔ h)) (o ⊔ h)
Prosets o h = proset where
open Precategory
open Proset

proset : Precategory _ _
proset .Ob = Proset o h
proset .Hom C D = Functor (C .underlying) (D .underlying)
proset .Hom-set _ D = Functor-is-set (D .Ob-is-set)
proset .id = Id
proset ._∘_ = _F∘_
proset .idr f = Functor-path (λ _ → refl) λ _ → refl
proset .idl f = Functor-path (λ _ → refl) λ _ → refl
proset .assoc f g h = Functor-path (λ _ → refl) λ _ → refl


We also have a convenience function for making any set with a preorder into a ThinCat.

module _ where
open Proset

make-proset : ∀ {ℓ ℓ'} {A : Type ℓ} {R : A → A → Type ℓ'}
→ is-set A
→ (∀ {x} → R x x)
→ (∀ {x y z} → R x y → R y z → R x z)
→ (∀ {x y} → is-prop (R x y))
→ Proset ℓ ℓ'
make-proset {A = A} {R} Aset Rrefl Rtrans Rprop = tc where
open Precategory

tc : Proset _ _
tc .underlying .Ob          = A
tc .underlying .Hom         = R
tc .underlying .Hom-set _ _ = is-prop→is-set Rprop
tc .underlying .id          = Rrefl
tc .underlying ._∘_ f g     = Rtrans g f
tc .underlying .idr f       = Rprop _ _
tc .underlying .idl f       = Rprop _ _
tc .underlying .assoc f g h = Rprop _ _

tc .has-is-thin .is-thin.Ob-is-set = Aset
tc .has-is-thin .is-thin.Hom-is-prop A B x y = Rprop x y


# Posets🔗

We refer to a [univalent] thin category as a poset, short for partially-ordered set. Recall that a category $\ca{C}$ is univalent when the type $\sum_{(B : \ca{C})} A \cong B$ is contractible for any fixed $A : \ca{C}$ or (more useful here) we have a function $\id{iso→path} : A \cong B \to A \equiv B$ sending the identity isomorphism to refl.

In a thin category, any pair of maps $(A \to B) \times (B \to A)$ is an isomorphism, so in effect we have a map $(A \to B) \times (B \to A) \to (A \equiv B)$: If a thin category is a preordered set, then a univalent thin category is a partially ordered set.

record Poset (o h : Level) : Type (lsuc (o ⊔ h)) where
no-eta-equality
field
{underlying}     : Precategory o h
has-is-thin      : is-thin underlying
has-is-univalent : is-category underlying

open Precategory underlying
using ( Ob ; Hom ; Hom-set ; id ; _∘_ ; idl ; idr ; assoc ) public
open is-thin has-is-thin public

open import Cat.Univalent underlying
module HLevel-instance where
instance
H-Level-Hom : ∀ {x y} {n} → H-Level (Hom x y) (suc n)
H-Level-Hom = prop-instance (Hom-is-prop _ _)


Since posets are most commonly considered in the context of order theory, we abbreviate their $\hom$-props by $(a \le b)$. Similarly, we rename the identity, composition and univalence operations to order-theoretic names.

  _≤_ : Ob → Ob → Type h
_≤_ = Hom

reflexive : ∀ {x} → x ≤ x
reflexive = id

transitive : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
transitive f g = g ∘ f


Any pair of opposing morphisms in a proset (thus in a poset) gives an isomorphism. The “inversion” equations hold by thinness: Since $(f \circ g) : A \le A$, then it must be equal to reflexive above.

  antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≡ y
antisym f g = iso→path has-is-univalent
(record
{ to = f
; from = g
; inverses = record
{ invl = Hom-is-prop _ _ _ _ ; invr = Hom-is-prop _ _ _ _ } })


Forgetting the univalence datum lets us turn a Poset into a Proset.

  →Proset : Proset o h
→Proset .Proset.underlying = underlying
→Proset .Proset.has-is-thin  = has-is-thin


## Making posets🔗

Rijke’s theorem says that any type equipped with a reflexive relation $x \sim y$ which implies $x \equiv y$ is automatically a set. If $x \le y$ is a reflexive, antisymmetric relation, we can take the relation $x \sim y = (x \le y) \land (y \le x)$, which is evidently reflexive and, by antisymmetry, implies $x \equiv y$.

module _ where
open Poset

make-poset : ∀ {ℓ ℓ'} {A : Type ℓ} {R : A → A → Type ℓ'}
→ (∀ {x} → R x x)
→ (∀ {x y z} → R x y → R y z → R x z)
→ (∀ {x y} → R x y → R y x → x ≡ y)
→ (∀ {x y} → is-prop (R x y))
→ Poset ℓ ℓ'


Thus, to make a poset, it suffices to have a type $A$ (any old type!), a relation on $R$, and witnesses of reflexivity, transitivity, and antisymmetry. We derive that $A$ is a set using Rijke’s theorem as described above, and prove that any antisymmetric proset is univalent.

  make-poset {A = A} {R} Rrefl Rtrans Rantisym Rprop = tc where
abstract
Aset : is-set A
Aset = Rijke-is-set {R = λ x y → R x y × R y x}
(Rrefl , Rrefl)
(λ (f , g) → Rantisym f g)
λ x y i → Rprop (x .fst) (y .fst) i , Rprop (x .snd) (y .snd) i

open Proset (make-proset Aset Rrefl Rtrans Rprop)
renaming ( underlying to cat ; has-is-thin to ist )

tc : Poset _ _
tc .underlying = cat
tc .has-is-thin  = ist


For the centre of contraction, we take $A$ and the identity isomorphism. Then, assume that we have some other object $B$ equipped with an iso $i : A \cong B$. Since an iso is a big conjunction of propositional components, it’s a proposition, so it suffices to show $A \equiv B$. But from the iso we have $(A \le B) \land (B \le A)$, and antisymmetry finishes the job.

    tc .has-is-univalent A .centre        = A , id-iso
tc .has-is-univalent A .paths (B , i) = Σ-prop-path isp (Rantisym i.to i.from) where
module i = _≅_ i
abstract
isp : ∀ x → is-prop (A ≅ x)
isp ob x y i .to   = Rprop (x .to)   (y .to)   i
isp ob x y i .from = Rprop (x .from) (y .from) i
isp ob x y i .inverses =
is-prop→pathp
(λ i → Inverses-are-prop {f = Rprop (x .to)   (y .to)   i}
{g = Rprop (x .from) (y .from) i})
(x .inverses) (y .inverses) i


## Monotone maps🔗

Rather than considering functors between posets, we can consider monotone maps between them. This is because, since each hom-set is a proposition, the functor identities are automatically satisfied:

module _ where
open Poset

Monotone-map : Poset o h → Poset o′ h′ → Type _
Monotone-map C D = Functor (C .underlying) (D .underlying)

make-monotone-map
: (C : Poset o h) (D : Poset o′ h′)
→ (f : C .Ob → D .Ob)
→ (∀ x y → Hom C x y → Hom D (f x) (f y))
→ Monotone-map C D
make-monotone-map C D f ord .Functor.F₀ = f
make-monotone-map C D f ord .Functor.F₁ = ord _ _
make-monotone-map C D f ord .Functor.F-id = D .Hom-is-prop _ _ _ _
make-monotone-map C D f ord .Functor.F-∘ _ _ = D .Hom-is-prop _ _ _ _

open Precategory

Posets : ∀ o h → Precategory (lsuc (o ⊔ h)) (o ⊔ h)
Posets o h .Ob = Poset o h
Posets _ _ .Hom = Monotone-map
Posets _ _ .Hom-set _ d = Functor-is-set (d .Ob-is-set)
Posets _ _ .id = Id
Posets _ _ ._∘_ = _F∘_
Posets _ _ .idr f = Functor-path (λ _ → refl) λ _ → refl
Posets _ _ .idl f = Functor-path (λ _ → refl) λ _ → refl
Posets _ _ .assoc f g h = Functor-path (λ _ → refl) λ _ → refl


# Prosetal reflection🔗

There is an evident functor from $\prosets$ to $\strcat$ given by forgetting the thinness data. This functor is ff., since maps between prosets are functors between strict categories: it acts on morphisms literally by the identity function.

Forget : ∀ {o h} → Functor (Prosets o h) (Strict-Cat o h)
Forget .F₀ C = Proset.underlying C , Proset.Ob-is-set C
Forget .F₁ f = f
Forget .F-id = refl
Forget .F-∘ _ _ = refl


This functor begs the question: is it possible to freely turn a strict category into a proset? The answer is yes! We can propositionally truncate each of the $\hom$-sets. This provides a reflection of strict categories into prosets.

Free : ∀ {o h} → Functor (Strict-Cat o h) (Prosets o h)
Free .F₀ C = pro where
open Precategory

pro : Proset _ _
pro = make-proset {R = λ x y → ∥ C .fst .Hom x y ∥} (C .snd)
(inc (C .fst .id))
(∥-∥-elim₂ (λ _ _ → squash) λ f g → inc (C .fst ._∘_ g f))
squash


The Free proset functor takes a strict category on the proset obtained by truncating each of its hom-sets. This induced relation is reflexive (by including the identity map), and transitive (by lifting the composition map onto the truncation). On morphisms, it preserves the object part, and lifts the morphism action onto the truncations.

Free .F₁ F .F₀      = F₀ F
Free .F₁ F .F₁      = ∥-∥-map (F₁ F)
Free .F₁ F .F-id i  = inc (F-id F i)
Free .F₁ F .F-∘ _ _ = squash _ _
Free .F-id    = Functor-path (λ _ → refl) λ f → squash _ _
Free .F-∘ f g = Functor-path (λ _ → refl) λ f → squash _ _


This Free functor is a left adjoint to the Forget functor defined above, so in particular we conclude that it induces an idempotent monad on Strict-Cat: The “thinning” of a Proset is the same proset we started with.

Free⊣Forget : Free ⊣ Forget {o} {h}
Free⊣Forget .unit .η _ .F₀ x = x
Free⊣Forget .unit .η _ .F₁ = inc
Free⊣Forget .unit .η _ .F-id = refl
Free⊣Forget .unit .η _ .F-∘ f g = refl
Free⊣Forget .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → refl

Free⊣Forget .counit .η pro .F₀ x = x
Free⊣Forget .counit .η pro .F₁ = ∥-∥-elim (λ _ → pro .Proset.Hom-is-prop _ _) λ x → x
Free⊣Forget .counit .η pro .F-id = refl
Free⊣Forget .counit .η pro .F-∘ f g = pro .Proset.Hom-is-prop _ _ _ _
Free⊣Forget .counit .is-natural x y f =
Functor-path (λ _ → refl) λ f → y .Proset.Hom-is-prop _ _ _ _

Free⊣Forget .zig = Functor-path (λ _ → refl) λ _ → squash _ _
Free⊣Forget .zag = Functor-path (λ _ → refl) λ _ → refl


## Poset completions🔗

It’s also possible to freely turn a proset into a poset. We do this in a separate module: Cat.Thin.Completion.