Proposition. $L(f)$ 保持元素的 meet [ag-3HBW]

$L$ 保持有限 meet 是運算子格上的 meet，這裡要證明的是 $L(f)$ 是否保持 frame 元素的 meet，也就是

這正是 $L(f)$ 是不是 nucleus 的關鍵條件

{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Size
open import UF.Logic

module ag-3HBW
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-V2O7 pt fe pe ρ
open import ag-5W9X pt fe pe ρ
open import ag-GY8B pt fe pe ρ
open import ag-95LU pt fe pe ρ
open is-local-operator

⊤ ⇒ s 等於 s 成立。

⊤⇒ : (s : Ω 𝓤) → (⊤ {𝓤} ⇒ s) ＝ s
⊤⇒ s = Ω-extensionality pe fe (λ ⊤⇒s → ⊤⇒s ⊤-holds) (λ sh _ → sh)

(⇐) 方向：L f p ∧ L f q → L f (p ∧ q)

L-preserves-arg-∧-⇐ : (f : Ω 𝓤 → Ω 𝓤) (p q : Ω 𝓤)
                    → (L f p holds × L f q holds)
                    → L f (p ∧ q) holds
L-preserves-arg-∧-⇐ f p q (L[f][p] , L[f][q]) = ηL f (p ∧ q) I
  where
  L[p] = εL f p L[f][p]
  L[q] = εL f q L[f][q]

  I : (L⁺ f (p ∧ q)) holds
  I s (p∧q⇒s , fs⇒s) = L[q] s (q⇒s , fs⇒s)
    where
    -- 在 L f p 代入 r := (q ⇒ s)，取得 q ⇒ s
    q⇒s : (q ⇒ s) holds
    q⇒s = L[p] (q ⇒ s) (uncurried , f⟨q⇒s⟩⇒)
      where
      uncurried : (p ⇒ (q ⇒ s)) holds
      uncurried ph qh = p∧q⇒s (ph , qh)

      -- f (q ⇒ s) ⇒ (q ⇒ s)：q 成立時 (q ⇒ s) ＝ s，故 f (q ⇒ s) ＝ f s
      f⟨q⇒s⟩⇒ : (f (q ⇒ s) ⇒ (q ⇒ s)) holds
      f⟨q⇒s⟩⇒ y qh = fs⇒s (transport (λ - → f - holds) ⟨q⇒s⟩＝s y)
        where
        ⟨q⇒s⟩＝s : (q ⇒ s) ＝ s
        ⟨q⇒s⟩＝s = ap (_⇒ s) (holds-gives-equal-⊤ pe fe q qh) ∙ ⊤⇒ s

(⇒) 方向：由 L f 的單調性（因為 L(f) 是 local operator）配上 p ∧ q ⇒ p、p ∧ q ⇒ q。

L-preserves-arg-∧-⇒ : (m : Mon) (p q : Ω 𝓤)
   → L (monotone-function m) (p ∧ q) holds
   → (L (monotone-function m) p holds × L (monotone-function m) q holds)
L-preserves-arg-∧-⇒ m p q lf[p∧q] = mn (p ∧ q) p pr₁ lf[p∧q]
                                   , mn (p ∧ q) q pr₂ lf[p∧q]
  where
  mn = L-is-local-operator m .mono

合併得到

L-preserves-arg-∧ : (m : Mon) (p q : Ω 𝓤)
   → L (monotone-function m) (p ∧ q)
   ＝ L (monotone-function m) p ∧ L (monotone-function m) q
L-preserves-arg-∧ m p q =
  Ω-extensionality pe fe (L-preserves-arg-∧-⇒ m p q)
                         (L-preserves-arg-∧-⇐ (monotone-function m) p q)