Tom de Jong, 3 June 2022

The poset reflection of a preorder, using (large) set quotients as constructed
in Quotient.Large.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Subsingletons
open import UF.SubtypeClassifier

module OrderedTypes.PosetReflection
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
       where

open import Quotient.Type
open import Quotient.Large pt fe pe
open import UF.Base hiding (_β‰ˆ_)
open import UF.ImageAndSurjection pt
open import UF.Subsingletons-FunExt

open general-set-quotients-exist large-set-quotients
open extending-relations-to-quotient fe pe

module poset-reflection
        (X : 𝓀 Μ‡ )
        (_≲_ : X β†’ X β†’ 𝓣 Μ‡ )
        (≲-is-prop-valued : (x y : X) β†’ is-prop (x ≲ y))
        (≲-is-reflexive : (x : X) β†’ x ≲ x)
        (≲-is-transitive : (x y z : X) β†’ x ≲ y β†’ y ≲ z β†’ x ≲ z)
       where

 private
  _≲Ω_ : X β†’ X β†’ Ξ© 𝓣
  x ≲Ω y = x ≲ y , ≲-is-prop-valued x y

 _β‰ˆ_ : X β†’ X β†’ 𝓣 Μ‡
 x β‰ˆ y = x ≲ y Γ— y ≲ x

 β‰ˆ-is-equiv-rel : is-equiv-relation _β‰ˆ_
 β‰ˆ-is-equiv-rel = (Ξ» x y β†’ Γ—-is-prop (≲-is-prop-valued x y)
                                     (≲-is-prop-valued y x))
                , (Ξ» x β†’ ≲-is-reflexive x , ≲-is-reflexive x)
                , (Ξ» x y (k , l) β†’ l , k)
                , (Ξ» x y z (k , l) (u , v) β†’ (≲-is-transitive x y z k u)
                                           , (≲-is-transitive z y x v l))

 ≋ : EqRel X
 ≋ = _β‰ˆ_ , β‰ˆ-is-equiv-rel

 private
  ≲-congruence : {x y x' y' : X} β†’ x β‰ˆ x' β†’ y β‰ˆ y' β†’ x ≲Ω y ＝ x' ≲Ω y'
  ≲-congruence {x} {y} {x'} {y'} (k , l) (u , v) =
   Ξ©-extensionality pe fe
    (Ξ» m β†’ ≲-is-transitive x' x y' l
            (≲-is-transitive x y y' m u))
    (Ξ» m β†’ ≲-is-transitive x x' y k
            (≲-is-transitive x' y' y m v))

  _≀Ω_ : X / ≋ β†’ X / ≋ β†’ Ξ© 𝓣
  _≀Ω_ = extension-relβ‚‚ ≋ (Ξ» x y β†’ x ≲Ω y) ≲-congruence

 poset-reflection-carrier : 𝓣 ⁺ βŠ” 𝓀 Μ‡
 poset-reflection-carrier = X / ≋

 poset-reflection-is-set : is-set poset-reflection-carrier
 poset-reflection-is-set = /-is-set ≋

 _≀_ : X / ≋ β†’ X / ≋ β†’ 𝓣 Μ‡
 x' ≀ y' = (x' ≀Ω y') holds

 ≀-is-prop-valued : (x' y' : X / ≋) β†’ is-prop (x' ≀ y')
 ≀-is-prop-valued x' y' = holds-is-prop (x' ≀Ω y')

 Ξ· : X β†’ X / ≋
 Ξ· = Ξ·/ ≋

 Ξ·-is-surjection : is-surjection Ξ·
 Ξ·-is-surjection = Ξ·/-is-surjection ≋ pt

 Ξ·-reflects-order : {x y : X} β†’ Ξ· x ≀ Ξ· y β†’ x ≲ y
 Ξ·-reflects-order {x} {y} =
  Idtofun (ap pr₁ (extension-rel-triangleβ‚‚ ≋ _≲Ω_ ≲-congruence x y))

 Ξ·-preserves-order : {x y : X} β†’ x ≲ y β†’ Ξ· x ≀ Ξ· y
 Ξ·-preserves-order {x} {y} =
  Idtofun (ap pr₁ ((extension-rel-triangleβ‚‚ ≋ _≲Ω_ ≲-congruence x y) ⁻¹))

 Ξ·-↔-order : {x y : X} β†’ x ≲ y ↔ Ξ· x ≀ Ξ· y
 Ξ·-↔-order = Ξ·-preserves-order , Ξ·-reflects-order

 ≀-is-reflexive : (x' : X / ≋) β†’ x' ≀ x'
 ≀-is-reflexive = /-induction ≋ (Ξ» x' β†’ ≀-is-prop-valued x' x')
                                (Ξ» x β†’ Ξ·-preserves-order (≲-is-reflexive x))

 ≀-is-transitive : (x' y' z' : X / ≋) β†’ x' ≀ y' β†’ y' ≀ z' β†’ x' ≀ z'
 ≀-is-transitive =
  /-induction₃ fe ≋ (Ξ» x' y' z' β†’ Ξ β‚‚-is-prop fe (Ξ» _ _ β†’ ≀-is-prop-valued x' z'))
                    (Ξ» x y z k l β†’ Ξ·-preserves-order
                                    (≲-is-transitive x y z
                                      (Ξ·-reflects-order k)
                                      (Ξ·-reflects-order l)))

 ≀-is-antisymmetric : (x' y' : X / ≋) β†’ x' ≀ y' β†’ y' ≀ x' β†’ x' ＝ y'
 ≀-is-antisymmetric =
  /-inductionβ‚‚ fe ≋ (Ξ» x' q β†’ Ξ β‚‚-is-prop fe (Ξ» _ _ β†’ /-is-set ≋))
                    (Ξ» x y k l β†’ Ξ·/-identifies-related-points ≋
                                  ( Ξ·-reflects-order k
                                  , Ξ·-reflects-order l))

\end{code}

The requirement that Q is a set actually follows from the order assumptions, but
it is convenient to assume it (for now) anyway.

\begin{code}

 universal-property :
    {Q : 𝓀' Μ‡ } (_βŠ‘_ : Q β†’ Q β†’ 𝓣' Μ‡ )
  β†’ is-set Q
  β†’ ((p q : Q) β†’ is-prop (p βŠ‘ q))
  β†’ ((q : Q) β†’ q βŠ‘ q)
  β†’ ((p q r : Q) β†’ p βŠ‘ q β†’ q βŠ‘ r β†’ p βŠ‘ r)
  β†’ ((p q : Q) β†’ p βŠ‘ q β†’ q βŠ‘ p β†’ p ＝ q)
  β†’ (f : X β†’ Q)
  β†’ ((x y : X) β†’ x ≲ y β†’ f x βŠ‘ f y)
  β†’ βˆƒ! fΜƒ κž‰ (X / ≋ β†’ Q) , ((x' y' : X / ≋) β†’ x' ≀ y' β†’ fΜƒ x' βŠ‘ fΜƒ y')
                       Γ— (fΜƒ ∘ Ξ· ∼ f)
 universal-property {𝓀'} {𝓣'} {Q} _βŠ‘_ Q-is-set βŠ‘-prop βŠ‘-refl βŠ‘-trans
                                               βŠ‘-antisym f f-mon =
  (f̃ , f̃-mon , f̃-eq) , σ
   where
    ΞΌ : βˆƒ! fΜƒ κž‰ (X / ≋ β†’ Q), fΜƒ ∘ Ξ· ∼ f
    ΞΌ = /-universality ≋
         Q-is-set f (Ξ» {x} {y} (k , l) β†’ βŠ‘-antisym (f x) (f y)
                                          (f-mon x y k) (f-mon y x l))
    fΜƒ : X / ≋ β†’ Q
    fΜƒ = βˆƒ!-witness ΞΌ
    fΜƒ-eq : fΜƒ ∘ Ξ· ∼ f
    fΜƒ-eq = βˆƒ!-is-witness ΞΌ
    fΜƒ-mon : (x' y' : X / ≋) β†’ x' ≀ y' β†’ fΜƒ x' βŠ‘ fΜƒ y'
    fΜƒ-mon = /-inductionβ‚‚ fe ≋
             (Ξ» x' y' β†’ Ξ -is-prop fe (Ξ» _ β†’ βŠ‘-prop (fΜƒ x') (fΜƒ y')))
             (Ξ» x y l β†’ transportβ‚‚ _βŠ‘_ ((fΜƒ-eq x) ⁻¹) ((fΜƒ-eq y) ⁻¹)
                         (f-mon x y (Ξ·-reflects-order l)))
    fΜƒ-is-unique : (g : X / ≋ β†’ Q)
                β†’ ((x' y' : X / ≋) β†’ x' ≀ y' β†’ g x' βŠ‘ g y')
                β†’ (g ∘ Ξ· ∼ f)
                β†’ fΜƒ ∼ g
    f̃-is-unique g g-mon g-eq = happly e
     where
      e : fΜƒ ＝ g
      e = ap pr₁ (βˆƒ!-uniqueness' ΞΌ (g , g-eq))
    Οƒ : is-central (Ξ£ g κž‰ (X / ≋ β†’ Q)
                        , ((x' y' : X / ≋) β†’ x' ≀ y' β†’ g x' βŠ‘ g y')
                        Γ— g ∘ Ξ· ∼ f)
                   (f̃ , f̃-mon , f̃-eq)
    Οƒ (g , g-mon , g-eq) =
     to-subtype-＝ (Ξ» h β†’ Γ—-is-prop
                          (Π₃-is-prop fe (Ξ» x' y' _ β†’ βŠ‘-prop (h x') (h y')))
                          (Ξ -is-prop fe (Ξ» _ β†’ Q-is-set)))
                  (dfunext fe (f̃-is-unique g g-mon g-eq))

\end{code}