Preorders and monotone functions

formalizations/guarded-cubical/Common/Monotone.agda

+{-# OPTIONS --safe #-}
+
+module Common.Monotone where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Relation.Binary.Base
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Structure
+
+open import Cubical.Foundations.HLevels
+open import Cubical.Reflection.Base hiding (_$_)
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+
+
+open import Common.Preorder
+
+open BinaryRelation
+
+
+private
+  variable
+    ℓ ℓ' : Level
+
+
+-- Helper functions
+
+-- The relation associated to a preorder X
+rel : (X : Preorder ℓ ℓ') -> (⟨ X ⟩ -> ⟨ X ⟩ -> Type ℓ')
+rel X = PreorderStr._≤_ (X .snd)
+
+reflexive : (X : Preorder ℓ ℓ') -> (x : ⟨ X ⟩) -> (rel X x x)
+reflexive X x = IsPreorder.is-refl (PreorderStr.isPreorder (str X)) x
+
+transitive : (X : Preorder ℓ ℓ') -> (x y z : ⟨ X ⟩) ->
+  rel X x y -> rel X y z -> rel X x z
+transitive X x y z x≤y y≤z =
+  IsPreorder.is-trans (PreorderStr.isPreorder (str X)) x y z x≤y y≤z
+
+isSet-preorder : (X : Preorder ℓ ℓ') -> isSet ⟨ X ⟩
+isSet-preorder X = IsPreorder.is-set (PreorderStr.isPreorder (str X))
+
+isPropValued-preorder : (X : Preorder ℓ ℓ') ->
+  isPropValued (PreorderStr._≤_ (str X))
+isPropValued-preorder X = IsPreorder.is-prop-valued
+  (PreorderStr.isPreorder (str X))
+
+
+-- If Y is a set, then functions into Y form a set
+isSetArrow : {X Y : Type} -> isSet Y -> isSet (X -> Y)
+isSetArrow Hy = λ f g p q i j x →
+  Hy (f x) (g x) (λ k -> p k x) (λ k -> q k x) i j
+
+
+module _ {ℓ ℓ' : Level} where
+
+  -- Because of a bug with Cubical Agda's reflection, we need to declare
+  -- a separate version of MonFun where the arguments to the isMon
+  -- constructor are explicit.
+  -- See https://github.com/agda/cubical/issues/995.
+  module _ {X Y : Preorder ℓ ℓ'} where
+
+    module X = PreorderStr (X .snd)
+    module Y = PreorderStr (Y .snd)
+    _≤X_ = X._≤_
+    _≤Y_ = Y._≤_
+
+    monotone' : (⟨ X ⟩ -> ⟨ Y ⟩) -> Type (ℓ-max ℓ ℓ')
+    monotone' f = (x y : ⟨ X ⟩) -> x ≤X y → f x ≤Y f y       
+
+    monotone : (⟨ X ⟩ -> ⟨ Y ⟩) -> Type (ℓ-max ℓ ℓ')
+    monotone f = {x y : ⟨ X ⟩} -> x ≤X y → f x ≤Y f y   
+
+  -- Monotone functions from X to Y
+  -- This definition works with Cubical Agda's reflection.
+  record MonFun' (X Y : Preorder ℓ ℓ') : Type ((ℓ-max ℓ ℓ')) where
+    field
+      f : (X .fst) → (Y .fst)
+      isMon : monotone' {X} {Y} f
+
+  -- This is the definition we want, where the first two arguments to isMon
+  -- are implicit.
+  record MonFun (X Y : Preorder ℓ ℓ') : Type ((ℓ-max ℓ ℓ')) where
+    field
+      f : (X .fst) → (Y .fst)
+      isMon : monotone {X} {Y} f
+
+  open MonFun
+
+  isoMonFunMonFun' : {X Y : Preorder ℓ ℓ'} -> Iso (MonFun X Y) (MonFun' X Y) 
+  isoMonFunMonFun' = iso
+    (λ g → record { f = MonFun.f g ; isMon = λ x y x≤y → isMon g x≤y })
+    (λ g → record { f = MonFun'.f g ; isMon = λ {x} {y} x≤y -> MonFun'.isMon g x y x≤y })
+    (λ g → refl)
+    (λ g → refl)
+
+  {-
+  isPropIsMon : {X Y : Preorder ℓ ℓ'} -> {f : MonFun X Y} ->
+    isProp (∀ x y -> rel X x y -> rel Y (MonFun.f f x) (MonFun.f f y))
+  isPropIsMon {X} {Y} {f} =
+    isPropΠ3 λ x y x≤y -> isPropValued-preorder Y (MonFun.f f x) (MonFun.f f y)
+  -}
+
+  
+  isPropIsMon : {X Y : Preorder ℓ ℓ'} -> (f : MonFun X Y) ->
+    isProp (monotone {X} {Y} (MonFun.f f))
+  isPropIsMon {X} {Y} f =
+    isPropImplicitΠ2 (λ x y ->
+      isPropΠ (λ x≤y -> isPropValued-preorder Y (MonFun.f f x) (MonFun.f f y)))
+
+  isPropIsMon' : {X Y : Preorder ℓ ℓ'} -> (f : ⟨ X ⟩ -> ⟨ Y ⟩) ->
+    isProp (monotone' {X} {Y} f)
+  isPropIsMon' {X} {Y} f =
+    isPropΠ3 (λ x y x≤y -> isPropValued-preorder Y (f x) (f y))
+
+
+ -- Equivalence between MonFun' record and a sigma type   
+  unquoteDecl MonFun'IsoΣ = declareRecordIsoΣ MonFun'IsoΣ (quote (MonFun'))
+
+  Sigma : (X Y : Preorder ℓ ℓ') -> Type (ℓ-max ℓ ℓ')
+  Sigma X Y =
+     (Σ (X .fst → Y .fst)
+     (λ z → (x y : ⟨ X ⟩) → _≤X_ {X} {Y} x y → _≤Y_ {X} {Y} (z x) (z y)))
+
+  test : {X Y : Preorder ℓ ℓ'} -> Iso (MonFun' X Y) (Sigma X Y)
+  test = MonFun'IsoΣ
+
+  MonFun≡Sigma : {X Y : Preorder ℓ ℓ'} -> MonFun' X Y ≡ Sigma X Y
+  MonFun≡Sigma = isoToPath MonFun'IsoΣ
+
+  Sigma≡ : {X Y : Preorder ℓ ℓ'} -> {s1 s2 : Sigma X Y} ->
+    s1 .fst ≡ s2 .fst -> s1 ≡ s2
+  Sigma≡ {X} {Y} = Σ≡Prop (λ f → isPropΠ3
+    (λ x y x≤y -> isPropValued-preorder Y (f x) (f y)))
+
+  -- Equality of monotone functions is equivalent to equality of the
+  -- underlying functions.
+  EqMon' : {X Y : Preorder ℓ ℓ'} -> (f g : MonFun' X Y) ->
+    MonFun'.f f ≡ MonFun'.f g -> f ≡ g
+  EqMon' {X} {Y} f g p = isoFunInjective MonFun'IsoΣ f g
+    (Σ≡Prop (λ h → isPropΠ3 (λ y z q → isPropValued-preorder Y (h y) (h z))) p)
+
+  EqMon : {X Y : Preorder ℓ ℓ'} -> (f g : MonFun X Y) ->
+    MonFun.f f ≡ MonFun.f g -> f ≡ g
+  EqMon {X} {Y} f g p = isoFunInjective isoMonFunMonFun' f g (EqMon' _ _ p)
+
+  -- isSet for Sigma
+  isSetSigma : {X Y : Preorder ℓ ℓ'} -> isSet (Sigma X Y)
+  isSetSigma {X} {Y} = isSetΣSndProp
+    (isSet→ (isSet-preorder Y))
+    λ f -> isPropIsMon' {X} {Y} f
+
+  -- isSet for monotone functions
+  MonFunIsSet : {X Y : Preorder ℓ ℓ'} -> isSet (MonFun X Y)
+  MonFunIsSet {X} {Y} = let composedIso = (compIso isoMonFunMonFun' MonFun'IsoΣ) in
+    isSetRetract
+      (Iso.fun composedIso) (Iso.inv composedIso) (Iso.leftInv composedIso)
+      (isSetΣSndProp
+        (isSet→ (isSet-preorder Y))
+        (isPropIsMon' {X} {Y}))
+
+
+
+ -- Ordering on monotone functions
+  module _ {X Y : Preorder ℓ ℓ'} where
+
+    _≤mon_ :
+      MonFun X Y → MonFun X Y → Type (ℓ-max ℓ ℓ')
+    _≤mon_ f g = ∀ x -> rel Y (MonFun.f f x) (MonFun.f g x)
+
+    ≤mon-prop : isPropValued _≤mon_
+    ≤mon-prop f g =
+      isPropΠ (λ x -> isPropValued-preorder Y (MonFun.f f x) (MonFun.f g x))
+
+    ≤mon-refl : isRefl _≤mon_
+    ≤mon-refl = λ f x → reflexive Y (MonFun.f f x)
+
+    ≤mon-trans : isTrans _≤mon_
+    ≤mon-trans = λ f g h f≤g g≤h x →
+      transitive Y (MonFun.f f x) (MonFun.f g x) (MonFun.f h x)
+        (f≤g x) (g≤h x)
+
+    -- Alternate definition of ordering on monotone functions, where we allow for the
+    -- arguments to be distinct
+    _≤mon-het_ : MonFun X Y -> MonFun X Y -> Type (ℓ-max ℓ ℓ')
+    _≤mon-het_ f f' = ∀ x x' -> rel X x x' -> rel Y (MonFun.f f x) (MonFun.f f' x')
+
+    ≤mon→≤mon-het : (f f' : MonFun X Y) -> f ≤mon f' -> f ≤mon-het f'
+    ≤mon→≤mon-het f f' f≤f' = λ x x' x≤x' →
+      MonFun.f f x    ≤⟨ MonFun.isMon f x≤x' ⟩
+      MonFun.f f x'   ≤⟨ f≤f' x' ⟩
+      MonFun.f f' x'  ◾
+      where
+        open PreorderReasoning Y
+
+
+ -- Predomain of monotone functions between two predomains
+  IntHom : Preorder ℓ ℓ' -> Preorder ℓ ℓ' ->
+    Preorder (ℓ-max ℓ ℓ') (ℓ-max ℓ ℓ') -- (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-max ℓ ℓ')
+  IntHom X Y =
+    MonFun X Y ,
+    (preorderstr
+      (_≤mon_)
+      (ispreorder MonFunIsSet ≤mon-prop ≤mon-refl ≤mon-trans))
+
+    -- Notation
+  _==>_ : Preorder ℓ ℓ' -> Preorder ℓ ℓ' ->
+    Preorder (ℓ-max ℓ ℓ') (ℓ-max ℓ ℓ') -- (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-max ℓ ℓ')
+  X ==> Y = IntHom X Y -- IntHom X Y
+
+
+
+  -- Some basic combinators/utility functions on monotone functions
+
+  MonId : {X : Preorder ℓ ℓ'} -> MonFun X X
+  MonId = record { f = λ x -> x ; isMon = λ x≤y → x≤y }
+
+  _$_ : {X Y : Preorder ℓ ℓ'} -> MonFun X Y -> ⟨ X ⟩ -> ⟨ Y ⟩
+  f $ x = MonFun.f f x
+
+  MonComp : {X Y Z : Preorder ℓ ℓ'} ->
+    MonFun X Y -> MonFun Y Z -> MonFun X Z
+  MonComp f g = record {
+    f = λ x -> g $ (f $ x) ;
+    isMon = λ {x1} {x2} x1≤x2 → isMon g (isMon f x1≤x2) }

formalizations/guarded-cubical/Common/Preorder.agda

+{-# OPTIONS --safe #-}
+{-# OPTIONS --cubical #-}
+
+module Common.Preorder where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.HalfAdjoint
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.SIP
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Reflection.StrictEquiv
+
+open import Cubical.Displayed.Base
+open import Cubical.Displayed.Auto
+open import Cubical.Displayed.Record
+open import Cubical.Displayed.Universe
+
+open import Cubical.Relation.Binary.Base
+
+open Iso
+open BinaryRelation
+
+
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ₀ ℓ₀' ℓ₁ ℓ₁' : Level
+
+record IsPreorder {A : Type ℓ} (_≤_ : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
+  no-eta-equality
+  constructor ispreorder
+
+  field
+    is-set : isSet A
+    is-prop-valued : isPropValued _≤_
+    is-refl : isRefl _≤_
+    is-trans : isTrans _≤_
+
+unquoteDecl IsPreorderIsoΣ = declareRecordIsoΣ IsPreorderIsoΣ (quote IsPreorder)
+
+
+record PreorderStr (ℓ' : Level) (A : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
+
+  constructor preorderstr
+
+  field
+    _≤_     : A → A → Type ℓ'
+    isPreorder : IsPreorder _≤_
+
+  infixl 7 _≤_
+
+  open IsPreorder isPreorder public
+
+Preorder : ∀ ℓ ℓ' → Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ'))
+Preorder ℓ ℓ' = TypeWithStr ℓ (PreorderStr ℓ')
+
+preorder : (A : Type ℓ) (_≤_ : A → A → Type ℓ') (h : IsPreorder _≤_) → Preorder ℓ ℓ'
+preorder A _≤_ h = A , preorderstr _≤_ h
+
+record IsPreorderEquiv {A : Type ℓ₀} {B : Type ℓ₁}
+  (M : PreorderStr ℓ₀' A) (e : A ≃ B) (N : PreorderStr ℓ₁' B)
+  : Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁')
+  where
+  constructor
+   ispreorderequiv
+  -- Shorter qualified names
+  private
+    module M = PreorderStr M
+    module N = PreorderStr N
+
+  field
+    pres≤ : (x y : A) → x M.≤ y ≃ equivFun e x N.≤ equivFun e y
+
+
+PreorderEquiv : (M : Preorder ℓ₀ ℓ₀') (M : Preorder ℓ₁ ℓ₁') → Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁'))
+PreorderEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsPreorderEquiv (M .snd) e (N .snd)
+
+isPropIsPreorder : {A : Type ℓ} (_≤_ : A → A → Type ℓ') → isProp (IsPreorder _≤_)
+isPropIsPreorder _≤_ = isOfHLevelRetractFromIso 1 IsPreorderIsoΣ
+  (isPropΣ isPropIsSet
+    λ isSetA → isPropΣ (isPropΠ2 (λ _ _ → isPropIsProp))
+      λ isPropValued≤ -> isProp× (isPropΠ (λ _ -> isPropValued≤ _ _))
+                                 (isPropΠ5 (λ _ _ _ _ _ -> isPropValued≤ _ _)))
+{-
+  (isPropΣ isPropIsSet
+    λ isSetA → isPropΣ (isPropΠ2 (λ _ _ → isPropIsProp))
+      λ isPropValued≤ → isProp×2
+                         (isPropΠ (λ _ → isPropValued≤ _ _))
+                           (isPropΠ5 λ _ _ _ _ _ → isPropValued≤ _ _)
+                             (isPropΠ4 λ _ _ _ _ → isSetA _ _))
+-}                           
+
+𝒮ᴰ-Preorder : DUARel (𝒮-Univ ℓ) (PreorderStr ℓ') (ℓ-max ℓ ℓ')
+𝒮ᴰ-Preorder =
+  𝒮ᴰ-Record (𝒮-Univ _) IsPreorderEquiv
+    (fields:
+      data[ _≤_ ∣ autoDUARel _ _ ∣ pres≤ ]
+      prop[ isPreorder ∣ (λ _ _ → isPropIsPreorder _) ])
+    where
+    open PreorderStr
+    open IsPreorder
+    open IsPreorderEquiv
+
+PreorderPath : (M N : Preorder ℓ ℓ') → PreorderEquiv M N ≃ (M ≡ N)
+PreorderPath = ∫ 𝒮ᴰ-Preorder .UARel.ua
+
+-- an easier way of establishing an equivalence of preorders
+module _ {P : Preorder ℓ₀ ℓ₀'} {S : Preorder ℓ₁ ℓ₁'} (e : ⟨ P ⟩ ≃ ⟨ S ⟩) where
+  private
+    module P = PreorderStr (P .snd)
+    module S = PreorderStr (S .snd)
+
+  module _ (isMon : ∀ x y → x P.≤ y → equivFun e x S.≤ equivFun e y)
+           (isMonInv : ∀ x y → x S.≤ y → invEq e x P.≤ invEq e y) where
+    open IsPreorderEquiv
+    open IsPreorder
+
+    makeIsPreorderEquiv : IsPreorderEquiv (P .snd) e (S .snd)
+    pres≤ makeIsPreorderEquiv x y = propBiimpl→Equiv (P.isPreorder .is-prop-valued _ _)
+                                                  (S.isPreorder .is-prop-valued _ _)
+                                                  (isMon _ _) (isMonInv' _ _)
+      where
+      isMonInv' : ∀ x y → equivFun e x S.≤ equivFun e y → x P.≤ y
+      isMonInv' x y ex≤ey = transport (λ i → retEq e x i P.≤ retEq e y i) (isMonInv _ _ ex≤ey)
+
+
+module PreorderReasoning (P' : Preorder ℓ ℓ') where
+ private P = fst P'
+ open PreorderStr (snd P')
+ open IsPreorder
+
+ _≤⟨_⟩_ : (x : P) {y z : P} → x ≤ y → y ≤ z → x ≤ z
+ x ≤⟨ p ⟩ q = isPreorder .is-trans x _ _ p q
+
+ _◾ : (x : P) → x ≤ x
+ x ◾ = isPreorder .is-refl x
+
+ infixr 0 _≤⟨_⟩_
+ infix  1 _◾