update PosetWithPtb

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

@@ -20,6 +20,7 @@ open import Cubical.Foundations.Function
 
 open import Cubical.Algebra.Monoid.Base
 open import Cubical.Algebra.Semigroup.Base
+open import Cubical.Algebra.CommMonoid.Base
 
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_ ; _^_)
@@ -56,28 +57,30 @@ isSetMonoid M = M .snd .isMonoid .isSemigroup .is-set
     open IsMonoid
     open IsSemigroup
 
-
-
 monoidId : (M : Monoid ℓ) -> ⟨ M ⟩
 monoidId M = M .snd .ε
   where open MonoidStr
 
-_×M_ : Monoid ℓ -> Monoid ℓ' -> Monoid (ℓ-max ℓ ℓ')
-M1 ×M M2 = makeMonoid
+commMonoidId : (M : CommMonoid ℓ) -> ⟨ M ⟩
+commMonoidId M = M .snd .ε
+  where open CommMonoidStr
+
+_×M_ : CommMonoid ℓ -> CommMonoid ℓ' -> CommMonoid (ℓ-max ℓ ℓ')
+M1 ×M M2 = makeCommMonoid
   {M = ⟨ M1 ⟩ × ⟨ M2 ⟩}
-  (monoidId M1 , monoidId M2)
-  (λ { (m1 , m2) (m1' , m2') -> (m1 ·M1 m1') , (m2 ·M2 m2') })
-  (isSet× (isSetMonoid M1) (isSetMonoid M2))
-  (λ { (m1 , m2) (m1' , m2') (m1'' , m2'') →
-    ≡-× (M1 .snd .isMonoid .isSemigroup .·Assoc m1 m1' m1'') ((M2 .snd .isMonoid .isSemigroup .·Assoc m2 m2' m2'')) })
+  (commMonoidId M1 , commMonoidId M2)
+  (λ { (m1 , m2) (m1' , m2') -> (m1 ·M1 m1') , (m2 ·M2 m2')})
+  (isSet× (isSetCommMonoid M1) (isSetCommMonoid M2))
+  (λ { (m1 , m2) (m1' , m2') (m1'' , m2'') ->
+    ≡-× (M1 .snd .isMonoid .isSemigroup .·Assoc m1 m1' m1'') (M2 .snd .isMonoid .isSemigroup .·Assoc m2 m2' m2'') })
   (λ { (m1 , m2) -> ≡-× (M1 .snd .isMonoid .·IdR m1) ((M2 .snd .isMonoid .·IdR m2)) })
-  (λ { (m1 , m2) -> ≡-× (M1 .snd .isMonoid .·IdL m1) ((M2 .snd .isMonoid .·IdL m2)) })
-   where
-     open MonoidStr
-     open IsMonoid
-     open IsSemigroup
-     _·M1_ = M1 .snd ._·_
-     _·M2_ = M2 .snd ._·_
+  λ { (m1 , m2) (m1' , m2') -> ≡-× (M1 .snd .·Comm m1 m1') (M2 .snd .·Comm m2 m2') }
+    where
+      open CommMonoidStr
+      open IsMonoid
+      open IsSemigroup
+      _·M1_ = M1 .snd ._·_
+      _·M2_ = M2 .snd ._·_
 
 -- Monoid of all monotone endofunctions on a poset
 EndoMonFun : (X : Poset ℓ ℓ') -> Monoid (ℓ-max ℓ ℓ')
@@ -90,8 +93,8 @@ EndoMonFun X = makeMonoid {M = MonFun X X} Id mCompU MonFunIsSet
 record PosetWithPtb (ℓ ℓ' ℓ'' : Level) : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-suc ℓ') (ℓ-suc ℓ''))) where
   field
     P       : Poset ℓ ℓ'
-    Perturb : Monoid ℓ''
-    perturb : MonoidHom Perturb (EndoMonFun P)
+    Perturb : CommMonoid ℓ''
+    perturb : MonoidHom (CommMonoid→Monoid Perturb) (EndoMonFun P) -- Perturb (EndoMonFun P)
     --TODO: needs to be injective map
     -- Perturb : ⟨ EndoMonFun P ⟩
 
