update representableRelation

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

@@ -35,6 +35,7 @@ open import Cubical.Relation.Binary.Poset
 open import Common.Poset.Convenience
 open import Common.Poset.Constructions
 open import Common.Poset.Monotone
+open import Common.Poset.MonotoneRelation
 open import Semantics.MonotoneCombinators
 
 open import Semantics.LockStepErrorOrdering k
@@ -45,12 +46,15 @@ open ClockedCombinators k
 
 private
   variable
-    ℓ ℓ' : Level
+    ℓ ℓ' ℓX ℓX' : Level
 
   ▹_ : Type ℓ → Type ℓ
   ▹_ A = ▹_,_ k A
 
 
+
+
+
 -- Can have type Poset ℓ ℓ
 DynP' : (D : ▹ Poset ℓ-zero ℓ-zero) -> Poset ℓ-zero ℓ-zero
 DynP' D = ℕ ⊎p (▸' k (λ t → D t ==> 𝕃 (D t)))
@@ -67,7 +71,8 @@ unfold-⟨DynP⟩ = λ i → ⟨ unfold-DynP i ⟩
 DynP-Sum : DynP ≡ ℕ ⊎p ((▸'' k) (DynP ==> 𝕃 DynP))
 DynP-Sum = unfold-DynP
 
-
+⟨DynP⟩-Sum : ⟨ DynP ⟩ ≡ Nat ⊎ (▹ (⟨ DynP ==> 𝕃 DynP ⟩)) -- MonFun DynP (𝕃 DynP)
+⟨DynP⟩-Sum i = ⟨ DynP-Sum i ⟩
 
 InjNat : ⟨ ℕ ==> DynP ⟩
 InjNat = mCompU (mTransport (sym DynP-Sum)) σ1
