---
title:         Properties of the way-below relation
author:        Ayberk Tosun
date-started:  2023-08-19
dates-updated: [2024-09-12]
---

The module contains properties of the way below relation defined in
`Locales.WayBelowRelation.Definition`.

\begin{code}[hide]

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

open import UF.PropTrunc
open import UF.FunExt
open import MLTT.Spartan
open import UF.Logic
open import UF.SubtypeClassifier
open import Slice.Family

module Locales.WayBelowRelation.Properties (pt : propositional-truncations-exist)
                                           (fe : Fun-Ext) where

open import Locales.WayBelowRelation.Definition pt fe

open import Locales.Frame pt fe

open PropositionalTruncation pt

open AllCombinators pt fe
open Locale

\end{code}

The bottom open `𝟎` is way below anything.

\begin{code}

𝟎-is-way-below-anything : (X : Locale 𝓀 π“₯ 𝓦)
                        β†’ (U : ⟨ π’ͺ X ⟩) β†’ (𝟎[ π’ͺ X ] β‰ͺ[ π’ͺ X ] U) holds
𝟎-is-way-below-anything X U S (ΞΉ , _) p = βˆ₯βˆ₯-rec βˆƒ-is-prop † ΞΉ
 where
  † : index S β†’ βˆƒ i κž‰ index S , (𝟎[ π’ͺ X ] ≀[ poset-of (π’ͺ X) ] S [ i ]) holds
  † i = ∣ i , 𝟎-is-bottom (π’ͺ X) (S [ i ]) ∣

\end{code}

Added on 2024-09-12.

\begin{code}

way-below-implies-below : (X : Locale 𝓀 π“₯ 𝓦)
                        β†’ {U V : ⟨ π’ͺ X ⟩}
                        β†’ (U β‰ͺ[ π’ͺ X ] V β‡’ U ≀[ poset-of (π’ͺ X) ] V) holds
way-below-implies-below {𝓀} {π“₯} {𝓦} X {U} {V} Ο† =
 βˆ₯βˆ₯-rec (holds-is-prop (U ≀[ Xβ‚š ] V)) † (Ο† S Ξ΄ p)
  where
   S : Fam 𝓦 ⟨ π’ͺ X ⟩
   S = πŸ™ , Ξ» { ⋆ β†’ V}

   Xβ‚š = poset-of (π’ͺ X)

   Ξ³ : (i j : index S)
     β†’ βˆƒ k κž‰ index S , (S [ i ] ≀[ Xβ‚š ] S [ k ]) holds
                     Γ— (S [ j ] ≀[ Xβ‚š ] S [ k ]) holds
   Ξ³ ⋆ ⋆ = ∣ ⋆ , ≀-is-reflexive Xβ‚š V , ≀-is-reflexive Xβ‚š V ∣

   Ξ΄ : is-directed (π’ͺ X) S holds
   Ξ΄ = ∣ ⋆ ∣ , Ξ³

   p : (V ≀[ Xβ‚š ] (⋁[ π’ͺ X ] S)) holds
   p = ⋁[ π’ͺ X ]-upper S ⋆

   † : (Ξ£ _ κž‰ πŸ™ , (U ≀[ Xβ‚š ] V) holds) β†’ (U ≀[ Xβ‚š ] V) holds
   † (⋆ , p) = p

\end{code}

Added on 2024-09-12.

\begin{code}

↑↑-is-upward-closed
 : (X : Locale 𝓀 π“₯ 𝓦)
 β†’ {U V W : ⟨ π’ͺ X ⟩}
 β†’ (U β‰ͺ[ π’ͺ X ] V β‡’ V ≀[ poset-of (π’ͺ X) ] W β‡’ U β‰ͺ[ π’ͺ X ] W) holds
↑↑-is-upward-closed X {U} {V} {W} Ο† q = †
 where
  open PosetReasoning (poset-of (π’ͺ X))

  † : (U β‰ͺ[ π’ͺ X ] W) holds
  † S Ξ΄ r = Ο† S Ξ΄ p
   where
    p : (V ≀[ poset-of (π’ͺ X) ] (⋁[ π’ͺ X ] S)) holds
    p = V β‰€βŸ¨ q ⟩ W β‰€βŸ¨ r ⟩ ⋁[ π’ͺ X ] S β– 

\end{code}

Added on 2024-09-12.

\begin{code}

being-way-below-is-closed-under-binary-joins
 : (X : Locale 𝓀 π“₯ 𝓦)
 β†’ {U V W : ⟨ π’ͺ X ⟩}
 β†’ (V β‰ͺ[ π’ͺ X ] U β‡’ W β‰ͺ[ π’ͺ X ] U β‡’ (V ∨[ π’ͺ X ] W) β‰ͺ[ π’ͺ X ] U) holds
being-way-below-is-closed-under-binary-joins X {U} {V} {W} p q S Ξ΄@(_ , Ο…) r =
 βˆ₯βˆ₯-recβ‚‚ βˆƒ-is-prop Ξ³ (p S Ξ΄ r) (q S Ξ΄ r)
  where
   open PosetReasoning (poset-of (π’ͺ X))

   † : (V ≀[ poset-of (π’ͺ X) ] (⋁[ π’ͺ X ] S)) holds
   † = way-below-implies-below X (↑↑-is-upward-closed X p r)

   ‑ : (W ≀[ poset-of (π’ͺ X) ] (⋁[ π’ͺ X ] S)) holds
   ‑ = way-below-implies-below X (↑↑-is-upward-closed X q r)

   Xβ‚š = poset-of (π’ͺ X)

   Ξ³ : Ξ£ i κž‰ index S , (V ≀[ Xβ‚š ] S [ i ]) holds
     β†’ Ξ£ i κž‰ index S , (W ≀[ Xβ‚š ] S [ i ]) holds
     β†’ βˆƒ k κž‰ index S , ((V ∨[ π’ͺ X ] W) ≀[ Xβ‚š ] S [ k ]) holds
   Ξ³ (i , p) (j , q) = βˆ₯βˆ₯-rec βˆƒ-is-prop Ξ΅ (Ο… i j)
    where
     Ξ΅ : Ξ£ k κž‰ index S ,
          (S [ i ] ≀[ Xβ‚š ] S [ k ] ∧ S [ j ] ≀[ Xβ‚š ] S [ k ]) holds
       β†’ βˆƒ k κž‰ index S ,
          ((V ∨[ π’ͺ X ] W) ≀[ Xβ‚š ] S [ k ]) holds
     Ξ΅ (k , r , s) = ∣ k , ∨[ π’ͺ X ]-least Ο† ψ ∣
      where
       Ο† : (V ≀[ poset-of (π’ͺ X) ] (S [ k ])) holds
       Ο† = V β‰€βŸ¨ p ⟩ S [ i ] β‰€βŸ¨ r ⟩ S [ k ] β– 

       ψ : (W ≀[ poset-of (π’ͺ X) ] (S [ k ])) holds
       ψ = W β‰€βŸ¨ q ⟩ S [ j ] β‰€βŸ¨ s ⟩ S [ k ] β– 

\end{code}