Definition. ΩΩ\Omega^\Omega 的逐點序 ≼ [ag-UAEO]

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

open Conjunction
open Universal   fe
open Implication fe

ΩΩ\Omega^\Omega 的元素之間我們可以用 pointwise 的方式定義一個順序 f ≼ g：對每個 p，f p ⇒ g p

_≼_ : (Ω 𝓤 → Ω 𝓤) → (Ω 𝓤 → Ω 𝓤) → Ω (𝓤 ⁺)
f ≼ g = Ɐ p ꞉ Ω 𝓤 , f p ⇒ g p

後面談 L 是左伴隨時就是用這個順序。