@@ -78,14 +83,35 @@ InjArr = mCompU (mTransport (sym DynP-Sum)) (mCompU σ2 Next)
 ProjNat : ⟨ DynP ==> 𝕃 ℕ ⟩
 ProjNat = mCompU (Case' mRet (K _ ℧)) (mTransport DynP-Sum)
 
-ProjArr : ⟨ DynP ==> 𝕃 (DynP ==> 𝕃 DynP) ⟩
-ProjArr = {!!}
-
-
 
+▹g→g : MonFun ((▸'' k) (DynP ==> 𝕃 DynP)) (𝕃 (DynP ==> 𝕃 DynP))
+▹g→g = record {
+   f = λ f~ -> θ (λ t -> η (f~ t)) ;
+   isMon = λ {f~} {g~} f~≤g~ → ord-θ-monotone _ (λ t -> ord-η-monotone _ (f~≤g~ t))
+        -- ord-θ-monotone _ (λ t -> ord-η-monotone _ (f~≤g~ t))
+   }
 
+ProjArr : ⟨ DynP ==> 𝕃 (DynP ==> 𝕃 DynP) ⟩
+ProjArr = mCompU (Case' (K _ ℧) ▹g→g) (mTransport DynP-Sum)
+ 
+    
+
+ProjArr-fun : ∀ d g~ ->
+  transport ⟨DynP⟩-Sum d ≡ inr g~ ->
+  MonFun.f ProjArr d ≡ θ (λ t -> η (g~ t))
+ProjArr-fun d g~ eq = {!!} ∙
+  -- (λ i -> MonFun.f (mCompU (Case' (K _ ℧) aux) (mTransport DynP-Sum)) d) ∙
+  (congS ((λ { (inl a) → MonFun.f (K ℕ ℧) a
+             ; (inr b) → MonFun.f ▹g→g b
+         })) eq) ∙
+  {!!}
+-- MonFun.f ProjArr d ≡ θ (λ t → η (g~ t))
+
+-- (transp (λ i → ⟨ DynP-Sum i ⟩) i0 d)
+-- transport ⟨DynP⟩-Sum d ≡ inr g~
 {-
 
+-- MonFun.f ( mCompU (Case' (K _ ℧) _) (mTransport DynP-Sum)) ?) ∙ ?
 
 data Dyn' (D : ▹ Poset ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
   nat : Nat -> Dyn' D

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

@@ -35,7 +35,7 @@ open import Common.Poset.Constructions
 private
   variable
     ℓ ℓ' : Level
-    ℓR1 ℓR2 : Level
+    ℓR ℓR1 ℓR2 : Level
     ℓA ℓ'A ℓA' ℓ'A' ℓB ℓ'B ℓB' ℓ'B' : Level
     A :  Poset ℓA ℓ'A
     A' : Poset ℓA' ℓ'A'
@@ -104,6 +104,92 @@ module ClockedProofs (k : Clock) where
   ret-monotone-het {A = A} {A' = A'} rAA' = λ a a' a≤a' →
     LiftRelation.Properties.ord-η-monotone ⟨ A ⟩ ⟨ A' ⟩ rAA' a≤a'
 
+  ret-monotone : {A : Poset ℓA ℓ'A} ->
+    (a a' : ⟨ A ⟩) ->
+    (rAA : ⟨ A ⟩ -> ⟨ A ⟩ -> Type ℓR) ->
+    rel (𝕃 A) (ret a) (ret a')
+  ret-monotone = {!!}
+
+  _×rel_ : {A : Type ℓA} {A' : Type ℓA'} {B : Type ℓB} {B' : Type ℓB'} ->
+    (R : A -> A' -> Type ℓR1) -> (S : B -> B' -> Type ℓR2) ->
+    (p : A × B) -> (p' : A' × B') -> Type (ℓ-max ℓR1 ℓR2)
+  (R ×rel S) (a , b) (a' , b') = R a a' × S b b' --R a a' , S b b' won't work
+
+  lift×-monotone-het : {A : Poset ℓA ℓ'A} {A' : Poset ℓA' ℓ'A'}
+    {B : Poset ℓB ℓ'B} {B' : Poset ℓB' ℓ'B'} ->
+    (R : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type ℓR1) ->
+    (S : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type ℓR2) ->
+    (lab : ⟨ 𝕃 (A ×p B) ⟩) -> (la'b' : ⟨ 𝕃 (A' ×p B') ⟩) ->
+    (_ LiftRelation.≾ _) (R ×rel S) lab la'b' ->
+    ((_ LiftRelation.≾ _) R ×rel (_ LiftRelation.≾ _) S) (lift× lab) (lift× la'b')
+  lift×-monotone-het {A = A} {A' = A'} {B = B} {B' = B'} R S lab la'b' lab≤la'b' =
+    let fixed = fix monotone-lift×' in
+    transport {!!} {!!}
+    where
+      _≾'LA_  = LiftPoset._≾'_ A
+      _≾'LA'_ = LiftPoset._≾'_ A'
+      _≾'LB_  = LiftPoset._≾'_ B
+      _≾'LB'_ = LiftPoset._≾'_ B'
+
+      module LiftP' = LiftRelation (⟨ A ⟩ × ⟨ B ⟩) (⟨ A' ⟩ × ⟨ B' ⟩) (R ×rel S)
+      module LiftP1' = LiftRelation ⟨ A ⟩ ⟨ A' ⟩ R
+      module LiftP2' = LiftRelation ⟨ B ⟩ ⟨ B' ⟩ S
+
+      _≾'P'_ = LiftP'.Inductive._≾'_ (next LiftP'._≾_)
+      _≾'P1'_ = LiftP1'.Inductive._≾'_ (next LiftP1'._≾_)
+      _≾'P2'_ = LiftP2'.Inductive._≾'_ (next LiftP2'._≾_)
+
+      monotone-lift×' :
+        ▹ ((lab : ⟨ 𝕃 (A ×p B) ⟩) -> (la'b' : ⟨ 𝕃 (A' ×p B') ⟩) ->
+          lab ≾'P' la'b' ->
+          (lift×' (next lift×) lab .fst ≾'P1' {!!}) × ({!!} ≾'P2' {!!})) ->
+          -- {!? ≾'P1' ?!} × {! ? ≾'P2' ?!}) ->
+        (lab : ⟨ 𝕃 (A ×p B) ⟩) -> (la'b' : ⟨ 𝕃 (A' ×p B') ⟩) ->
+          lab ≾'P' la'b' ->
+          {!!}
+      monotone-lift×' = {!!}
+
+--todo: follow ext-monotone-het
+  lift×-inv-monotone-het : {A : Poset ℓA ℓ'A} {A' : Poset ℓA' ℓ'A'}
+    {B : Poset ℓB ℓ'B} {B' : Poset ℓB' ℓ'B'} ->
+    (R : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type ℓR1) ->
+    (S : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type ℓR2) ->
+    (lalb : ⟨ 𝕃 A ×p 𝕃 B ⟩) -> (la'lb' : ⟨ 𝕃 A' ×p 𝕃 B' ⟩) ->
+    ((_ LiftRelation.≾ _) R ×rel (_ LiftRelation.≾ _) S) lalb la'lb' ->
+    (_ LiftRelation.≾ _) (R ×rel S) (lift×-inv lalb) (lift×-inv la'lb')
+  lift×-inv-monotone-het {A = A} {A' = A'} {B = B} {B' = B'} R S p p' (la≤la' , lb≤lb') =
+    let fixed = fix monotone-lift×-inv' in
+    transport
+      (sym (λ i -> LiftP'.unfold-≾ i (unfold-lift×-inv i p) (unfold-lift×-inv i p')))
+      (fixed p p' ((transport (λ i → LiftP1'.unfold-≾ i (p .fst) (p' .fst)) la≤la')
+                  , transport (λ i → LiftP2'.unfold-≾ i (p .snd) (p' .snd)) lb≤lb'))
+    where
+      _≾'LA_  = LiftPoset._≾'_ A
+      _≾'LA'_ = LiftPoset._≾'_ A'
+      _≾'LB_  = LiftPoset._≾'_ B
+      _≾'LB'_ = LiftPoset._≾'_ B'
+
+      module LiftP' = LiftRelation (⟨ A ⟩ × ⟨ B ⟩) (⟨ A' ⟩ × ⟨ B' ⟩) (R ×rel S)
+      module LiftP1' = LiftRelation ⟨ A ⟩ ⟨ A' ⟩ R
+      module LiftP2' = LiftRelation ⟨ B ⟩ ⟨ B' ⟩ S
+
+      _≾'P'_ = LiftP'.Inductive._≾'_ (next LiftP'._≾_)
+      _≾'P1'_ = LiftP1'.Inductive._≾'_ (next LiftP1'._≾_)
+      _≾'P2'_ = LiftP2'.Inductive._≾'_ (next LiftP2'._≾_)
+      monotone-lift×-inv' :
+        ▹ ((p : ⟨ 𝕃 A ×p 𝕃 B ⟩) -> (p' : ⟨ 𝕃 A' ×p 𝕃 B' ⟩) ->
+          ((p .fst ≾'P1' p' .fst) × (p .snd ≾'P2' p' .snd)) ->
+          lift×-inv' (next lift×-inv) p ≾'P' lift×-inv' (next lift×-inv) p') ->
+        (p : ⟨ 𝕃 A ×p 𝕃 B ⟩) -> (p' : ⟨ 𝕃 A' ×p 𝕃 B' ⟩) ->
+          ((p .fst ≾'P1' p' .fst) × (p .snd ≾'P2' p' .snd)) ->
+          lift×-inv' (next lift×-inv) p ≾'P' lift×-inv' (next lift×-inv) p'
+      monotone-lift×-inv' IH (η a , η b) (η a' , η b') (la≤la' , lb≤lb') = transport (λ i → LiftP'.unfold-≾ i {!lift×-inv (η a , η b )!} {!!}) {!!}
+      monotone-lift×-inv' IH ((η a) , (θ lb~)) ((η a') , (θ lb'~)) (la≤la' , lb≤lb') = {!!}
+      monotone-lift×-inv' IH (℧ , _) (℧ , _) (la≤la' , lb≤lb') = {!!}
+      monotone-lift×-inv' IH (_ , ℧) (_ , ℧) (la≤la' , lb≤lb') = {!!}
+      monotone-lift×-inv' IH ((θ la~) , lb) (la' , lb') (la≤la' , lb≤lb') = {!!}
+      monotone-lift×-inv' IH p p' p≤p' = {!!}
+ 
   -- 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) ->
@@ -148,11 +234,11 @@ module ClockedProofs (k : Clock) where
           (la ≾'LALA' la') ->
           (ext' f  (next (ext f))  la) ≾'LBLB'
           (ext' f' (next (ext f')) la')
-      monotone-ext' IH (η x) (η y) x≤y =
-        transport
+      monotone-ext' IH (η x) (η y) x≤y = transport (λ i → LiftBB'.unfold-≾ i (f x) (f' y)) (f≤f' 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*
+        (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
@@ -173,7 +259,18 @@ module ClockedProofs (k : Clock) where
     rel (𝕃 B) (ext f la) (ext f' la')
   ext-monotone {A} {B} f f' f≤f' la la' la≤la' = {!!}
 
-
+  lift×-monotone : {A : Poset ℓA ℓ'A} {B : Poset ℓB ℓ'B} ->
+    (l l' : ⟨ 𝕃 (A ×p B) ⟩) ->
+    rel (𝕃 (A ×p B)) l l' ->
+    rel (𝕃 A ×p 𝕃 B) (lift× l) (lift× l')
+  lift×-monotone = {!!}
+
+  lift×-inv-monotone : {A : Poset ℓA ℓ'A} {B : Poset ℓB ℓ'B} ->
+    (l l' : ⟨ 𝕃 A ×p 𝕃 B ⟩) ->
+    rel (𝕃 A ×p 𝕃 B) l l' ->
+    rel (𝕃 (A ×p B)) (lift×-inv l) (lift×-inv l')
+  lift×-inv-monotone = {!!} 
+  
   bind-monotone :
     {la la' : ⟨ 𝕃 A ⟩} ->
     (f f' : ⟨ A ⟩ -> ⟨ (𝕃 B) ⟩) ->

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

@@ -11,6 +11,8 @@ module Semantics.Concrete.RepresentableRelation (k : Clock) where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Structure
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum hiding (elim)
 
 open import Cubical.HITs.PropositionalTruncation
 
@@ -32,7 +34,7 @@ open import Semantics.LockStepErrorOrdering k
 open import Semantics.Concrete.DynNew k
 
 
-open LiftPoset
+open LiftPoset using (𝕃)
 open ClockedCombinators k
 open ClockedProofs k
 
@@ -43,6 +45,10 @@ private
     ℓX' ℓ'X' ℓY' ℓ'Y' : Level
     ℓR ℓR' : Level
 
+private
+  ▹_ : Type ℓ → Type ℓ
+  ▹_ A = ▹_,_ k A
+
 ----------------------------------
 -- Left pseudo-representation
 ----------------------------------
@@ -127,8 +133,9 @@ IdRepRel X .rightRep = record {
   p = MonId ;
   δX = MonId ;
   δY = MonId ;
-  dnR = λ lx ly lx≤ly → {!!} ;
-  dnL = λ lx ly lx≤ly → {!!} }
+  dnR = λ lx lx' lx≤lx' → {!!};
+  dnL = λ lx lx' lx≤lx' → {!MonRel.R !} }
+  -- How to construct a relation?
 
 
 -- "Product" of pseudo-representable relations
@@ -138,19 +145,40 @@ RepRel× : {X : Poset ℓX ℓ'X} {X' : Poset ℓX' ℓ'X'}
   RepresentableRel Y Y' ℓR' ->
   RepresentableRel (X ×p Y) (X' ×p Y') (ℓ-max ℓR ℓR')
 RepRel× c d .R = c .R ×monrel d .R
-RepRel× c d .leftRep = record {
-  e = {!!} ;
-  δX = {!!} ;
-  δY = {!!} ;
-  UpL = {!!} ;
-  UpR = {!!} }
-RepRel× c d .rightRep = record {
-  p = {!!} ;
-  δX = {!!} ;
-  δY = {!!} ;
-  dnR = {!!} ;
-  dnL = {!!} }
+RepRel× {X = X} {X' = X'} {Y = Y} {Y' = Y'} c d .leftRep = record {
+  e = PairFun (With1st (c .leftRep .e)) (With2nd (d .leftRep .e)) ;
+  δX = PairFun (With1st (c .leftRep .δX)) (With2nd (d .leftRep .δX)) ;
+  δY = PairFun (With1st (c .leftRep .δY)) (With2nd (d .leftRep .δY)) ;
+  UpL = λ (x , y) (x' , y') (p1 , p2) → c .leftRep .UpL x x' p1 , d .leftRep .UpL y y' p2 ;
+  UpR = λ (x , y) (x' , y') (p1 , p2) → c .leftRep .UpR x x' p1 , d .leftRep .UpR y y' p2 }
+{- (X' .snd PosetStr.≤
+       MonFun.f (With1st (c .leftRep .e)) .patternInTele0) x'-}
+RepRel× {X = X} {X' = X'} {Y = Y} {Y' = Y'} c d .rightRep = record {
+  p = mCompU (mCompU (mLift×p' X Y)
+             (PairFun (With1st (c .rightRep .p)) (With2nd (d .rightRep .p))))
+             (mLift×p X' Y') ;
+  δX = mCompU (mCompU (mLift×p' X Y)
+              (PairFun (With1st (c .rightRep .δX)) (With2nd (d .rightRep .δX))))
+              (mLift×p X Y) ;
+  δY = mCompU (mCompU (mLift×p' X' Y')
+              (PairFun (With1st (c .rightRep .δY)) (With2nd (d .rightRep .δY))))
+              (mLift×p X' Y') ;
+  dnR = λ l l' l≤l' → lift×-inv-monotone _ _
+    ((c .rightRep .dnR _ _
+      (lift×-monotone-het _ _ l l'
+      l≤l' .fst))
+    , (d .rightRep .dnR _ _
+        (lift×-monotone-het _ _ l l'
+        l≤l' .snd))) ;
+  dnL = λ l l' l≤l' → lift×-inv-monotone-het _ _ _ _ 
+    (c .rightRep .dnL _ _
+      (lift×-monotone l l' l≤l' .fst)
+    , d .rightRep .dnL _ _
+      (lift×-monotone l l' l≤l' .snd)) }
 
+{-
+(LX' × LY' → LX)  ->  (LX' × LY' → LY) -> 
+-}
 
 --
 -- Lifting pseudo-representable relations to a pseudo-representable relation
@@ -186,8 +214,7 @@ RepFun {Ai = Ai} {Ao = Ao} {Bi = Bi} {Bo = Bo} ci co .leftRep =
     With2nd (mCompU (ci .rightRep .δY) mRet) ∘m
     π2) ;
   
-  UpL = λ f g f≤g bi ->
-    mapL-monotone-het _ _
+  UpL = λ f g f≤g bi -> mapL-monotone-het _ _
     (MonFun.f (co .leftRep .e))
     (MonFun.f (co .leftRep .δY))
     (co .leftRep .UpL) _ _
@@ -203,12 +230,22 @@ RepFun {Ai = Ai} {Ao = Ao} {Bi = Bi} {Bo = Bo} ci co .leftRep =
       _ _ (bind-monotone (MonFun.f f) (MonFun.f g)
         (ci .rightRep .dnR _ _ (ret-monotone-het _ ai bi ai≤bi)) (≤mon→≤mon-het f g f≤g)) }
 
-RepFun ci co .rightRep = record {
-  p = U mMap {!!} ;
-  δX = {!!} ;
-  δY = {!!} ;
-  dnR = {!!} ;
-  dnL = {!!} }
+RepFun {Ai = Ai} {Ao = Ao} {Bi = Bi} {Bo = Bo} ci co .rightRep = record {
+  p = U mMap (Curry (With2nd (co .rightRep .p) ∘m App ∘m With2nd (ci .leftRep .e))) ;
+  δX = U mMap (Curry (With2nd (co .rightRep .δX) ∘m App ∘m With2nd (ci .leftRep .δX))) ;
+  δY = U mMap (Curry (With2nd (co .rightRep .δY) ∘m App ∘m With2nd (ci .leftRep .δY))) ;
+  dnR = λ lf lg lf≤lg → mapL-monotone-het _ _
+    (MonFun.f (Curry (With2nd (co .rightRep .δX) ∘m App ∘m With2nd (ci .leftRep .δX))))
+    (MonFun.f (Curry (With2nd (co .rightRep .p) ∘m App ∘m With2nd (ci .leftRep .e))))
+    (λ f g f≤g ai → co .rightRep .dnR _ _ {!!}) lf lg lf≤lg ; --todo ℓ' != ℓR of type Level
+  dnL = λ lg lg' lg≤lg' → mapL-monotone-het _ _
+    (MonFun.f (Curry (With2nd (co .rightRep .p) ∘m App ∘m With2nd (ci .leftRep .e))))
+    (MonFun.f (Curry (With2nd (co .rightRep .δY) ∘m App ∘m With2nd (ci .leftRep .δY))))
+    (λ g g' g≤g' ai bi ai≤bi → co .rightRep .dnL _ _
+      (≤mon→≤mon-het g g' g≤g' {!!} {!!} {!!}) --(≤mon→≤mon-het g g' g≤g' _ _ (ci .leftRep .UpL ai bi ai≤bi))
+      )
+    lg lg' lg≤lg' }
+
 
 --
 -- Pseudo-representable relations involving Dyn
@@ -232,13 +269,24 @@ injℕ .rightRep = record {
   δX = U mExt mRet ; -- ext ret (which equals id)
   δY = U mExt mRet ;
   dnR = λ ln ld ln≤ld →
-    ext-monotone-het {!!} (rel ℕ) ret (MonFun.f ProjNat)
-    (λ n d n≤d → {!!}) ln ld ln≤ld ;
-  dnL = {!!} }
+    ext-monotone-het (R (injℕ .R)) (rel ℕ) ret (MonFun.f ProjNat)
+    (λ n d n≤d → {!R!}) ln ld ln≤ld ;
+  dnL = λ ld ld' ld≤ld' →
+    ext-monotone-het (rel DynP) (R (injℕ .R)) (MonFun.f ProjNat) ret
+    (λ d d' d≤d' → {!!}) ld ld' ld≤ld' }
+
 
+Rel : ∀ ℓ -> _
+Rel ℓ = functionalRel InjArr Id (poset-monrel {ℓo = ℓ} DynP)
+
+Rel-lem : ∀ f d ℓ -> R (Rel ℓ) f d ->
+  Σ[ g~ ∈ ⟨ ▹' k ((DynP ==> 𝕃 DynP)) ⟩ ]
+    (transport  ⟨DynP⟩-Sum d ≡ inr g~) × (▸ (λ t -> f ≤mon g~ t))
+Rel-lem f d ℓ injA = (transport {!!} {!!}) , ({!!} , {!!})
+--  (λ t → f) , (λ i → {!!}) , (λ t x → reflexive _ d)o
 
 injArr : RepresentableRel (DynP ==> 𝕃 DynP) DynP ℓR
-injArr .R = functionalRel InjArr Id (poset-monrel DynP)
+injArr {ℓR = ℓR} .R = Rel ℓR
 injArr .leftRep = record {
   e = InjArr ;
   δX = Id ;
@@ -246,9 +294,31 @@ injArr .leftRep = record {
   UpL = λ f d f≤d → lower f≤d ;
   UpR = λ f g f≤g → lift (MonFun.isMon InjArr f≤g) }
   
-injArr .rightRep = record { p = ? ; δX = ? ; δY = ? ; dnR = ? ; dnL = ? }
-
-
+injArr {ℓR = ℓR} .rightRep = record {
+  p = mExtU ProjArr ;
+  δX = mExtU (mCompU Δ mRet) ; --@not sure
+  δY = mExtU (mCompU Δ mRet) ;
+  dnR = λ lf ld lf≤ld → ext-monotone-het _ _
+    (MonFun.f (mCompU Δ mRet))
+    (MonFun.f ProjArr)
+    (λ f d f≤d -> aux f d f≤d (Rel-lem f d ℓR f≤d)) lf ld lf≤ld ;
+  dnL = λ ld ld' ld≤ld' → ext-monotone-het _ _
+    (MonFun.f ProjArr)
+    (MonFun.f (mCompU Δ mRet))
+    (λ d d' d≤d' → {!!})
+    ld ld' ld≤ld' }
+
+    where
+      open LiftRelation.Properties
+      aux : ∀ f d f≤d sigma -> 
+       LiftRelation._≾_ ⟨ DynP ==> 𝕃 DynP ⟩ ⟨ DynP ==> 𝕃 DynP ⟩ (rel (DynP ==> 𝕃 DynP))
+        (δ (ret f)) (MonFun.f ProjArr d)
+      aux f d f≤d (g~ , eq-inr , f≤g~) = let eq = ProjArr-fun d g~ eq-inr in
+        transport ((λ i -> LiftRelation._≾_ _ _ (rel (DynP ==> 𝕃 DynP)) (δ (ret f)) (sym eq i)))
+             (ord-θ-monotone ⟨ DynP ==> 𝕃 DynP ⟩ ⟨ DynP ==> 𝕃 DynP ⟩ (rel (DynP ==> 𝕃 DynP))
+                λ t -> ord-η-monotone ⟨ DynP ==> 𝕃 DynP ⟩ ⟨ DynP ==> 𝕃 DynP ⟩ (rel (DynP ==> 𝕃 DynP)) (f≤g~ t))
+     
+-- (λ i -> LiftRelation._≾_ _ _ _ (δ (ret f)) (eq i))
 --
 -- Composing pseudo-representable relations
 -- Note: It is not in general possible to compose arbitrary pseudo-rep
@@ -267,16 +337,16 @@ composeRep : {A B C : Poset ℓ ℓ'} ->
 composeRep c d c-filler-l d-filler-r .R = CompMonRel (c .R) (d .R)
 composeRep {C = C} c d c-filler-l d-filler-r .leftRep = record {
   e = mCompU (d .leftRep .e) (c .leftRep .e) ;
-  δX = {!!} ;
-  δY = {!!} ;
+  δX = c .leftRep .δX;
+  δY = d .leftRep .δY ;
   UpL =  λ x z x≤z -> elim
     (λ _ -> isPropValued-poset C _ _)
     (λ { (y , x≤y , y≤z) -> d .leftRep .UpL _ _
-      (is-antitone (d .R) (c .leftRep .UpL x y x≤y) {!!}) })
-    x≤z  ;
-  UpR = {!!} }
+      (is-antitone (d .R) (c .leftRep .UpL x y x≤y) {!d-filler-r!}) })
+    x≤z ;
+  UpR = λ a a' a≤a' → elim (λ _ -> isPropValued-poset {!!} _ _) {!!} {!!} }
 composeRep c d c-filler-l d-filler-r .rightRep = record {
-  p = {!!} ;
+  p = mCompU (c .rightRep .p) (d .rightRep .p) ;
   δX = {!!} ;
   δY = {!!} ;
   dnR = {!!} ;

formalizations/guarded-cubical/Semantics/Lift.agda

@@ -18,6 +18,7 @@ open import Cubical.Data.Sum
 open import Cubical.Data.Unit renaming (Unit to ⊤)
 open import Cubical.Foundations.Transport
 open import Cubical.Data.Nat hiding (_^_)
+open import Cubical.Data.Sigma
 
 open import Common.Common
 open import Common.LaterProperties
@@ -217,9 +218,6 @@ inj-θ lx~ ly~ H = let lx~≡ly~ = cong pred H in
   λ t i → lx~≡ly~ i t
 
 
-
-
-
 -- Monadic structure
 
 ret : {X : Type ℓ} -> X -> L℧ X
@@ -234,6 +232,28 @@ ext' f rec (θ l-la) = θ (rec ⊛ l-la)
 ext : (A -> L℧ B) -> L℧ A -> L℧ B
 ext f = fix (ext' f)
 
+lift×' : (▹ (L℧ (A × B) -> L℧ A × L℧ B)) -> L℧ (A × B) -> L℧ A × L℧ B
+lift×' rec (η (a , b)) = η a , η b
+lift×' rec ℧ = ℧ , ℧
+lift×' rec (θ l~) = (θ (λ t → rec t (l~ t) .fst)) , θ (λ t -> rec t (l~ t) .snd)
+
+lift× : {A : Type ℓ} {B : Type ℓ'} -> L℧ (A × B) -> L℧ A × L℧ B
+lift× {A = A} {B = B} = fix lift×'
+
+lift×-inv' : ▹ (L℧ A × L℧ B -> L℧ (A × B)) -> L℧ A × L℧ B -> L℧ (A × B)
+lift×-inv' rec (η a , η b) = η (a , b)
+lift×-inv' rec (η a , θ l'~) = θ (λ t -> (rec t (η a , l'~ t)))
+lift×-inv' rec (℧ , _) = ℧
+lift×-inv' rec (_ , ℧) = ℧ -- not sure whether it's gray
+lift×-inv' rec (θ l~ , η b) = θ (λ t -> rec t (l~ t , η b))
+lift×-inv' rec (θ l~ , θ l'~) = θ (λ t -> rec t (l~ t , l'~ t))
+
+lift×-inv : {A : Type ℓ} {B : Type ℓ'} -> L℧ A × L℧ B -> L℧ (A × B)
+lift×-inv {A = A} {B = B} = fix lift×-inv'
+
+unfold-lift×-inv : {A : Type ℓ} {B : Type ℓ'} ->
+  lift×-inv {A = A} {B = B} ≡ lift×-inv' (next lift×-inv)
+unfold-lift×-inv = fix-eq lift×-inv'
 
 bind : L℧ A -> (A -> L℧ B) -> L℧ B
 bind {A} {B} la f = ext f la