Infinite products

iris/algebra/category/morphism.v

@@ -291,6 +291,90 @@ Proof. apply fpairM_umpN. Qed.
 Lemma fpairUM_ump {A B C} (f : A -ur> prodUR B C) (g : A -ur> B) (h : A -ur> C) : f ≡ fpairUM g h ↔ fstUM ○ f ≡ g ∧ sndUM ○ f ≡ h.
 Proof. apply fpairM_ump. Qed.
 
+(*Infinite Product*)
+Definition flam {I} {A} {B : I → ucmra} (f : ∀ i, A → B i) (a : A) : discrete_funUR B :=
+  λ i, f i a.
+Global Instance flam_morph {I} {A : cmra} {B : I → ucmra} (f : ∀ i, A → B i) : (∀ i, Morphism (f i)) → Morphism (flam f).
+Proof.
+  split.
+  - solve_proper.
+  - intros n a ? i.
+    by apply (morph_validN (f i)).
+  - intros a1 a2 i.
+    apply (morph_op (f i)).
+Qed.
+Global Instance flam_umorph {I} {A : ucmra} {B : I → ucmra} (f : ∀ i, A → B i) : (∀ i, PerservesUnit (f i)) → PerservesUnit (flam f).
+Proof. intros ? i. apply morph_unit. Qed.
+
+Canonical flamM {I} {A : cmra} {B : I → ucmra} (f : ∀ i, A -r> B i) := Morph (flam f).
+Canonical flamUM {I} {A : ucmra} {B : I → ucmra} (f : ∀ i, A -ur> B i) := UMorph (flam f).
+
+Global Instance flamM_ne {I} {A : cmra} {B : I → ucmra} : ∀ n, Proper (forall_relation (λ _, dist n) ==> dist n) (@flamM I A B).
+Proof.
+  intros n f g Hfg m a ?? i.
+  by apply Hfg.
+Qed.
+Global Instance flamM_proper {I} {A : cmra} {B : I → ucmra} : Proper (forall_relation (λ _, (≡)) ==> (≡)) (@flamM I A B).
+Proof.
+  intros f g Hfg n a ? i.
+  by apply Hfg.
+Qed.
+Global Instance flamUM_ne {I} {A : ucmra} {B : I → ucmra} : ∀ n, Proper (forall_relation (λ _, dist n) ==> dist n) (@flamUM I A B).
+Proof. exact flamM_ne. Qed.
+Global Instance flamUM_proper {I} {A : ucmra} {B : I → ucmra} : Proper (forall_relation (λ _, (≡)) ==> (≡)) (@flamUM I A B).
+Proof. exact flamM_proper. Qed.
+
+Definition fproj {I} {B : I → ucmra} (i : I) (f : discrete_funUR B) : B i :=
+  f i.
+Global Instance fproj_morph {I} {B : I → ucmra} (i : I) : Morphism (@fproj I B i).
+Proof.
+  split.
+  - intros n f g Hfg.
+    apply Hfg.
+  - intros n f Hf.
+    apply Hf.
+  - by intros f g.
+Qed.
+Global Instance fproj_umorph {I} {B : I → ucmra} (i : I) : PerservesUnit (@fproj I B i).
+Proof. by red. Qed.
+
+Canonical fprojM {I} {B : I → ucmra} (i : I) := Morph (@fproj I B i).
+Canonical fprojUM {I} {B : I → ucmra} (i : I) := UMorph (@fproj I B i).
+
+Lemma fprojM_flamM {I A} {B : I → ucmra} (i : I) (f : ∀ i, A -r> B i) : fprojM i ® flamM f ≡ f i.
+Proof. by intros n a. Qed.
+Lemma flamM_eta {I A} {B : I → ucmra} (f : A -r> discrete_funUR B) : f ≡ flamM (λ i, fprojM i ® f).
+Proof. by intros n a. Qed.
+
+Lemma flamM_umpN {I A} {B : I → ucmra} n (f : A -r> discrete_funUR B) (g : ∀ i, A -r> B i) : f ≡{n}≡ flamM g ↔ ∀ i, fprojM i ® f ≡{n}≡ g i.
+Proof.
+  split.
+  - intros Hfg i.
+    by rewrite Hfg fprojM_flamM.
+  - intros Hfg.
+    rewrite (flamM_eta f).
+    by f_equiv.
+Qed.
+Lemma flamM_ump {I A} {B : I → ucmra} (f : A -r> discrete_funUR B) (g : ∀ i, A -r> B i) : f ≡ flamM g ↔ ∀ i, fprojM i ® f ≡ g i.
+Proof.
+  split.
+  - intros Hfg i.
+    by rewrite Hfg fprojM_flamM.
+  - intros Hfg.
+    rewrite (flamM_eta f).
+    by f_equiv.
+Qed.
+
+Lemma fprojUM_flamUM {I A} {B : I → ucmra} (i : I) (f : ∀ i, A -ur> B i) : fprojUM i ○ flamUM f ≡ f i.
+Proof. exact: fprojM_flamM. Qed.
+Lemma flamUM_eta {I A} {B : I → ucmra} (f : A -ur> discrete_funUR B) : f ≡ flamUM (λ i, fprojUM i ○ f).
+Proof. exact: flamM_eta. Qed.
+
+Lemma flamUM_umpN {I A} {B : I → ucmra} n (f : A -ur> discrete_funUR B) (g : ∀ i, A -ur> B i) : f ≡{n}≡ flamUM g ↔ ∀ i, fprojUM i ○ f ≡{n}≡ g i.
+Proof. exact: flamM_umpN. Qed.
+Lemma flamUM_ump {I A} {B : I → ucmra} (f : A -ur> discrete_funUR B) (g : ∀ i, A -ur> B i) : f ≡ flamUM g ↔ ∀ i, fprojUM i ○ f ≡ g i.
+Proof. exact: flamM_ump. Qed.
+
 (** option *)
 Global Instance Some_morph {A : cmra} : Morphism (@Some A).
 Proof. split=>//. apply _. Qed.