@@ -105,33 +108,48 @@ open PosetWithPtb
 _==>PWP_ : PosetWithPtb ℓ ℓ' ℓ'' -> PosetWithPtb ℓ ℓ' ℓ'' -> PosetWithPtb (ℓ-max ℓ ℓ') (ℓ-max ℓ ℓ') ℓ''
 A ==>PWP B = record {
   P = (A .P) ==> (B .P) ;
-  Perturb = A .Perturb ×M B .Perturb ;
+  Perturb = A .Perturb ×M B .Perturb ; -- A .Perturb ×M B .Perturb ;
   perturb =
     (λ { (δᴬ , δᴮ) -> ptb-fun A δᴬ ~-> ptb-fun B δᴮ }) ,
     monoidequiv (eqMon _ _ (funExt (λ g -> let pfA = cong (MonFun.f) (perturb A .snd .presε) in
                                            let pfB = cong (MonFun.f) (perturb B .snd .presε) in
                                            eqMon _ _ λ i -> pfB i ∘ MonFun.f g ∘ pfA i)))
-                (λ ma mb → {!!}) }
+                (λ { (ma , mb) (ma' , mb') → eqMon _ _ (funExt (λ g ->
+                  let pfA = cong MonFun.f (perturb A .snd .pres· ma ma') in
+                  let pfB = cong MonFun.f (perturb B .snd .pres· mb mb') in
+                  let ma-comm = (MonFun.f (ptb-fun A ma)) ∘ (MonFun.f (ptb-fun A ma')) ≡⟨ sym (cong (MonFun.f) (perturb A .snd .pres· ma ma')) ⟩
+                                 MonFun.f (fst (perturb A) ((CommMonoid→Monoid (Perturb A) .snd MonoidStr.· ma) ma'))
+                                   ≡⟨ (λ i -> MonFun.f (ptb-fun A (Perturb A .snd .isCommMonoid .·Comm ma ma' i)))⟩
+                                 _ ≡⟨ cong MonFun.f (perturb A .snd .pres· ma' ma) ⟩
+                                 _ ∎ in
+                  eqMon _ _ ((λ i -> pfB i ∘ MonFun.f g ∘  pfA i) ∙ (λ i -> MonFun.f (ptb-fun B mb) ∘ MonFun.f (ptb-fun B mb') ∘ MonFun.f g ∘ ma-comm i)) ))    } )  }
     where
       open IsMonoidHom
-
+      open CommMonoidStr
+      open IsCommMonoid
+      
 
 -- Monoid of natural numbers with addition
-nat-monoid : Monoid ℓ-zero
-nat-monoid = makeMonoid {M = Nat} zero _+_ isSetℕ +-assoc +-zero (λ x -> refl)
+nat-monoid : CommMonoid ℓ-zero
+nat-monoid = makeCommMonoid {M = Nat} zero _+_ isSetℕ +-assoc +-zero +-comm
 
 open ClockedCombinators k
 
+δ-splits-n : {A : Type ℓ} -> ∀ (n n' : Nat) -> (δ {X = A} ^ n) ∘ (δ ^ n') ≡ δ ^ (n + n')
+δ-splits-n zero n' = ∘-idʳ (δ ^ n')
+δ-splits-n (suc n) n' = ∘-assoc δ (δ ^ n) (δ ^ n') ∙ cong (λ a -> δ ∘ a) (δ-splits-n n n')
+
 𝕃PWP : PosetWithPtb ℓ ℓ' ℓ'' -> PosetWithPtb ℓ ℓ' ℓ''
 𝕃PWP A = record {
   P = LiftPoset.𝕃 (A .P) ;
   Perturb = nat-monoid ×M A .Perturb ;
   perturb =
-    (λ ma → fix f' ma) ,
-    monoidequiv (eqMon (ptb-fun {!!} {!!}) MonId {!refl!}) {!!} }
+    fix f' , -- f' (next f) / fix f'
+    fix {!!} }
     where
       MA = nat-monoid ×M A .Perturb
       open LiftPoset
+      open IsMonoidHom
       f' : ▹ (⟨ MA ⟩ -> MonFun (𝕃 (A .P)) (𝕃 (A .P))) ->
              (⟨ MA ⟩ -> MonFun (𝕃 (A .P)) (𝕃 (A .P)))
       f' rec (n , ma) = record {
@@ -139,8 +157,32 @@ open ClockedCombinators k
                  ℧ -> (δ ^ n) ℧ ;
                 (θ la~) -> θ (λ t -> MonFun.f (rec t ((n , ma))) (la~ t))} ;
         isMon = λ x → {!!} }
+      f : ⟨ MA ⟩ -> MonFun (𝕃 (A .P)) (𝕃 (A .P))
+      f ma = fix f' ma
 
+      
 
+      unfold-f : f ≡ f' (next f)
+      unfold-f = fix-eq f'
+
+      δ-fun : ∀ (n : Nat) (ma : ⟨ MA ⟩) -> (δ ^ n) ∘ (MonFun.f (f' (next f) ma)) ≡ (MonFun.f (f' (next f) ma)) ∘ (δ ^ n) -- (h ∘ (δ ^ n)) ≡ ((δ ^ n) ∘ h)
+      δ-fun zero ma = refl
+      δ-fun (suc n) ma = funExt (λ la -> cong δ (funExt⁻ (δ-fun n ma) la ∙ λ i -> MonFun.f (sym unfold-f i ma) ((δ ^ n) la)))
+
+      {-
+      δ-fun : ∀ (n : Nat) (ma : ⟨ MA ⟩) -> mCompU (Δ ^m n) (f' (next f) ma) ≡ mCompU (f' (next f) ma) (Δ ^m n) -- (h ∘ (δ ^ n)) ≡ ((δ ^ n) ∘ h)
+      δ-fun zero ma = refl
+      δ-fun (suc n) ma = eqMon _ _ (funExt (λ a -> cong δ {!funExt⁻ (cong MonFun.f (δ-fun n ma)) a!}))
+      -}
+
+      
+
+      isHom' : ( ▹ IsMonoidHom (CommMonoid→Monoid (nat-monoid ×M A .Perturb) .snd) (f' (next f)) (EndoMonFun (𝕃 (A .P)) .snd))
+              -> IsMonoidHom (CommMonoid→Monoid (nat-monoid ×M A .Perturb) .snd) (f' (next f)) (EndoMonFun (𝕃 (A .P)) .snd)
+      isHom' IH = monoidequiv
+        (eqMon _ _ (funExt (λ { (η a) -> {!!} ≡⟨ {!!} ⟩ {!!};
+                                (θ la) -> {!!}; μ -> {!!} })))
+        λ { (n , ma) (n' , ma') → eqMon _ _ (funExt λ { (η a) -> {!!} ; (θ la) -> {!!}; μ -> {!!} })}
 
 --MonFun A A' -> MonFun B B' -> MonFun (A × B) (A'× B')
 _×PWP_ : PosetWithPtb ℓ ℓ' ℓ'' -> PosetWithPtb ℓ ℓ' ℓ'' -> PosetWithPtb ℓ (ℓ-max ℓ' ℓ') ℓ''
@@ -150,34 +192,19 @@ A ×PWP B = record {
   perturb =
     (λ { (ma , mb) -> PairFun (mCompU (ptb-fun A ma) π1) (mCompU (ptb-fun B mb) π2) }),
     monoidequiv
-      (eqMon (PairFun
-      (mCompU (perturb A .fst (A .Perturb .snd .MonoidStr.ε)) π1)
-      (mCompU (perturb B .fst (B .Perturb .snd .MonoidStr.ε)) π2)) Id (funExt (λ { (a , b) →
+      (eqMon _ _
+        (funExt (λ { (a , b) →
         ≡-× (funExt⁻ (cong MonFun.f (perturb A .snd .presε)) a)
              (funExt⁻ (cong MonFun.f (perturb B .snd .presε)) b) })))
      λ { (ma , mb) (ma' , mb') →
        eqMon _ _
              (funExt (λ { (a , b ) -> ≡-× (funExt⁻ (cong MonFun.f (perturb A .snd .pres· ma ma')) a)
-                                           (funExt⁻ (cong MonFun.f (perturb B .snd .pres· mb mb')) b) })) } -- λ { (ma , mb) (ma' , mb') → eqMon (ptb-fun {!? ×PWP ?!} {!!}) (mCompU (ptb-fun {!!} {!!}) (ptb-fun {!!} {!!})) {!!} }
+                                           (funExt⁻ (cong MonFun.f (perturb B .snd .pres· mb mb')) b) })) }
   }
   where
     open MonoidStr
     open IsMonoidHom
 
-{-
-PairFun
-      (mCompU (perturb A .fst (A .Perturb .snd ._·_ ma ma')) π1)
-      (mCompU (perturb B .fst (B .Perturb .snd ._·_ mb mb')) π2)
-      ≡
-      mCompU
-      (PairFun (mCompU (perturb A .fst ma) π1)
-       (mCompU (perturb B .fst mb) π2))
-      (PairFun (mCompU (perturb A .fst ma') π1)
-       (mCompU (perturb B .fst mb') π2))
-—————————————————————————————————————————
--}
-
-
 --
 -- Monotone functions on Posets with Perturbations
 --
@@ -220,14 +247,11 @@ unquoteDecl FillersForIsoΣ = declareRecordIsoΣ FillersForIsoΣ (quote (Fillers
 
 FillersFor-Set : ∀ {ℓ ℓ' ℓ'' ℓR : Level} {P1 P2 : PosetWithPtb ℓ ℓ'  ℓ''} {R : MonRel (P1 .P) (P2 .P) ℓR}->
   isSet (FillersFor P1 P2 R)
-FillersFor-Set {P1 = P1} {P2 = P2} {R = R} =
-                       isSetRetract (Iso.fun FillersForIsoΣ) (Iso.inv FillersForIsoΣ) (Iso.leftInv FillersForIsoΣ) (
-                           isSet× (isSetΠ (λ δᴮ → isSetΣSndProp (isSetMonoid (P1 .Perturb)) λ δᴬ → isPropTwoCell (R .MonRel.is-prop-valued)))
-                             (isSet× (isSetΠ (λ δᴸᴮ → isSetΣSndProp (isSet× (isSetMonoid nat-monoid) (isSetMonoid (P1 .Perturb)))
+FillersFor-Set {P1 = P1} {P2 = P2} {R = R} = 
+                     isSetRetract (Iso.fun FillersForIsoΣ) (Iso.inv FillersForIsoΣ) (Iso.leftInv FillersForIsoΣ) (
+                           isSet× (isSetΠ (λ δᴮ → isSetΣSndProp (isSetMonoid (CommMonoid→Monoid (P1 .Perturb))) λ δᴬ → isPropTwoCell (R .MonRel.is-prop-valued)))
+                             (isSet× (isSetΠ (λ δᴸᴮ → isSetΣSndProp (isSet× (isSetMonoid (CommMonoid→Monoid nat-monoid)) (isSetMonoid (CommMonoid→Monoid (P1 .Perturb))))
                                λ δᴸᴬ → isPropTwoCell (LiftMonRel.ℝ (P1 .P) (P2 .P) R .MonRel.is-prop-valued)))
-                                 (isSet× (isSetΠ (λ δᴬ → isSetΣSndProp (isSetMonoid (P2 .Perturb)) (λ δᴮ → isPropTwoCell (R .MonRel.is-prop-valued))))
-                                   (isSetΠ (λ δᴸᴬ → isSetΣSndProp (isSet× (isSetMonoid nat-monoid) (isSetMonoid (P2 .Perturb)))
+                                 (isSet× (isSetΠ (λ δᴬ → isSetΣSndProp (isSetMonoid (CommMonoid→Monoid (P2 .Perturb))) (λ δᴮ → isPropTwoCell (R .MonRel.is-prop-valued))))
+                                   (isSetΠ (λ δᴸᴬ → isSetΣSndProp (isSet× (isSetMonoid (CommMonoid→Monoid nat-monoid)) (isSetMonoid (CommMonoid→Monoid (P2 .Perturb))))
                                       (λ δᴸᴮ → isPropTwoCell (LiftMonRel.ℝ (P1 .P) (P2 .P) R .MonRel.is-prop-valued)))))))
--- isSetΣSndProp ? ?
--- isSet× (isSetΠ ( λ δᴸᴮ → isSetΣSndProp (isSetΣ (isSetMonoid {!!}) λ x → {!!}) λ δᴸᴬ → isPropTwoCell {! R .MonRel.is-prop-valued!}))
-