Monotone stuff

formalizations/guarded-cubical/Common/Poset/Monotone.agda

+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+-- TODO: This could be generalized to handle monotone functions on
+-- both preorders and posets.
+
+module Common.Poset.Monotone where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function hiding (_$_)
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Relation.Binary.Base
+open import Cubical.Reflection.Base
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Data.Sigma
+
+-- open import Common.Preorder.Base
+open import Cubical.Relation.Binary.Poset
+open import Common.Poset.Convenience
+
+
+open BinaryRelation
+
+
+private
+  variable
+    ℓ ℓ' : Level
+    ℓX ℓ'X ℓY ℓ'Y : Level
+
+
+module _ 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 : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} where
+
+    private
+
+      module X = PosetStr (X .snd)
+      module Y = PosetStr (Y .snd)
+      _≤X_ = X._≤_
+      _≤Y_ = Y._≤_
+
+    monotone' : (⟨ X ⟩ -> ⟨ Y ⟩) -> Type (ℓ-max (ℓ-max ℓX ℓ'X) ℓ'Y)
+    monotone' f = (x y : ⟨ X ⟩) -> x ≤X y → f x ≤Y f y       
+
+    monotone : (⟨ X ⟩ -> ⟨ Y ⟩) -> Type (ℓ-max (ℓ-max ℓX ℓ'X) ℓ'Y)
+    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 : Poset ℓX ℓ'X) (Y : Poset ℓY ℓ'Y) :
+    Type ((ℓ-max (ℓ-max ℓX ℓ'X) (ℓ-max ℓY ℓ'Y))) where
+    field
+      f : (X .fst) → (Y .fst)
+      isMon : monotone' {X = X} {Y = Y} f
+
+  -- This is the definition we want, where the first two arguments to isMon
+  -- are implicit.
+  record MonFun (X : Poset ℓX ℓ'X) (Y : Poset ℓY ℓ'Y) :
+    Type (ℓ-max (ℓ-max ℓX ℓ'X) (ℓ-max ℓY ℓ'Y)) where
+    field
+      f : (X .fst) → (Y .fst)
+      isMon : monotone {X = X} {Y = Y} f
+
+  open MonFun
+
+
+  isoMonFunMonFun' : {X : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} -> 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 : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} -> (f : MonFun X Y) ->
+    isProp (monotone {X = X} {Y = Y} (MonFun.f f))
+  isPropIsMon {X = X} {Y = Y} f =
+    isPropImplicitΠ2 (λ x y ->
+      isPropΠ (λ x≤y -> isPropValued-poset Y (MonFun.f f x) (MonFun.f f y)))
+
+  isPropIsMon' : {X : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} -> (f : ⟨ X ⟩ -> ⟨ Y ⟩) ->
+    isProp (monotone' {X = X} {Y = Y} f)
+  isPropIsMon' {X = X} {Y = Y} f =
+    isPropΠ3 (λ x y x≤y -> isPropValued-poset Y (f x) (f y))
+
+
+ -- Equivalence between MonFun' record and a sigma type   
+  unquoteDecl MonFun'IsoΣ = declareRecordIsoΣ MonFun'IsoΣ (quote (MonFun'))
+
+
+  -- Equality of monotone functions is implied by equality of the
+  -- underlying functions.
+  eqMon' : {X : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} -> (f g : MonFun' X Y) ->
+    MonFun'.f f ≡ MonFun'.f g -> f ≡ g
+  eqMon' {X = X} {Y = Y} f g p = isoFunInjective MonFun'IsoΣ f g
+    (Σ≡Prop (λ h → isPropΠ3 (λ y z q → isPropValued-poset Y (h y) (h z))) p)
+
+  eqMon : {X : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} -> (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 monotone functions
+  MonFunIsSet : {X : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} -> isSet (MonFun X Y)
+  MonFunIsSet {X = X} {Y = Y} = let composedIso = (compIso isoMonFunMonFun' MonFun'IsoΣ) in
+    isSetRetract
+      (Iso.fun composedIso) (Iso.inv composedIso) (Iso.leftInv composedIso)
+      (isSetΣSndProp
+        (isSet→ (isSet-poset Y))
+        (isPropIsMon' {X = X} {Y = Y}))
+
+
+
+ -- Ordering on monotone functions
+  module _ {X : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y}  where
+
+    _≤mon_ :
+      MonFun X Y → MonFun X Y → Type (ℓ-max ℓX ℓ'Y)
+    _≤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-poset 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)
+
+    ≤mon-antisym : isAntisym _≤mon_
+    ≤mon-antisym f g f≤g g≤f =
+      eqMon f g (funExt (λ x -> antisym Y (MonFun.f f x) (MonFun.f g x) (f≤g x) (g≤f 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 (ℓ-max ℓX ℓ'X) ℓ'Y)
+    _≤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 PosetReasoning Y
+
+
+
+ -- Predomain of monotone functions between two predomains
+  IntHom : Poset ℓX ℓ'X -> Poset ℓY ℓ'Y ->
+    Poset (ℓ-max (ℓ-max (ℓ-max ℓX ℓ'X) ℓY) ℓ'Y) (ℓ-max ℓX ℓ'Y)
+  IntHom X Y =
+    MonFun X Y ,
+    (posetstr
+      (_≤mon_)
+      (isposet MonFunIsSet ≤mon-prop ≤mon-refl ≤mon-trans ≤mon-antisym))
+
+    -- Notation
+  _==>_ : Poset ℓX ℓ'X -> Poset ℓY ℓ'Y ->
+    Poset (ℓ-max (ℓ-max (ℓ-max ℓX ℓ'X) ℓY) ℓ'Y) (ℓ-max ℓX ℓ'Y) -- (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-max ℓ ℓ')
+  X ==> Y = IntHom X Y
+
+  infixr 20 _==>_
+
+
+
+  -- Some basic combinators/utility functions on monotone functions
+
+  MonId : {X : Poset ℓ ℓ'} -> MonFun X X
+  MonId = record { f = λ x -> x ; isMon = λ x≤y → x≤y }
+
+  _$_ : {X Y : Poset ℓ ℓ'} -> MonFun X Y -> ⟨ X ⟩ -> ⟨ Y ⟩
+  f $ x = MonFun.f f x
+
+  MonComp : {X Y Z : Poset ℓ ℓ'} ->
+    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/Poset/MonotoneRelation.agda

+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Common.Poset.MonotoneRelation where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Sigma
+
+open import Common.Common
+open import Common.Poset.Convenience
+open import Common.Poset.Monotone hiding (monotone)
+
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+    ℓo : Level
+
+
+-- Monotone relations between posets X and Y
+-- (antitone in X, monotone in Y).
+record MonRel (X Y : Poset ℓ ℓ') {ℓ'' : Level} : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓ'')) where
+  module X = PosetStr (X .snd)
+  module Y = PosetStr (Y .snd)
+  _≤X_ = X._≤_
+  _≤Y_ = Y._≤_
+  field
+    R : ⟨ X ⟩ -> ⟨ Y ⟩ -> Type ℓ''
+    isAntitone : ∀ {x x' y} -> R x y -> x' ≤X x -> R x' y
+    isMonotone : ∀ {x y y'} -> R x y -> y ≤Y y' -> R x y'
+
+
+module MonReasoning {ℓ'' : Level} {X Y : Poset ℓ ℓ'} where
+  --open MonRel
+  module X = PosetStr (X .snd)
+  module Y = PosetStr (Y .snd)
+  _≤X_ = X._≤_
+  _≤Y_ = Y._≤_
+  
+  
+  -- _Anti⟨_⟩_: R x y -> x'≤X x -> R x' y
+  [_]_Anti⟨_⟩_ : (S : MonRel X Y {ℓ''}) ->
+    (x' : ⟨ X ⟩) -> {x : ⟨ X ⟩} -> {y : ⟨ Y ⟩} ->
+    x' ≤X x -> (S .MonRel.R) x y -> (S .MonRel.R) x' y
+  [ S ] x' Anti⟨ x'≤x ⟩ x≤y = S .MonRel.isAntitone x≤y x'≤x
+
+
+  [_]_Mon⟨_⟩_ : (S : MonRel X Y {ℓ''}) ->
+    (x : ⟨ X ⟩) -> {y y' : ⟨ Y ⟩} ->
+    (S .MonRel.R) x y -> y ≤Y y' -> (S .MonRel.R x y')
+  [ S ] x Mon⟨ x≤y ⟩ y≤y' = S .MonRel.isMonotone x≤y y≤y'
+
+poset-monrel : {ℓo : Level} -> (X : Poset ℓ ℓ') -> MonRel X X {ℓ-max ℓo ℓ'}
+poset-monrel {ℓ' = ℓ'} {ℓo = ℓo} X = record {
+  R = λ x1 x2 -> Lift {i = ℓ'} {j = ℓo} (rel X x1 x2) ;
+  isAntitone = λ {x} {x'} {y} x≤y x'≤x → lift (transitive X x' x y x'≤x (lower x≤y)) ;
+  isMonotone = λ {x} {y} {y'} x≤y y≤y' -> lift (transitive X x y y' (lower x≤y) y≤y') }
+
+
+-- Composing with functions on either side
+functionalRel : {X' X Y Y' : Poset ℓ ℓ'} ->
+  (f : MonFun X' X) ->
+  (g : MonFun Y' Y) ->
+  (R : MonRel X Y {ℓ''}) ->
+  MonRel X' Y'
+functionalRel f g R = record {
+  R = λ x' y' -> MonRel.R R (MonFun.f f x') (MonFun.f g y') ;
+  isAntitone = λ {x'2} {x'1} {y} H x'1≤x'2 → MonRel.isAntitone R H (MonFun.isMon f x'1≤x'2) ;
+  isMonotone = λ {x'} {y'1} {y'2} H y'1≤y'2 → MonRel.isMonotone R H (MonFun.isMon g y'1≤y'2) }
+  
+
+compRel : {ℓ ℓ' : Level} -> {X Y Z : Type ℓ} ->
+  (R1 : X -> Y -> Type ℓ') ->
+  (R2 : Y -> Z -> Type ℓ') ->
+  (X -> Z -> Type (ℓ-max ℓ ℓ'))
+compRel {ℓ} {ℓ'} {X} {Y} {Z} R1 R2 x z = Σ[ y ∈ Y ] R1 x y × R2 y z
+
+CompMonRel : -- {ℓX ℓ'X ℓY ℓ'Y ℓZ ℓ'Z : Level} {X : Poset ℓX ℓ'X} {Y : Poset ℓY ℓ'Y} {Z : Poset ℓZ ℓ'Z} ->
+  {X Y Z : Poset ℓ ℓ'} ->
+  MonRel X Y {ℓ''} ->
+  MonRel Y Z {ℓ''} ->
+  MonRel X Z {ℓ-max ℓ ℓ''}
+CompMonRel {ℓ''} {X = X} {Y = Y} {Z = Z} R1 R2 = record {
+  R = compRel (MonRel.R R1) (MonRel.R R2) ;
+  isAntitone = antitone ;
+  isMonotone = monotone }
+    where
+      antitone : {x x' : ⟨ X ⟩} {z : ⟨ Z ⟩} ->
+        compRel (MonRel.R R1) (MonRel.R R2) x z ->
+        rel X x' x ->
+        compRel (MonRel.R R1) (MonRel.R R2) x' z 
+      antitone (y , xR1y , yR2z) x'≤x = y , (MonRel.isAntitone R1 xR1y x'≤x) , yR2z
+
+      monotone : {x : ⟨ X ⟩} {z z' : ⟨ Z ⟩} ->
+        compRel (MonRel.R R1) (MonRel.R R2) x z ->
+        rel Z z z' ->
+        compRel (MonRel.R R1) (MonRel.R R2) x z'
+      monotone (y , xR1y , yR2z) z≤z' = y , xR1y , (MonRel.isMonotone R2 yR2z z≤z')
+
+
+-- Monotone relations between function spaces
+_==>monrel_ : {ℓ'' : Level} {Ai Ao Bi Bo : Poset ℓ ℓ'} ->
+  MonRel Ai Bi {ℓ''} ->
+  MonRel Ao Bo {ℓ''} ->
+  MonRel (Ai ==> Ao) (Bi ==> Bo) {ℓ-max ℓ ℓ''}
+R ==>monrel S = record {
+  R = λ f g -> TwoCell (MonRel.R R) (MonRel.R S) (MonFun.f f) (MonFun.f g)  ;
+  isAntitone = λ {f1} {f2} {g} f1≤g f2≤f1 a b aRb → MonRel.isAntitone S (f1≤g a b aRb) (f2≤f1 a) ;
+  isMonotone = λ {f} {g1} {g2} f≤g1 g1≤g2 a b aRb → MonRel.isMonotone S (f≤g1 a b aRb) (g1≤g2 b) }

formalizations/guarded-cubical/Semantics/Concrete/MonotonicityProofs.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.Concrete.MonotonicityProofs (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_^_)
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+
+open import Cubical.Foundations.Function
+
+-- open import Semantics.Predomains
+open import Semantics.Lift k
+-- open import Semantics.Monotone.Base
+-- open import Semantics.StrongBisimulation k
+-- open import Semantics.PredomainInternalHom
+
+open import Common.Common
+
+open import Cubical.Relation.Binary.Poset
+open import Common.Poset.Convenience
+open import Common.Poset.Monotone
+open import Common.Poset.Constructions
+
+open import Semantics.LockStepErrorOrdering k
+
+private
+  variable
+    ℓ ℓ' : Level
+    ℓR1 ℓR2 : Level
+    ℓA ℓ'A ℓA' ℓ'A' ℓB ℓ'B ℓB' ℓ'B' : Level
+    A :  Poset ℓA ℓ'A
+    A' : Poset ℓA' ℓ'A'
+    B :  Poset ℓB ℓ'B
+    B' : Poset ℓB' ℓ'B'
+private
+  ▹_ : Type ℓ → Type ℓ
+  ▹_ A = ▹_,_ k A
+
+open LiftPoset
+
+
+-- If A ≡ B, then we can translate knowledge about a relation on A
+-- to its image in B obtained by transporting the related elements of A
+-- along the equality of the underlying sets of A and B
+rel-transport :
+  {A B : Poset ℓ ℓ'} ->
+  (eq : A ≡ B) ->
+  {a1 a2 : ⟨ A ⟩} ->
+  rel A a1 a2 ->
+  rel B
+    (transport (λ i -> ⟨ eq i ⟩) a1)
+    (transport (λ i -> ⟨ eq i ⟩) a2)
+rel-transport {A} {B} eq {a1} {a2} a1≤a2 =
+  transport (λ i -> rel (eq i)
+    (transport-filler (λ j -> ⟨ eq j ⟩) a1 i)
+    (transport-filler (λ j -> ⟨ eq j ⟩) a2 i))
+  a1≤a2
+
+rel-transport-sym : {A B : Poset ℓ ℓ'} ->
+  (eq : A ≡ B) ->
+  {b1 b2 : ⟨ B ⟩} ->
+  rel B b1 b2 ->
+  rel A
+    (transport (λ i → ⟨ sym eq i ⟩) b1)
+    (transport (λ i → ⟨ sym eq i ⟩) b2)
+rel-transport-sym eq {b1} {b2} b1≤b2 = rel-transport (sym eq) b1≤b2
+
+
+mTransport : {A B : Poset ℓ ℓ'} -> (eq : A ≡ B) -> ⟨ A ==> B ⟩
+mTransport {A} {B} eq = record {
+  f = λ b → transport (λ i -> ⟨ eq i ⟩) b ;
+  isMon = λ {b1} {b2} b1≤b2 → rel-transport eq b1≤b2 }
+
+
+mTransportSym : {A B : Poset ℓ ℓ'} -> (eq : A ≡ B) -> ⟨ B ==> A ⟩
+mTransportSym {A} {B} eq = record {
+  f = λ b → transport (λ i -> ⟨ sym eq i ⟩) b ;
+  isMon = λ {b1} {b2} b1≤b2 → rel-transport (sym eq) b1≤b2 }
+
+
+-- Transporting the domain of a monotone function preserves monotonicity
+mon-transport-domain : {A B C : Poset ℓ ℓ'} ->
+  (eq : A ≡ B) ->
+  (f : MonFun A C) ->
+  {b1 b2 : ⟨ B ⟩} ->
+  (rel B b1 b2) ->
+  rel C
+    (MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b1))
+    (MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b2))
+mon-transport-domain eq f {b1} {b2} b1≤b2 =
+  MonFun.isMon f (rel-transport (sym eq) b1≤b2)
+
+mTransportDomain : {A B C : Poset ℓ ℓ'} ->
+  (eq : A ≡ B) ->
+  MonFun A C ->
+  MonFun B C
+mTransportDomain {A} {B} {C} eq f = record {
+  f = g eq f;
+  isMon = mon-transport-domain eq f }
+  where
+    g : {A B C : Poset ℓ ℓ'} ->
+      (eq : A ≡ B) ->
+      MonFun A C ->
+      ⟨ B ⟩ -> ⟨ C ⟩
+    g eq f b = MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b)
+
+
+
+
+-- ext respects monotonicity, in a general, heterogeneous sense
+ext-monotone-het : {A A' : Poset ℓA ℓ'A} {B B' : Poset ℓB ℓ'B}
+  (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type ℓR1) ->
+  (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type ℓR2) ->
+  (f :  ⟨ A ⟩  -> ⟨ (𝕃 B) ⟩) ->
+  (f' : ⟨ A' ⟩ -> ⟨ (𝕃 B') ⟩) ->
+  TwoCell rAA' (LiftRelation._≾_ _ _ rBB') f f' ->
+  (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩) ->
+  (LiftRelation._≾_ _ _ rAA' la la') ->
+  LiftRelation._≾_ _ _ rBB' (ext f la) (ext f' la')
+ext-monotone-het {A = A} {A' = A'} {B = B} {B' = B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+  let fixed = fix (monotone-ext') in
+  transport
+    (sym (λ i -> LiftBB'.unfold-≾ i (unfold-ext f i la) (unfold-ext f' i la')))
+    (fixed la la' (transport (λ i → LiftAA'.unfold-≾ i la la') la≤la'))
+  where
+
+    -- Note that these four have already been
+    -- passed (next _≾_) as a parameter (this happened in
+    -- the defintion of the module 𝕃, where we said
+    -- open Inductive (next _≾_) public)
+    _≾'LA_  = LiftPoset._≾'_ A
+    _≾'LA'_ = LiftPoset._≾'_ A'
+    _≾'LB_  = LiftPoset._≾'_ B
+    _≾'LB'_ = LiftPoset._≾'_ B'
+
+    module LiftAA' = LiftRelation ⟨ A ⟩ ⟨ A' ⟩ rAA'
+    module LiftBB' = LiftRelation ⟨ B ⟩ ⟨ B' ⟩ rBB'
+
+    -- The heterogeneous lifted relations
+    _≾'LALA'_ = LiftAA'.Inductive._≾'_ (next LiftAA'._≾_)
+    _≾'LBLB'_ = LiftBB'.Inductive._≾'_ (next LiftBB'._≾_)
+    
+
+    monotone-ext' :
+      ▹ (
+          (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩)  ->
+          (la ≾'LALA' la') ->
+          (ext' f  (next (ext f))  la) ≾'LBLB'
+          (ext' f' (next (ext f')) la')) ->
+        (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩)  ->
+        (la ≾'LALA' la') ->
+        (ext' f  (next (ext f))  la) ≾'LBLB'
+        (ext' f' (next (ext f')) la')
+    monotone-ext' IH (η x) (η y) x≤y =
+      transport
+      (λ i → LiftBB'.unfold-≾ i (f x) (f' y))
+      (f≤f' x y x≤y)
+    monotone-ext' IH ℧ la' la≤la' = tt*
+    monotone-ext' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+      transport
+        (λ i → (sym (LiftBB'.unfold-≾)) i
+          (sym (unfold-ext f) i (lx~ t))
+          (sym (unfold-ext f') i (ly~ t)))
+        (IH t (lx~ t) (ly~ t)
+          (transport (λ i -> LiftAA'.unfold-≾ i (lx~ t) (ly~ t)) (la≤la' t)))
+
+
+
+-- ext respects monotonicity (in the usual homogeneous sense)
+-- This can be rewritten to reuse the above result!
+ext-monotone :
+  (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->
+  TwoCell (rel A) (rel (𝕃 B)) f f' ->
+  (la la' : ⟨ 𝕃 A ⟩) ->
+  rel (𝕃 A) la la' ->
+  rel (𝕃 B) (ext f la) (ext f' la')
+ext-monotone {A} {B} f f' f≤f' la la' la≤la' = {!!}
+ 
+
+bind-monotone :
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->
+  rel (𝕃 A) la la' ->
+  TwoCell (rel A) (rel (𝕃 B)) f f' ->
+  rel (𝕃 B) (bind la f) (bind la' f')
+bind-monotone {A = A} {B = B} {la = la} {la' = la'} f f' la≤la' f≤f' =
+  ext-monotone {A = A} {B = B} f f' f≤f' la la' la≤la'
+   
+
+mapL-monotone-het : {A A' : Poset ℓA ℓ'A} {B B' : Poset ℓB' ℓ'B'} ->
+  (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type ℓR1) ->
+  (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type ℓR2) ->
+  (f : ⟨ A ⟩ -> ⟨ B ⟩) ->
+  (f' : ⟨ A' ⟩ -> ⟨ B' ⟩) ->
+  TwoCell rAA' rBB' f f' ->
+  (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩) ->
+  (LiftRelation._≾_ _ _ rAA' la la') ->
+   LiftRelation._≾_ _ _ rBB' (mapL f la) (mapL f' la')
+mapL-monotone-het {A = A} {A' = A'} {B = B} {B' = B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+  ext-monotone-het {A = A} {A' = A'} {B = B} {B' = B'} rAA' rBB' (ret ∘ f) (ret ∘ f')
+    (λ a a' a≤a' → LiftRelation.Properties.ord-η-monotone _ _ rBB' (f≤f' a a' a≤a'))
+    la la' la≤la'
+
+
+-- This is a special case of the above
+mapL-monotone : {A B : Poset ℓ ℓ'} ->
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f f' : ⟨ A ⟩ -> ⟨ B ⟩) ->
+  rel (𝕃 A) la la' ->
+  TwoCell (rel A) (rel B) f f' ->
+  rel (𝕃 B) (mapL f la) (mapL f' la')
+mapL-monotone {A = A} {B = B} {la = la} {la' = la'} f f' la≤la' f≤f' =
+  bind-monotone (ret ∘ f) (ret ∘ f') la≤la'
+    (λ a1 a2 a1≤a2 → ord-η-monotone B (f≤f' a1 a2 a1≤a2))
+
+
+-- As a corollary/special case, we can consider the case of a single
+-- monotone function.
+monotone-bind-mon :
+  {la la' : ⟨ 𝕃 A ⟩} ->
+  (f : MonFun A (𝕃 B)) ->
+  (rel (𝕃 A) la la') ->
+  rel (𝕃 B) (bind la (MonFun.f f)) (bind la' (MonFun.f f))
+monotone-bind-mon f la≤la' =
+  bind-monotone (MonFun.f f) (MonFun.f f) la≤la' (≤mon-refl {!!})
+

formalizations/guarded-cubical/Semantics/MonotoneCombinators.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+{-# OPTIONS --lossy-unification #-}
+
+open import Common.Later
+
+module Semantics.MonotoneCombinators where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (ℕ to Nat)
+
+open import Cubical.Relation.Binary
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Unit
+-- open import Cubical.Data.Prod
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+open import Cubical.Data.Sum
+
+open import Cubical.Foundations.Function hiding (_$_)
+
+open import Common.Common
+
+
+
+open import Cubical.Relation.Binary.Poset
+open import Common.Poset.Convenience
+open import Common.Poset.Monotone
+open import Common.Poset.Constructions
+
+
+private
+  variable
+    ℓ ℓ' : Level
+    ℓA ℓ'A ℓA' ℓ'A' ℓB ℓ'B ℓB' ℓ'B' ℓC ℓ'C ℓΓ ℓ'Γ : Level
+    Γ :  Poset ℓΓ ℓ'Γ
+    A :  Poset ℓA ℓ'A
+    A' : Poset ℓA' ℓ'A'
+    B :  Poset ℓB ℓ'B
+    B' : Poset ℓB' ℓ'B'
+    C :  Poset ℓC ℓ'C
+    
+
+
+open MonFun
+
+
+
+
+-- Composing monotone functions
+mCompU : MonFun B C -> MonFun A B -> MonFun A C
+mCompU f1 f2 = record {
+    f = λ a -> f1 .f (f2 .f a) ;
+    isMon = λ x≤y -> f1 .isMon (f2 .isMon x≤y) }
+  where open MonFun
+
+mComp :
+    ⟨ (B ==> C) ==> (A ==> B) ==> (A ==> C) ⟩
+mComp = record {
+    f = λ fBC →
+      record {
+        f = λ fAB → mCompU fBC fAB ;
+        isMon = λ {f1} {f2} f1≤f2 -> λ a → isMon fBC (f1≤f2 a) } ;
+    isMon = λ {f1} {f2} f1≤f2 → λ f' a → f1≤f2 (MonFun.f f' a) }
+
+
+Pair : ⟨ A ==> B ==> (A ×p B) ⟩
+Pair {A = A} {B = B} = record {
+  f = λ a →
+    record {
+      f = λ b -> a , b ;
+      isMon = λ b1≤b2 → (reflexive A a) , b1≤b2 } ;
+  isMon = λ {a1} {a2} a1≤a2 b → a1≤a2 , reflexive B b }
+
+PairFun : (f : ⟨ A ==> B ⟩) -> (g : ⟨ A ==> C ⟩ ) -> ⟨ A ==> B ×p C ⟩
+PairFun f g = record {
+  f = λ a -> (MonFun.f f a) , (MonFun.f g a) ;
+  isMon = {!!} }
+
+
+Case' : ⟨ A ==> C ⟩ -> ⟨ B ==> C ⟩ -> ⟨ (A ⊎p B) ==> C ⟩
+Case' f g = record {
+  f = λ { (inl a) → MonFun.f f a ; (inr b) → MonFun.f g b} ;
+  isMon = λ { {inl a1} {inl a2} a1≤a2 → isMon f (lower a1≤a2) ;
+              {inr b1} {inr b2} b1≤b2 → isMon g (lower b1≤b2) } }
+
+Case : ⟨ (A ==> C) ==> (B ==> C) ==> ((A ⊎p B) ==> C) ⟩
+Case = {!!}
+
+-- Lifting a monotone function functorially
+_~->_ : {A B C D : Poset ℓ ℓ'} ->
+    ⟨ A ==> B ⟩ -> ⟨ C ==> D ⟩ -> ⟨ (B ==> C) ==> (A ==> D) ⟩
+pre ~-> post = {!!}
+  -- λ f -> mCompU post (mCompU f pre)
+
+
+
+  -- Monotone successor function
+mSuc : ⟨ ℕ ==> ℕ ⟩
+mSuc = record {
+    f = suc ;
+    isMon = λ {n1} {n2} n1≤n2 -> λ i -> suc (n1≤n2 i) }
+
+
+  -- Combinators
+
+U : ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+U f = MonFun.f f
+
+S : (Γ : Poset ℓΓ ℓ'Γ) ->
+    ⟨ Γ ×p A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+S Γ f g =
+    record {
+      f = λ γ -> MonFun.f f (γ , (U g γ)) ;
+      isMon = λ {γ1} {γ2} γ1≤γ2 ->
+        MonFun.isMon f (γ1≤γ2 , (MonFun.isMon g γ1≤γ2)) }
+
+
+_!_<*>_ :
+    (Γ : Poset ℓ ℓ') -> ⟨ Γ ×p A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+Γ ! f <*> g = S Γ f g
+
+
+K : (Γ : Poset ℓ ℓ') -> {A : Poset ℓ ℓ'} -> ⟨ A ⟩ -> ⟨ Γ ==> A ⟩
+K _ {A} = λ a → record {
+    f = λ γ → a ;
+    isMon = λ {a1} {a2} a1≤a2 → reflexive A a }
+
+
+Id : {A : Poset ℓ ℓ'} -> ⟨ A ==> A ⟩
+Id = record { f = id ; isMon = λ x≤y → x≤y }
+
+
+Curry :  ⟨ (Γ ×p A) ==> B ⟩ -> ⟨ Γ ==> A ==> B ⟩
+Curry {Γ = Γ} {A = A} g = record {
+    f = λ γ →
+      record {
+        f = λ a → MonFun.f g (γ , a) ;
+        -- For a fixed γ, f as defined directly above is monotone
+        isMon = λ {a} {a'} a≤a' → MonFun.isMon g (reflexive Γ _ , a≤a') } ;
+
+    -- The outer f is monotone in γ
+    isMon = λ {γ} {γ'} γ≤γ' → λ a -> MonFun.isMon g (γ≤γ' , reflexive A a) }
+
+Lambda :  ⟨ ((Γ ×p A) ==> B) ==> (Γ ==> A ==> B) ⟩
+Lambda {Γ = Γ} {A = A} = record {
+  f = Curry ;
+  isMon = λ {f1} {f2} f1≤f2 γ a → f1≤f2 ((γ , a)) }
+
+
+
+Uncurry : ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×p A) ==> B ⟩
+Uncurry f = record {
+    f = λ (γ , a) → MonFun.f (MonFun.f f γ) a ;
+    isMon = λ {(γ1 , a1)} {(γ2 , a2)} (γ1≤γ2 , a1≤a2) ->
+      let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+        ≤mon→≤mon-het (MonFun.f f γ1) (MonFun.f f γ2) fγ1≤fγ2 a1 a2 a1≤a2 }
+
+
+App : ⟨ ((A ==> B) ×p A) ==> B ⟩
+App = Uncurry Id
+
+
+Swap : (Γ : Poset ℓ ℓ') -> {A B : Poset ℓ ℓ'} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ A ==> Γ ==> B ⟩
+Swap Γ f = record {
+    f = λ a →
+      record {
+        f = λ γ → MonFun.f (MonFun.f f γ) a ;
+        isMon = λ {γ1} {γ2} γ1≤γ2 ->
+          let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+          ≤mon→≤mon-het _ _ fγ1≤fγ2 a a (reflexive _ a) } ;
+    isMon = λ {a1} {a2} a1≤a2 ->
+      λ γ -> {!!} } 
+
+
+SwapPair : ⟨ (A ×p B) ==> (B ×p A) ⟩
+SwapPair = record {
+  f = λ { (a , b) -> b , a } ;
+  isMon = λ { {a1 , b1} {a2 , b2} (a1≤a2 , b1≤b2) → b1≤b2 , a1≤a2} }
+
+
+-- Apply a monotone function to the first or second argument of a pair
+
+With1st :
+    ⟨ Γ ==> B ⟩ -> ⟨ Γ ×p A ==> B ⟩
+-- ArgIntro1 {_} {A} f = Uncurry (Swap A (K A f))
+With1st {_} {A} f = mCompU f π1
+
+With2nd :
+    ⟨ A ==> B ⟩ -> ⟨ Γ ×p A ==> B ⟩
+With2nd f = mCompU f π2
+-- ArgIntro2 {Γ} f = Uncurry (K Γ f)
+
+
+IntroArg' :
+    ⟨ Γ ==> B ⟩ -> ⟨ B ==> B' ⟩ -> ⟨ Γ ==> B' ⟩
+IntroArg' {Γ = Γ} {B = B} {B' = B'} fΓB fBB' = S Γ (With2nd fBB') fΓB
+
+IntroArg : {Γ B B' : Poset ℓ ℓ'} ->
+  ⟨ B ==> B' ⟩ -> ⟨ (Γ ==> B) ==> (Γ ==> B') ⟩
+IntroArg f = Curry (mCompU f App)
+
+{-
+IntroArg1' : {Γ Γ' B : Poset ℓ ℓ'} ->
+    ⟨ Γ' ==> Γ ⟩ -> ⟨ Γ ==> B ⟩ -> ⟨ Γ' ==> B ⟩
+IntroArg1' f = {!!}
+-}
+
+
+PairAssocLR :
+  ⟨ A ×p B ×p C ==> A ×p (B ×p C) ⟩
+PairAssocLR = record {
+  f = λ { ((a , b) , c) → a , (b , c) } ;
+  isMon = λ { {(a1 , b1) , c1} {(a2 , b2) , c2} ((a1≤a2 , b1≤b2) , c1≤c2) →
+    a1≤a2 , (b1≤b2 , c1≤c2)} }
+
+PairAssocRL :
+ ⟨ A ×p (B ×p C) ==> A ×p B ×p C ⟩
+PairAssocRL = record {
+  f =  λ { (a , (b , c)) -> (a , b) , c } ;
+  isMon = λ { {a1 , (b1 , c1)} {a2 , (b2 , c2)} (a1≤a2 , (b1≤b2 , c1≤c2)) →
+    (a1≤a2 , b1≤b2) , c1≤c2} }
+
+{-
+PairCong :
+  ⟨ A ==> A' ⟩ -> ⟨ (Γ ×p A) ==> (Γ ×p A') ⟩
+PairCong f = {!!}
+-}
+{-
+record {
+  f = λ { (γ , a) → γ , (f $ a)} ;
+  isMon = λ { {γ1 , a1} {γ2 , a2} (γ1≤γ2 , a1≤a2) → γ1≤γ2 , isMon f a1≤a2 }}
+-}
+
+TransformDomain :
+    ⟨ Γ ×p A ==> B ⟩ ->
+    ⟨ ( A ==> B ) ==> ( A' ==> B ) ⟩ ->
+    ⟨ Γ ×p A' ==> B ⟩
+TransformDomain fΓ×A->B f = Uncurry (IntroArg' (Curry fΓ×A->B) f)
+
+
+
+-- Convenience versions of comp, ext, and ret using combinators
+
+mComp' : (Γ : Poset ℓΓ ℓ'Γ) ->
+    ⟨ (Γ ×p B ==> C) ⟩ -> ⟨ (Γ ×p A ==> B) ⟩ -> ⟨ (Γ ×p A ==> C) ⟩
+mComp' Γ f g = record {
+  f = λ { (γ , a) → MonFun.f f (γ , (MonFun.f g (γ , a)))} ;
+  isMon = {!!} }
+  {- S {!!} (mCompU f aux) g
+    where
+      aux : ⟨ Γ ×p A ×p B ==> Γ ×p B ⟩
+      aux = mCompU π1 (mCompU (mCompU PairAssocRL (PairCong SwapPair)) PairAssocLR)
+
+      aux2 : ⟨ Γ ×p B ==> C ⟩ -> ⟨ Γ ×p A ×p B ==> C ⟩
+      aux2 h = mCompU f aux -}
+
+_∘m_ :
+   ⟨ (Γ ×p B ==> C) ⟩ -> ⟨ (Γ ×p A ==> B) ⟩ -> ⟨ (Γ ×p A ==> C) ⟩
+_∘m_ {Γ = Γ} = mComp' Γ
+
+_$_∘m_ :  (Γ : Poset ℓ ℓ') -> {A B C : Poset ℓ ℓ'} ->
+    ⟨ (Γ ×p B ==> C) ⟩ -> ⟨ (Γ ×p A ==> B) ⟩ -> ⟨ (Γ ×p A ==> C) ⟩
+Γ $ f ∘m g = mComp' Γ f g
+infixl 20 _∘m_
+
+Comp : (Γ : Poset ℓ ℓ') -> {A B C : Poset ℓ ℓ'} ->
+    ⟨ Γ ×p B ==> C ⟩ -> ⟨ Γ ×p A ==> B ⟩ -> ⟨ Γ ×p A ==> C ⟩
+Comp Γ f g = {!!}
+
+
+
+
+module Clocked (k : Clock) where
+  private
+    ▹_ : Type ℓ → Type ℓ
+    ▹_ A = ▹_,_ k A
+
+  open import Semantics.Lift k
+  open import Semantics.Concrete.MonotonicityProofs k
+  open import Semantics.LockStepErrorOrdering k
+  open LiftPoset
+
+
+  -- map and ap functions for later as monotone functions
+  Map▹ :
+    ⟨ A ==> B ⟩ -> ⟨ ▸''_ k A ==> ▸''_ k B ⟩
+  Map▹ {A} {B} f = record {
+    f = map▹ (MonFun.f f) ;
+    isMon = λ {a1} {a2} a1≤a2 t → isMon f (a1≤a2 t) }
+
+  Ap▹ :
+    ⟨ (▸''_ k (A ==> B)) ==> (▸''_ k A ==> ▸''_ k B) ⟩
+  Ap▹ {A = A} {B = B} = record { f = UAp▹ ; isMon = UAp▹-mon }
+    where
+      UAp▹ :
+        ⟨ ▸''_ k (A ==> B) ⟩ -> ⟨ ▸''_ k A ==> ▸''_ k B ⟩
+      UAp▹ f~ = record {
+        f = _⊛_ λ t → MonFun.f (f~ t) ;
+        isMon = λ {a1} {a2} a1≤a2 t → isMon (f~ t) (a1≤a2 t) }
+
+      UAp▹-mon : {f1~ f2~ : ▹ ⟨ A ==> B ⟩} ->
+        ▸ (λ t -> rel (A ==> B) (f1~ t) (f2~ t)) ->
+        rel ((▸''_ k A) ==> (▸''_ k B)) (UAp▹ f1~) (UAp▹ f2~)
+      UAp▹-mon {f1~} {f2~} f1~≤f2~ a~ t = f1~≤f2~ t (a~ t)
+
+
+
+  Next : {A : Poset ℓ ℓ'} ->
+    ⟨ A ==> ▸''_ k A ⟩
+  Next = record { f = next ; isMon = λ {a1} {a2} a1≤a2 t → a1≤a2 }
+
+
+  -- 𝕃's return as a monotone function
+  mRet : {A : Poset ℓ ℓ'} -> ⟨ A ==> 𝕃 A ⟩
+  mRet {A = A} = record { f = ret ; isMon = ord-η-monotone A }
+
+
+  -- Delay on Lift as a monotone function
+  Δ : {A : Poset ℓ ℓ'} -> ⟨ 𝕃 A ==> 𝕃 A ⟩
+  Δ {A = A} = record { f = δ ; isMon = λ x≤y → ord-δ-monotone A x≤y }
+
+
+  -- Extending a monotone function to 𝕃
+  mExtU : MonFun A (𝕃 B) -> MonFun (𝕃 A) (𝕃 B)
+  mExtU f = record {
+      f = λ la -> bind la (MonFun.f f) ;
+      isMon = monotone-bind-mon f }
+
+  mExt : ⟨ (A ==> 𝕃 B) ==> (𝕃 A ==> 𝕃 B) ⟩
+  mExt {A = A} = record {
+      f = mExtU ;
+      isMon = λ {f1} {f2} f1≤f2 la →
+        ext-monotone (MonFun.f f1) (MonFun.f f2)
+          (≤mon→≤mon-het f1 f2 f1≤f2) la la (reflexive (𝕃 A) la) }
+
+  mExt' : (Γ : Poset ℓ ℓ') ->
+      ⟨ (Γ ×p A ==> 𝕃 B) ⟩ -> ⟨ (Γ ×p 𝕃 A ==> 𝕃 B) ⟩
+  mExt' Γ f = TransformDomain f mExt
+
+  mRet' : (Γ : Poset ℓ ℓ') -> { A : Poset ℓ ℓ'} -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> 𝕃 A ⟩
+  mRet' Γ f = record { f = λ γ -> ret (MonFun.f f γ) ; isMon = {!!} } -- _ ! K _ mRet <*> a
+
+  Bind : (Γ : Poset ℓ ℓ') ->
+      ⟨ Γ ==> 𝕃 A ⟩ -> ⟨ Γ ×p A ==> 𝕃 B ⟩ -> ⟨ Γ ==> 𝕃 B ⟩
+  Bind Γ la f = S Γ (mExt' Γ f) la
+
+
+
+
+  -- Mapping a monotone function
+  mMap : ⟨ (A ==> B) ==> (𝕃 A ==> 𝕃 B) ⟩
+  mMap {A = A} {B = B} = Curry (mExt' (A ==> B) ((With2nd mRet) ∘m App))
+  -- Curry (mExt' {!!} {!!}) -- mExt' (mComp' (Curry {!!}) {!!}) -- mExt (mComp mRet f)
+
+
+  mMap' :
+      ⟨ (Γ ×p A ==> B) ⟩ -> ⟨ (Γ ×p 𝕃 A ==> 𝕃 B) ⟩
+  mMap' f = record {
+    f = λ { (γ , la) -> mapL (λ a -> MonFun.f f (γ , a)) la} ;
+    isMon = {!!} }
+
+  Map :
+      ⟨ (Γ ×p A ==> B) ⟩ -> ⟨ (Γ ==> 𝕃 A) ⟩ -> ⟨ (Γ ==> 𝕃 B) ⟩
+  Map {Γ = Γ} f la = S Γ (mMap' f) la -- Γ ! mMap' f <*> la
+
+
+  {-
+  -- Montone function between function spaces
+  mFun : {A A' B B' : Poset ℓ ℓ'} ->
+    MonFun A' A ->
+    MonFun B B' ->
+    MonFun (arr' A B) (arr' A' B')
+  mFun fA'A fBB' = record {
+    f = λ fAB → {!!} ; --  mComp (mComp fBB' fAB) fA'A ;
+    isMon = λ {fAB-1} {fAB-2} fAB-1≤fAB-2 →
+      λ a'1 a'2 a'1≤a'2 ->
+        MonFun.isMon fBB'
+          (fAB-1≤fAB-2
+            (MonFun.f fA'A a'1)
+            (MonFun.f fA'A a'2)
+            (MonFun.isMon fA'A a'1≤a'2))}
+
+  -- NTS :
+  -- In the space of monotone functions from A' to B', we have
+  -- mComp (mComp fBB' f1) fA'A) ≤ (mComp (mComp fBB' f2) fA'A)
+  -- That is, given a'1 and a'2 of type ⟨ A' ⟩ with a'1 ≤ a'2 we
+  -- need to show that
+  -- (fBB' ∘ fAB-1 ∘ fA'A)(a'1) ≤ (fBB' ∘ fAB-2 ∘ fA'A)(a'2)
+  -- By monotonicity of fBB', STS that
+  -- (fAB-1 ∘ fA'A)(a'1) ≤  (fAB-2 ∘ fA'A)(a'2)
+  -- which follows by assumption that fAB-1 ≤ fAB-2 and monotonicity of fA'A
+  -}
+
+
+    -- Embedding of function spaces is monotone
+  mFunEmb : (A A' B B' : Poset ℓ ℓ') ->
+      ⟨ A' ==> 𝕃 A ⟩ ->
+      ⟨ B ==> B' ⟩ ->
+      ⟨ (A ==> 𝕃 B) ==> (A' ==> 𝕃 B') ⟩
+  mFunEmb A A' B B' fA'LA fBB' =
+      Curry (Bind ((A ==> 𝕃 B) ×p A')
+        (mCompU fA'LA π2)
+        (Map (mCompU fBB' π2) ({!!})))
+    --  _ $ (mExt' _ (_ $ (mMap' (K _ fBB')) ∘m Id)) ∘m (K _ fA'LA)
+    -- mComp' (mExt' (mComp' (mMap' (K fBB')) Id)) (K fA'LA)
+
+  mFunProj : (A A' B B' : Poset ℓ ℓ') ->
+     ⟨ A ==> A' ⟩ ->
+     ⟨ B' ==> 𝕃 B ⟩ ->
+     ⟨ (A' ==> 𝕃 B') ==> 𝕃 (A ==> 𝕃 B) ⟩
+  mFunProj A A' B B' fAA' fB'LB = {!!}
+    -- mRet' (mExt' (K fB'LB) ∘m Id ∘m (K fAA'))
+