open import Cat.Instances.Sets
open import Cat.Functor.Base
open import Cat.Prelude

open import Order.Morphism
open import Order.Base

import Cat.Reasoning

module Order.Univalent where

Univalence of the category of PosetsπŸ”—

This module proves that the category of posets is actually univalent. As usual, we begin by constructing a function that constructs an identification from an isomorphism; this is the most tedious part of the argument.

Poset-path : βˆ€ {o β„“} {P Q : Poset o β„“} β†’ P Posets.β‰… Q β†’ P ≑ Q
Poset-path {P = P} {Q} f = path where

  module P = Poset P
  module Q = Poset Q
  open Posets

Since the forgetful functor maps isomorphisms of posets onto isomorphisms of their underlying sets, the first thing to observe is that an isomorphism of posets has an underlying equivalence of types, from which we can construct a path, by univalence.

  P≃Q : ⌞ P ⌟ ≃ ⌞ Q ⌟
  P≃Q = isoβ†’equiv (F-map-iso Posetsβ†ͺSets f)

  ob : βˆ€ i β†’ Type _
  ob i = ua P≃Q i

That handles the first field of the record Poset. The next thing to consider is the order relation. We’re looking for a term of the following type:

  order : PathP (Ξ» i β†’ ob i β†’ ob i β†’ Type _) P._≀_ Q._≀_

That is, an identification between the order relations, which is displayed over the identification between underlying sets we just constructed. We do this by an explicit cubical construction. It will suffice to construct a term

which reduces to when (resp. when We begin by observing that, since are inhabitants of a Glue type, we can unglue them to obtain values Moreover, these unglued values reduce to on and on We can arrange the data at hand and the data we want as the top and bottom faces in a square:

We can then obtain the dashed face β€” as well as the full square β€” again using a Glue type, as long as we can fill the missing faces by equivalences. And since the missing left-hand-side is precisely the statement β€œ is an order-embedding”, we can:

  order i x y = Glue (unglue (βˆ‚ i) x Q.≀ unglue (βˆ‚ i) y) Ξ» where
    (i = i0) β†’ x P.≀ y , order-iso-is-order-embedding f
    (i = i1) β†’ x Q.≀ y , _ , id-equiv

The definition above corresponds to the top face in the square

  order-thin : βˆ€ i x y β†’ is-prop (order i x y)
  order-thin i = coe0β†’i (Ξ» i β†’ (x y : ob i) β†’ is-prop (order i x y)) i (Ξ» _ _ β†’ hlevel 1)

  ob-set : βˆ€ i β†’ is-set (ob i)
  ob-set i = coe0β†’i (Ξ» i β†’ is-set (ob i)) i (hlevel 2)

  path : P ≑ Q
  path i .Poset.Ob      = ob i
  path i .Poset._≀_ x y = order i x y
That handles the fields with actual content. All the proposition-valued fields are entirely formulaic applications of is-prop→pathp, so we omit them from the page for space. 
  path i .Poset.≀-thin {x} {y} =
    is-prop→pathp
      (Ξ» i β†’
        Ξ -is-hlevelΒ² {A = ob i} {B = Ξ» _ β†’ ob i} 1 Ξ» x y β†’
        is-prop-is-prop {A = order i x y})
      (Ξ» _ _ β†’ P.≀-thin)
      (Ξ» _ _ β†’ Q.≀-thin) i x y
  path i .Poset.≀-refl {x = x} =
    is-prop→pathp
      (Ξ» i β†’ Ξ -is-hlevel {A = ob i} 1 Ξ» x β†’ order-thin i x x)
        (Ξ» _ β†’ P.≀-refl)
        (Ξ» _ β†’ Q.≀-refl) i x
  path i .Poset.≀-trans {x} {y} {z} x≀y y≀z =
    is-prop→pathp
      (Ξ» i β†’
        Ξ -is-hlevelΒ³ {A = ob i} {B = Ξ» _ β†’ ob i} {C = Ξ» _ _ β†’ ob i} 1 Ξ» x y z β†’
        Ξ -is-hlevelΒ² {A = order i x y} {B = Ξ» _ β†’ order i y z} 1 Ξ» _ _ β†’
        order-thin i x z)
      (Ξ» _ _ _ β†’ P.≀-trans)
      (Ξ» _ _ _ β†’ Q.≀-trans) i x y z x≀y y≀z
  path i .Poset.≀-antisym {x} {y} x≀y y≀x =
    is-prop→pathp
      (Ξ» i β†’
        Ξ -is-hlevelΒ² {A = ob i } {B = Ξ» _ β†’ ob i} 1 Ξ» x y β†’
        Ξ -is-hlevelΒ² {A = order i x y} {B = Ξ» _ β†’ order i y x} 1 Ξ» _ _ β†’
        ob-set i x y)
      (Ξ» _ _ β†’ P.≀-antisym)
      (Ξ» _ _ β†’ Q.≀-antisym) i x y x≀y y≀x

It remains to prove that this construction is coherent: given an isomorphism we’ve recovered a path over which we can compare isomorphisms with isomorphisms The necessary coherence datum says that, over the identity becomes 

Posets-is-category : βˆ€ {o β„“} β†’ is-category (Posets o β„“)
Posets-is-category .to-path        = Poset-path
Posets-is-category .to-path-over f = Posets.β‰…-pathp _ _ $
  Monotone-pathp $ funextP λ x → path→ua-pathp _ refl