Local operator

{-# 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-5W9X
  (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 ρ

Local operator 是一個 Ω 自映射 j : Ω → Ω，滿足

單調（mono）
保持 ⊤（unit）
冪等（idem）

三個條件定義在 record 中

record is-local-operator (j : Ω 𝓤 → Ω 𝓤) : 𝓤 ⁺ ̇ where
  field
    mono : is-monotone j holds
    unit : (⊤ {𝓤} ⇒ j ⊤) holds
    idem : (p : Ω 𝓤) → (j (j p) ⇒ j p) holds

Definition. Local operator [ag-5W9X]