Mon（單調自映射）

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

open Conjunction
open Universal   fe
open Implication fe

Monotone map 是 Ω 的自映射 f : Ω → Ω，滿足 p ⇒ q 蘊涵 f p ⇒ f q

is-monotone : (Ω 𝓤 → Ω 𝓤) → Ω (𝓤 ⁺)
is-monotone f = Ɐ p ꞉ Ω 𝓤 , Ɐ q ꞉ Ω 𝓤 , (p ⇒ q) ⇒ (f p ⇒ f q)

Mon 代表所有 monotone maps 的 type

Mon : 𝓤 ⁺ ̇
Mon = Σ f ꞉ (Ω 𝓤 → Ω 𝓤) , is-monotone f holds

我們定義一個輔助函數讓之後的證明可讀一點

monotone-function : Mon → (Ω 𝓤 → Ω 𝓤)
monotone-function m = pr₁ m

Definition. Mon（單調自映射） [ag-V2O7]