任何 local operator $j$ 都是 inflationary 的，也就是 $p \Rightarrow j\ p$

Proof [local-0]

{-# 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-GK6B
  (pt : propositional-truncations-exist)
  (fe : Fun-Ext)
  (pe : propext 𝓤)
  (ρ  : propositional-resizing (𝓤 ⁺) 𝓤)
  where

open Conjunction
open Universal   fe
open Implication fe

open import ag-5W9X pt fe pe ρ
open is-local-operator

證明方式：若 p 成立則 p ＝ ⊤（用到 propext），再由 unit 得到 j ⊤。

LO-infl : {j : Ω 𝓤 → Ω 𝓤} → is-local-operator j → (p : Ω 𝓤) → (p ⇒ j p) holds
LO-infl {j} j-is-local-op p p-holds = transport (λ - → j - holds) ⊤＝p j⊤
  where
  -- p 成立，故 p ＝ ⊤
  ⊤＝p : ⊤ ＝ p
  ⊤＝p = (holds-gives-equal-⊤ pe fe p p-holds) ⁻¹

  -- 由 unit
  j⊤ : j ⊤ holds
  j⊤ = unit j-is-local-op ⋆

Lemma. Local operator 是 inflationary [ag-GK6B]

Proof [local-0]