Tom de Jong, 24 January 2022
(Refactored from FreeJoinSemiLattice.lagda)

We define join-semilattices using a record. We also introduce convenient helpers
and syntax for reasoning about the order βŠ‘ and we construct finite joins using
the least element and binary joins.

\begin{code}

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

module OrderedTypes.JoinSemiLattices where

open import MLTT.Spartan
open import Fin.Type

open import UF.Subsingletons
open import UF.Sets

record JoinSemiLattice (π“₯ 𝓣 : Universe) : 𝓀ω where
  field
    L : π“₯ Μ‡
    L-is-set : is-set L
    _βŠ‘_ : L β†’ L β†’ 𝓣 Μ‡
    βŠ‘-is-prop-valued : (x y : L) β†’ is-prop (x βŠ‘ y)
    βŠ‘-is-reflexive : (x : L) β†’ x βŠ‘ x
    βŠ‘-is-transitive : (x y z : L) β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z
    βŠ‘-is-antisymmetric : (x y : L) β†’ x βŠ‘ y β†’ y βŠ‘ x β†’ x ＝ y
    βŠ₯ : L
    βŠ₯-is-least : (x : L) β†’ βŠ₯ βŠ‘ x
    _∨_ : L β†’ L β†’ L
    ∨-is-upperbound₁ : (x y : L) β†’ x βŠ‘ (x ∨ y)
    ∨-is-upperboundβ‚‚ : (x y : L) β†’ y βŠ‘ (x ∨ y)
    ∨-is-lowerbound-of-upperbounds : (x y z : L) β†’ x βŠ‘ z β†’ y βŠ‘ z β†’ (x ∨ y) βŠ‘ z

  transitivity' : (x : L) {y z : L}
                β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z
  transitivity' x {y} {z} = βŠ‘-is-transitive x y z

  syntax transitivity' x u v = x βŠ‘βŸ¨ u ⟩ v
  infixr 0 transitivity'

  reflexivity' : (x : L) β†’ x βŠ‘ x
  reflexivity' x = βŠ‘-is-reflexive x

  syntax reflexivity' x = x βŠ‘βˆŽ
  infix 1 reflexivity'

  ＝-to-βŠ‘ : {x y : L} β†’ x ＝ y β†’ x βŠ‘ y
  ＝-to-βŠ‘ {x} {x} refl = reflexivity' x

  ＝-to-βŠ’ : {x y : L} β†’ y ＝ x β†’ x βŠ‘ y
  ＝-to-βŠ’ p = ＝-to-βŠ‘ (p ⁻¹)

  ∨ⁿ : {n : β„•} β†’ (Fin n β†’ L) β†’ L
  ∨ⁿ {zero}   e = βŠ₯
  ∨ⁿ {succ m} e = (∨ⁿ (e ∘ suc)) ∨ (e 𝟎)

  ∨ⁿ-is-upperbound : {n : β„•} (Οƒ : Fin n β†’ L)
                   β†’ (k : Fin n) β†’ Οƒ k βŠ‘ ∨ⁿ Οƒ
  ∨ⁿ-is-upperbound {succ n} Οƒ 𝟎       = ∨-is-upperboundβ‚‚ _ _
  ∨ⁿ-is-upperbound {succ n} Οƒ (suc k) = Οƒ (suc k)    βŠ‘βŸ¨ IH ⟩
                                        ∨ⁿ (Οƒ ∘ suc) βŠ‘βŸ¨ ∨-is-upperbound₁ _ _ ⟩
                                        ∨ⁿ Οƒ         βŠ‘βˆŽ
   where
    IH = ∨ⁿ-is-upperbound (Οƒ ∘ suc) k

  ∨ⁿ-is-lowerbound-of-upperbounds : {n : β„•} (Οƒ : Fin n β†’ L)
                                    (x : L)
                                  β†’ ((k : Fin n) β†’ Οƒ k βŠ‘ x)
                                  β†’ ∨ⁿ Οƒ βŠ‘ x
  ∨ⁿ-is-lowerbound-of-upperbounds {zero}   Οƒ x ub = βŠ₯-is-least x
  ∨ⁿ-is-lowerbound-of-upperbounds {succ n} Οƒ x ub =
   ∨-is-lowerbound-of-upperbounds _ _ _ u v
    where
     u : ∨ⁿ (Οƒ ∘ suc) βŠ‘ x
     u = ∨ⁿ-is-lowerbound-of-upperbounds {n} (Οƒ ∘ suc) x (ub ∘ suc)
     v : Οƒ 𝟎 βŠ‘ x
     v = ub 𝟎

\end{code}