diff --git a/CHANGELOG.md b/CHANGELOG.md
index ba65c659667549212587165332358180d98643a6..44da725e29f4ab2144eadc61a7d730fcd225101f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
   is proven in the logic.
+* Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
+  recursive domain equation.  As a consequence, CMRAs no longer need a proof
+  of completeness.
 * Renaming and moving things around: uPred and the rest of the base logic are
   in [base_logic], while [program_logic] is for everything involving the
   general Iris notion of a language.
diff --git a/_CoqProject b/_CoqProject
index b6ca1449fe78f3932bf48f820c047dafc0eddbbd..aa3e00b81e811bf823fef7bae6bad36e54d5c3a9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -43,7 +43,7 @@ algebra/cmra_tactics.v
 algebra/sts.v
 algebra/auth.v
 algebra/gmap.v
-algebra/cofe.v
+algebra/ofe.v
 algebra/base.v
 algebra/dra.v
 algebra/cofe_solver.v
diff --git a/algebra/agree.v b/algebra/agree.v
index 35283796a67fcb7d968ac8c58a397bd50e86c880..8e73f6bb842cfa2409b623c86366371994dac45e 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -12,7 +12,7 @@ Arguments agree_car {_} _ _.
 Arguments agree_is_valid {_} _ _.
 
 Section agree.
-Context {A : cofeT}.
+Context {A : ofeT}.
 
 Instance agree_validN : ValidN (agree A) := λ n x,
   agree_is_valid x n ∧ ∀ n', n' ≤ n → agree_car x n ≡{n'}≡ agree_car x n'.
@@ -28,13 +28,7 @@ Instance agree_equiv : Equiv (agree A) := λ x y,
 Instance agree_dist : Dist (agree A) := λ n x y,
   (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
   (∀ n', n' ≤ n → agree_is_valid x n' → agree_car x n' ≡{n'}≡ agree_car y n').
-Program Instance agree_compl : Compl (agree A) := λ c,
-  {| agree_car n := agree_car (c n) n;
-     agree_is_valid n := agree_is_valid (c n) n |}.
-Next Obligation.
-  intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
-Qed.
-Definition agree_cofe_mixin : CofeMixin (agree A).
+Definition agree_ofe_mixin : OfeMixin (agree A).
 Proof.
   split.
   - intros x y; split.
@@ -47,10 +41,21 @@ Proof.
       * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
       * trans (agree_car y n'). by apply Hxy. by apply Hyz, Hxy.
   - intros n x y Hxy; split; intros; apply Hxy; auto.
-  - intros n c; apply and_wlog_r; intros;
-      symmetry; apply (chain_cauchy c); naive_solver.
 Qed.
-Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
+Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin.
+
+Program Definition agree_compl : Compl agreeC := λ c,
+  {| agree_car n := agree_car (c n) n;
+     agree_is_valid n := agree_is_valid (c n) n |}.
+Next Obligation.
+  intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
+Qed.
+Global Program Instance agree_cofe : Cofe agreeC :=
+  {| compl := agree_compl |}.
+Next Obligation.
+  intros n c; apply and_wlog_r; intros;
+    symmetry; apply (chain_cauchy c); naive_solver.
+Qed.
 
 Program Instance agree_op : Op (agree A) := λ x y,
   {| agree_car := agree_car x;
@@ -113,7 +118,7 @@ Proof.
     + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
 Qed.
 Canonical Structure agreeR : cmraT :=
-  CMRAT (agree A) agree_cofe_mixin agree_cmra_mixin.
+  CMRAT (agree A) agree_ofe_mixin agree_cmra_mixin.
 
 Global Instance agree_total : CMRATotal agreeR.
 Proof. rewrite /CMRATotal; eauto. Qed.
@@ -159,7 +164,7 @@ Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
 Proof. done. Qed.
 
 Section agree_map.
-  Context {A B : cofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+  Context {A B : ofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
   Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
   Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
   Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.
diff --git a/algebra/auth.v b/algebra/auth.v
index c9ba5b77674891b7efe08ba7785a2425df71f532..482b1eb943bf75c3db5d1e02c254f7acc10cecd1 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -14,7 +14,7 @@ Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
 
 (* COFE *)
 Section cofe.
-Context {A : cofeT}.
+Context {A : ofeT}.
 Implicit Types a : excl' A.
 Implicit Types b : A.
 Implicit Types x y : auth A.
@@ -37,9 +37,7 @@ Proof. by destruct 1. Qed.
 Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
 Proof. by destruct 1. Qed.
 
-Instance auth_compl : Compl (auth A) := λ c,
-  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
-Definition auth_cofe_mixin : CofeMixin (auth A).
+Definition auth_ofe_mixin : OfeMixin (auth A).
 Proof.
   split.
   - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
@@ -49,10 +47,17 @@ Proof.
     + by intros ?? [??]; split; symmetry.
     + intros ??? [??] [??]; split; etrans; eauto.
   - by intros ? [??] [??] [??]; split; apply dist_S.
-  - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
-    apply (conv_compl n (chain_map auth_own c)).
 Qed.
-Canonical Structure authC := CofeT (auth A) auth_cofe_mixin.
+Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
+
+Definition auth_compl `{Cofe A} : Compl authC := λ c,
+  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
+Global Program Instance auth_cofe `{Cofe A} : Cofe authC :=
+  {| compl := auth_compl |}.
+Next Obligation.
+  intros ? n c; split. apply (conv_compl n (chain_map authoritative c)).
+  apply (conv_compl n (chain_map auth_own c)).
+Qed.
 
 Global Instance Auth_timeless a b :
   Timeless a → Timeless b → Timeless (Auth a b).
@@ -151,7 +156,7 @@ Proof.
       as (b1&b2&?&?&?); auto using auth_own_validN.
     by exists (Auth ea1 b1), (Auth ea2 b2).
 Qed.
-Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
+Canonical Structure authR := CMRAT (auth A) auth_ofe_mixin auth_cmra_mixin.
 
 Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
 Proof.
@@ -171,7 +176,7 @@ Proof.
   - do 2 constructor; simpl; apply (persistent_core _).
 Qed.
 Canonical Structure authUR :=
-  UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
+  UCMRAT (auth A) auth_ofe_mixin auth_cmra_mixin auth_ucmra_mixin.
 
 Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
 Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
@@ -235,13 +240,13 @@ Proof. by destruct x as [[[]|]]. Qed.
 Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
   auth_map (g ∘ f) x = auth_map g (auth_map f x).
 Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_map_ext {A B : cofeT} (f g : A → B) x :
+Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
   (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
   constructor; simpl; auto.
   apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
 Qed.
-Instance auth_map_ne {A B : cofeT} n :
+Instance auth_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
 Proof.
   intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 85e0e2f7c07e162b3c39da3f539c26810954213b..08117babe892f8415e2de5af006af85c64eb21a0 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cofe.
+From iris.algebra Require Export ofe.
 
 Class PCore (A : Type) := pcore : A → option A.
 Instance: Params (@pcore) 2.
@@ -61,34 +61,32 @@ Structure cmraT := CMRAT' {
   cmra_car :> Type;
   cmra_equiv : Equiv cmra_car;
   cmra_dist : Dist cmra_car;
-  cmra_compl : Compl cmra_car;
   cmra_pcore : PCore cmra_car;
   cmra_op : Op cmra_car;
   cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
-  cmra_cofe_mixin : CofeMixin cmra_car;
+  cmra_ofe_mixin : OfeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car;
   _ : Type
 }.
-Arguments CMRAT' _ {_ _ _ _ _ _ _} _ _ _.
+Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
 Notation CMRAT A m m' := (CMRAT' A m m' A).
 Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
-Arguments cmra_compl : simpl never.
 Arguments cmra_pcore : simpl never.
 Arguments cmra_op : simpl never.
 Arguments cmra_valid : simpl never.
 Arguments cmra_validN : simpl never.
-Arguments cmra_cofe_mixin : simpl never.
+Arguments cmra_ofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
 Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
 Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
 Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
 Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
-Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
-Canonical Structure cmra_cofeC.
+Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
+Canonical Structure cmra_ofeC.
 
 (** Lifting properties from the mixin *)
 Section cmra_mixin.
@@ -160,36 +158,34 @@ Structure ucmraT := UCMRAT' {
   ucmra_car :> Type;
   ucmra_equiv : Equiv ucmra_car;
   ucmra_dist : Dist ucmra_car;
-  ucmra_compl : Compl ucmra_car;
   ucmra_pcore : PCore ucmra_car;
   ucmra_op : Op ucmra_car;
   ucmra_valid : Valid ucmra_car;
   ucmra_validN : ValidN ucmra_car;
   ucmra_empty : Empty ucmra_car;
-  ucmra_cofe_mixin : CofeMixin ucmra_car;
+  ucmra_ofe_mixin : OfeMixin ucmra_car;
   ucmra_cmra_mixin : CMRAMixin ucmra_car;
   ucmra_mixin : UCMRAMixin ucmra_car;
   _ : Type;
 }.
-Arguments UCMRAT' _ {_ _ _ _ _ _ _ _} _ _ _ _.
+Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
 Notation UCMRAT A m m' m'' := (UCMRAT' A m m' m'' A).
 Arguments ucmra_car : simpl never.
 Arguments ucmra_equiv : simpl never.
 Arguments ucmra_dist : simpl never.
-Arguments ucmra_compl : simpl never.
 Arguments ucmra_pcore : simpl never.
 Arguments ucmra_op : simpl never.
 Arguments ucmra_valid : simpl never.
 Arguments ucmra_validN : simpl never.
-Arguments ucmra_cofe_mixin : simpl never.
+Arguments ucmra_ofe_mixin : simpl never.
 Arguments ucmra_cmra_mixin : simpl never.
 Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmraT.
 Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
-Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
-Canonical Structure ucmra_cofeC.
+Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
+Canonical Structure ucmra_ofeC.
 Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
-  CMRAT A (ucmra_cofe_mixin A) (ucmra_cmra_mixin A).
+  CMRAT A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
 Canonical Structure ucmra_cmraR.
 
 (** Lifting properties from the mixin *)
@@ -687,7 +683,7 @@ Proof. split. apply _. by rewrite /= !ucmra_homomorphism_unit. Qed.
 
 (** Functors *)
 Structure rFunctor := RFunctor {
-  rFunctor_car : cofeT → cofeT → cmraT;
+  rFunctor_car : ofeT → ofeT → cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
   rFunctor_ne A1 A2 B1 B2 n :
@@ -705,7 +701,7 @@ Instance: Params (@rFunctor_map) 5.
 Class rFunctorContractive (F : rFunctor) :=
   rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
 
-Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
+Definition rFunctor_diag (F: rFunctor) (A: ofeT) : cmraT := rFunctor_car F A A.
 Coercion rFunctor_diag : rFunctor >-> Funclass.
 
 Program Definition constRF (B : cmraT) : rFunctor :=
@@ -716,7 +712,7 @@ Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
 Structure urFunctor := URFunctor {
-  urFunctor_car : cofeT → cofeT → ucmraT;
+  urFunctor_car : ofeT → ofeT → ucmraT;
   urFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
   urFunctor_ne A1 A2 B1 B2 n :
@@ -734,7 +730,7 @@ Instance: Params (@urFunctor_map) 5.
 Class urFunctorContractive (F : urFunctor) :=
   urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
 
-Definition urFunctor_diag (F: urFunctor) (A: cofeT) : ucmraT := urFunctor_car F A A.
+Definition urFunctor_diag (F: urFunctor) (A: ofeT) : ucmraT := urFunctor_car F A A.
 Coercion urFunctor_diag : urFunctor >-> Funclass.
 
 Program Definition constURF (B : ucmraT) : urFunctor :=
@@ -790,7 +786,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
 Section discrete.
   Context `{Equiv A, PCore A, Op A, Valid A, @Equivalence A (≡)}.
   Context (ra_mix : RAMixin A).
-  Existing Instances discrete_dist discrete_compl.
+  Existing Instances discrete_dist.
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
@@ -802,9 +798,9 @@ Section discrete.
 End discrete.
 
 Notation discreteR A ra_mix :=
-  (CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
+  (CMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix)).
 Notation discreteUR A ra_mix ucmra_mix :=
-  (UCMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
+  (UCMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
 
 Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
   @Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
@@ -843,13 +839,13 @@ Section unit.
   Instance unit_op : Op () := λ x y, ().
   Lemma unit_cmra_mixin : CMRAMixin ().
   Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
-  Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
+  Canonical Structure unitR : cmraT := CMRAT () unit_ofe_mixin unit_cmra_mixin.
 
   Instance unit_empty : Empty () := ().
   Lemma unit_ucmra_mixin : UCMRAMixin ().
   Proof. done. Qed.
   Canonical Structure unitUR : ucmraT :=
-    UCMRAT () unit_cofe_mixin unit_cmra_mixin unit_ucmra_mixin.
+    UCMRAT () unit_ofe_mixin unit_cmra_mixin unit_ucmra_mixin.
 
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
   Proof. done. Qed.
@@ -993,7 +989,7 @@ Section prod.
       by exists (z11,z21), (z12,z22).
   Qed.
   Canonical Structure prodR :=
-    CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
+    CMRAT (A * B) prod_ofe_mixin prod_cmra_mixin.
 
   Lemma pair_op (a a' : A) (b b' : B) : (a, b) â‹… (a', b') = (a â‹… a', b â‹… b').
   Proof. done. Qed.
@@ -1032,7 +1028,7 @@ Section prod_unit.
     - rewrite prod_pcore_Some'; split; apply (persistent _).
   Qed.
   Canonical Structure prodUR :=
-    UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin.
+    UCMRAT (A * B) prod_ofe_mixin prod_cmra_mixin prod_ucmra_mixin.
 
   Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
   Proof. by rewrite pair_op left_id right_id. Qed.
@@ -1166,7 +1162,7 @@ Section option.
       + exists None, None; repeat constructor.
   Qed.
   Canonical Structure optionR :=
-    CMRAT (option A) option_cofe_mixin option_cmra_mixin.
+    CMRAT (option A) option_ofe_mixin option_cmra_mixin.
 
   Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
   Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
@@ -1175,7 +1171,7 @@ Section option.
   Lemma option_ucmra_mixin : UCMRAMixin optionR.
   Proof. split. done. by intros []. done. Qed.
   Canonical Structure optionUR :=
-    UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
+    UCMRAT (option A) option_ofe_mixin option_cmra_mixin option_ucmra_mixin.
 
   (** Misc *)
   Global Instance Some_cmra_monotone : CMRAMonotone Some.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 20a9ff0f01bfb9788a0525f29c873d107950da65..b304dbb423f7a7408fbe6d6d436017ba7554cfb7 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -1,7 +1,8 @@
-From iris.algebra Require Export cofe.
+From iris.algebra Require Export ofe.
 
 Record solution (F : cFunctor) := Solution {
-  solution_car :> cofeT;
+  solution_car :> ofeT;
+  solution_cofe : Cofe solution_car;
   solution_unfold : solution_car -n> F solution_car;
   solution_fold : F solution_car -n> solution_car;
   solution_fold_unfold X : solution_fold (solution_unfold X) ≡ X;
@@ -9,14 +10,17 @@ Record solution (F : cFunctor) := Solution {
 }.
 Arguments solution_unfold {_} _.
 Arguments solution_fold {_} _.
+Existing Instance solution_cofe.
 
 Module solver. Section solver.
 Context (F : cFunctor) `{Fcontr : cFunctorContractive F}
-        `{Finhab : Inhabited (F unitC)}.
+        `{Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)} `{Finh : Inhabited (F unitC)}.
 Notation map := (cFunctor_map F).
 
-Fixpoint A (k : nat) : cofeT :=
+Fixpoint A (k : nat) : ofeT :=
   match k with 0 => unitC | S k => F (A k) end.
+Local Instance: ∀ k, Cofe (A k).
+Proof. induction 0; apply _. Defined.
 Fixpoint f (k : nat) : A k -n> A (S k) :=
   match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
 with g (k : nat) : A (S k) -n> A k :=
@@ -47,17 +51,7 @@ Record tower := {
 }.
 Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
 Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
-Program Definition tower_chain (c : chain tower) (k : nat) : chain (A k) :=
-  {| chain_car i := c i k |}.
-Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
-Program Instance tower_compl : Compl tower := λ c,
-  {| tower_car n := compl (tower_chain c n) |}.
-Next Obligation.
-  intros c k; apply equiv_dist=> n.
-  by rewrite (conv_compl n (tower_chain c k))
-    (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
-Qed.
-Definition tower_cofe_mixin : CofeMixin tower.
+Definition tower_ofe_mixin : OfeMixin tower.
 Proof.
   split.
   - intros X Y; split; [by intros HXY n k; apply equiv_dist|].
@@ -68,10 +62,24 @@ Proof.
     + by intros X Y Z ?? n; trans (Y n).
   - intros k X Y HXY n; apply dist_S.
     by rewrite -(g_tower X) (HXY (S n)) g_tower.
-  - intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
-    apply (chain_cauchy c); lia.
 Qed.
-Definition T : cofeT := CofeT tower tower_cofe_mixin.
+Definition T : ofeT := OfeT tower tower_ofe_mixin.
+
+Program Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
+  {| chain_car i := c i k |}.
+Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
+Program Definition tower_compl : Compl T := λ c,
+  {| tower_car n := compl (tower_chain c n) |}.
+Next Obligation.
+  intros c k; apply equiv_dist=> n.
+  by rewrite (conv_compl n (tower_chain c k))
+    (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
+Qed.
+Global Program Instance tower_cofe : Cofe T := { compl := tower_compl }.
+Next Obligation.
+  intros n c k; rewrite /= (conv_compl n (tower_chain c k)).
+  apply (chain_cauchy c); lia.
+Qed.
 
 Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
   match i with 0 => cid | S i => f (i + k) â—Ž ff i end.
@@ -197,7 +205,7 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
 Proof.
-  apply (Solution F T (CofeMor unfold) (CofeMor fold)).
+  apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
   - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
     trans (map (ff n, gg n) (X (S (n + k)))).
diff --git a/algebra/csum.v b/algebra/csum.v
index 954fdabf56dd1d564282ed1f1f7735d1c0841046..1adde00f7fa2afa1e7337466174b75ccca88203d 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -22,7 +22,7 @@ Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
   match x with Cinr b => Some b | _ => None end.
 
 Section cofe.
-Context {A B : cofeT}.
+Context {A B : ofeT}.
 Implicit Types a : A.
 Implicit Types b : B.
 
@@ -55,19 +55,7 @@ Proof. by inversion_clear 1. Qed.
 Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B).
 Proof. by inversion_clear 1. Qed.
 
-Program Definition csum_chain_l (c : chain (csum A B)) (a : A) : chain A :=
-  {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
-Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Program Definition csum_chain_r (c : chain (csum A B)) (b : B) : chain B :=
-  {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
-Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Instance csum_compl : Compl (csum A B) := λ c,
-  match c 0 with
-  | Cinl a => Cinl (compl (csum_chain_l c a))
-  | Cinr b => Cinr (compl (csum_chain_r c b))
-  | CsumBot => CsumBot
-  end.
-Definition csum_cofe_mixin : CofeMixin (csum A B).
+Definition csum_ofe_mixin : OfeMixin (csum A B).
 Proof.
   split.
   - intros mx my; split.
@@ -79,12 +67,30 @@ Proof.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
   - by inversion_clear 1; constructor; apply dist_S.
-  - intros n c; rewrite /compl /csum_compl.
-    feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-    + rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
-    + rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure csumC : cofeT := CofeT (csum A B) csum_cofe_mixin.
+Canonical Structure csumC : ofeT := OfeT (csum A B) csum_ofe_mixin.
+
+Program Definition csum_chain_l (c : chain csumC) (a : A) : chain A :=
+  {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
+Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+Program Definition csum_chain_r (c : chain csumC) (b : B) : chain B :=
+  {| chain_car n := match c n return _ with Cinr b' => b' | _ => b end |}.
+Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+Definition csum_compl `{Cofe A, Cofe B} : Compl csumC := λ c,
+  match c 0 with
+  | Cinl a => Cinl (compl (csum_chain_l c a))
+  | Cinr b => Cinr (compl (csum_chain_r c b))
+  | CsumBot => CsumBot
+  end.
+Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumC :=
+  {| compl := csum_compl |}.
+Next Obligation.
+  intros ?? n c; rewrite /compl /csum_compl.
+  feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
+  + rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
+  + rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
+Qed.
+
 Global Instance csum_discrete : Discrete A → Discrete B → Discrete csumC.
 Proof. by inversion_clear 3; constructor; apply (timeless _). Qed.
 Global Instance csum_leibniz :
@@ -115,10 +121,10 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
                        (g : B → B') (g' : B' → B'') (x : csum A B) :
   csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x).
 Proof. by destruct x. Qed.
-Lemma csum_map_ext {A A' B B' : cofeT} (f f' : A → A') (g g' : B → B') x :
+Lemma csum_map_ext {A A' B B' : ofeT} (f f' : A → A') (g g' : B → B') x :
   (∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
 Proof. by destruct x; constructor. Qed.
-Instance csum_map_cmra_ne {A A' B B' : cofeT} n :
+Instance csum_map_cmra_ne {A A' B B' : ofeT} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
          (@csum_map A A' B B').
 Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
@@ -224,7 +230,7 @@ Proof.
     + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
 Qed.
 Canonical Structure csumR :=
-  CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.
+  CMRAT (csum A B) csum_ofe_mixin csum_cmra_mixin.
 
 Global Instance csum_cmra_discrete :
   CMRADiscrete A → CMRADiscrete B → CMRADiscrete csumR.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index c7ccce543ed4a0caf1d07a6da75555cf903f80ce..42c54d8aa37b826c13e239076022a4d8b8d44069 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -20,7 +20,7 @@ Implicit Types x y : dec_agree A.
 
 Instance dec_agree_valid : Valid (dec_agree A) := λ x,
   if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeC : cofeT := leibnizC (dec_agree A).
+Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).
 
 Instance dec_agree_op : Op (dec_agree A) := λ x y,
   match x, y with
diff --git a/algebra/dra.v b/algebra/dra.v
index a3b51580b7b72aebc2140d628349929c153724dd..6bd0f018046f70561f4c0faa9ce55ce9754da56f 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -114,7 +114,7 @@ Proof.
   - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
     split; [|intros; trans y]; tauto.
 Qed.
-Canonical Structure validityC : cofeT := discreteC (validity A).
+Canonical Structure validityC : ofeT := discreteC (validity A).
 
 Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
 Proof. by split; apply: dra_valid_proper. Qed.
diff --git a/algebra/excl.v b/algebra/excl.v
index 4c0200eaa835ced2c7675732ccb25e7e1354aa13..a90fbd97d60b644bd681af60640e72513918cde7 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -17,7 +17,7 @@ Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
   match x with Excl a => Some a | _ => None end.
 
 Section excl.
-Context {A : cofeT}.
+Context {A : ofeT}.
 Implicit Types a b : A.
 Implicit Types x y : excl A.
 
@@ -40,12 +40,7 @@ Proof. by inversion_clear 1. Qed.
 Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
 Proof. by inversion_clear 1. Qed.
 
-Program Definition excl_chain (c : chain (excl A)) (a : A) : chain A :=
-  {| chain_car n := match c n return _ with Excl y => y | _ => a end |}.
-Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Instance excl_compl : Compl (excl A) := λ c,
-  match c 0 with Excl a => Excl (compl (excl_chain c a)) | x => x end.
-Definition excl_cofe_mixin : CofeMixin (excl A).
+Definition excl_ofe_mixin : OfeMixin (excl A).
 Proof.
   split.
   - intros x y; split; [by destruct 1; constructor; apply equiv_dist|].
@@ -56,11 +51,22 @@ Proof.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
   - by inversion_clear 1; constructor; apply dist_S.
-  - intros n c; rewrite /compl /excl_compl.
-    feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-    rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
-Canonical Structure exclC : cofeT := CofeT (excl A) excl_cofe_mixin.
+Canonical Structure exclC : ofeT := OfeT (excl A) excl_ofe_mixin.
+
+Program Definition excl_chain (c : chain exclC) (a : A) : chain A :=
+  {| chain_car n := match c n return _ with Excl y => y | _ => a end |}.
+Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+Definition excl_compl `{Cofe A} : Compl exclC := λ c,
+  match c 0 with Excl a => Excl (compl (excl_chain c a)) | x => x end.
+Global Program Instance excl_cofe `{Cofe A} : Cofe exclC :=
+  {| compl := excl_compl |}.
+Next Obligation.
+  intros ? n c; rewrite /compl /excl_compl.
+  feed inversion (chain_cauchy c 0 n); auto with omega.
+  rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
+Qed.
+
 Global Instance excl_discrete : Discrete A → Discrete exclC.
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
 Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
@@ -92,7 +98,7 @@ Proof.
   - intros n x [?|] [?|] ?; inversion_clear 1; eauto.
 Qed.
 Canonical Structure exclR :=
-  CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
+  CMRAT (excl A) excl_ofe_mixin excl_cmra_mixin.
 
 Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
 Proof. split. apply _. by intros []. Qed.
@@ -138,13 +144,13 @@ Proof. by destruct x. Qed.
 Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
   excl_map (g ∘ f) x = excl_map g (excl_map f x).
 Proof. by destruct x. Qed.
-Lemma excl_map_ext {A B : cofeT} (f g : A → B) x :
+Lemma excl_map_ext {A B : ofeT} (f g : A → B) x :
   (∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
 Proof. by destruct x; constructor. Qed.
-Instance excl_map_ne {A B : cofeT} n :
+Instance excl_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Instance excl_map_cmra_monotone {A B : cofeT} (f : A → B) :
+Instance excl_map_cmra_monotone {A B : ofeT} (f : A → B) :
   (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
 Proof.
   split; try apply _.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 5af9911a0b709c8d53e9183a499af511298735a9..0734d5c0f88198de0b1600607aec44a7286989f4 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -4,17 +4,12 @@ From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
 
 Section cofe.
-Context `{Countable K} {A : cofeT}.
+Context `{Countable K} {A : ofeT}.
 Implicit Types m : gmap K A.
 
 Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
   ∀ i, m1 !! i ≡{n}≡ m2 !! i.
-Program Definition gmap_chain (c : chain (gmap K A))
-  (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
-Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
-Instance gmap_compl : Compl (gmap K A) := λ c,
-  map_imap (λ i _, compl (gmap_chain c i)) (c 0).
-Definition gmap_cofe_mixin : CofeMixin (gmap K A).
+Definition gmap_ofe_mixin : OfeMixin (gmap K A).
 Proof.
   split.
   - intros m1 m2; split.
@@ -25,11 +20,22 @@ Proof.
     + by intros m1 m2 ? k.
     + by intros m1 m2 m3 ?? k; trans (m2 !! k).
   - by intros n m1 m2 ? k; apply dist_S.
-  - intros n c k; rewrite /compl /gmap_compl lookup_imap.
-    feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia.
-    by rewrite conv_compl /=; apply reflexive_eq.
 Qed.
-Canonical Structure gmapC : cofeT := CofeT (gmap K A) gmap_cofe_mixin.
+Canonical Structure gmapC : ofeT := OfeT (gmap K A) gmap_ofe_mixin.
+
+Program Definition gmap_chain (c : chain gmapC)
+  (k : K) : chain (optionC A) := {| chain_car n := c n !! k |}.
+Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
+Definition gmap_compl `{Cofe A} : Compl gmapC := λ c,
+  map_imap (λ i _, compl (gmap_chain c i)) (c 0).
+Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapC :=
+  {| compl := gmap_compl |}.
+Next Obligation.
+  intros ? n c k. rewrite /compl /gmap_compl lookup_imap.
+  feed inversion (λ H, chain_cauchy c 0 n H k);simplify_option_eq;auto with lia.
+  by rewrite conv_compl /=; apply reflexive_eq.
+Qed.
+
 Global Instance gmap_discrete : Discrete A → Discrete gmapC.
 Proof. intros ? m m' ? i. by apply (timeless _). Qed.
 (* why doesn't this go automatic? *)
@@ -165,7 +171,7 @@ Proof.
       * by rewrite lookup_partial_alter_ne // Hm2' lookup_delete_ne.
 Qed.
 Canonical Structure gmapR :=
-  CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
+  CMRAT (gmap K A) gmap_ofe_mixin gmap_cmra_mixin.
 
 Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR.
 Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
@@ -178,7 +184,7 @@ Proof.
   - constructor=> i. by rewrite lookup_omap lookup_empty.
 Qed.
 Canonical Structure gmapUR :=
-  UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
+  UCMRAT (gmap K A) gmap_ofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
 
 (** Internalized properties *)
 Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
@@ -440,7 +446,7 @@ Qed.
 End properties.
 
 (** Functor *)
-Instance gmap_fmap_ne `{Countable K} {A B : cofeT} (f : A → B) n :
+Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A → B) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
 Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
 Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 317484fbe47c1f3d4a2fcc52d000e7889eb30d85..dda02f67fce96f07d70a0e89ad69a8645bcd60e5 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -4,25 +4,20 @@ From iris.prelude Require Import finite.
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
-Definition iprod `{Finite A} (B : A → cofeT) := ∀ x, B x.
-Definition iprod_insert `{Finite A} {B : A → cofeT}
+Definition iprod `{Finite A} (B : A → ofeT) := ∀ x, B x.
+Definition iprod_insert `{Finite A} {B : A → ofeT}
     (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
 Instance: Params (@iprod_insert) 5.
 
 Section iprod_cofe.
-  Context `{Finite A} {B : A → cofeT}.
+  Context `{Finite A} {B : A → ofeT}.
   Implicit Types x : A.
   Implicit Types f g : iprod B.
 
   Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x.
   Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Program Definition iprod_chain (c : chain (iprod B)) (x : A) : chain (B x) :=
-    {| chain_car n := c n x |}.
-  Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed.
-  Program Instance iprod_compl : Compl (iprod B) := λ c x,
-    compl (iprod_chain c x).
-  Definition iprod_cofe_mixin : CofeMixin (iprod B).
+  Definition iprod_ofe_mixin : OfeMixin (iprod B).
   Proof.
     split.
     - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -32,11 +27,19 @@ Section iprod_cofe.
       + by intros f g ? x.
       + by intros f g h ?? x; trans (g x).
     - intros n f g Hfg x; apply dist_S, Hfg.
-    - intros n c x.
-      rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
-      apply (chain_cauchy c); lia.
   Qed.
-  Canonical Structure iprodC : cofeT := CofeT (iprod B) iprod_cofe_mixin.
+  Canonical Structure iprodC : ofeT := OfeT (iprod B) iprod_ofe_mixin.
+
+  Program Definition iprod_chain (c : chain iprodC) (x : A) : chain (B x) :=
+    {| chain_car n := c n x |}.
+  Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed.
+  Global Program Instance iprod_cofe `{∀ a, Cofe (B a)} : Cofe iprodC :=
+    {| compl c x := compl (iprod_chain c x) |}.
+  Next Obligation.
+    intros ? n c x.
+    rewrite (conv_compl n (iprod_chain c x)).
+    apply (chain_cauchy c); lia.
+  Qed.
 
   (** Properties of iprod_insert. *)
   Context `{EqDecision A}.
@@ -125,7 +128,7 @@ Section iprod_cmra.
       exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
   Qed.
   Canonical Structure iprodR :=
-    CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.
+    CMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin.
 
   Instance iprod_empty : Empty (iprod B) := λ x, ∅.
   Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl.
@@ -138,7 +141,7 @@ Section iprod_cmra.
     - constructor=> x. apply persistent_core, _.
   Qed.
   Canonical Structure iprodUR :=
-    UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
+    UCMRAT (iprod B) iprod_ofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
 
   Global Instance iprod_empty_timeless :
     (∀ i, Timeless (∅ : B i)) → Timeless (∅ : iprod B).
@@ -264,21 +267,21 @@ Section iprod_singleton.
 End iprod_singleton.
 
 (** * Functor *)
-Definition iprod_map `{Finite A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
+Definition iprod_map `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x)
   (g : iprod B1) : iprod B2 := λ x, f _ (g x).
 
-Lemma iprod_map_ext `{Finite A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) (g : iprod B1) :
+Lemma iprod_map_ext `{Finite A} {B1 B2 : A → ofeT} (f1 f2 : ∀ x, B1 x → B2 x) (g : iprod B1) :
   (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
 Proof. done. Qed.
-Lemma iprod_map_id `{Finite A} {B : A → cofeT} (g : iprod B) :
+Lemma iprod_map_id `{Finite A} {B : A → ofeT} (g : iprod B) :
   iprod_map (λ _, id) g = g.
 Proof. done. Qed.
-Lemma iprod_map_compose `{Finite A} {B1 B2 B3 : A → cofeT}
+Lemma iprod_map_compose `{Finite A} {B1 B2 B3 : A → ofeT}
     (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
   iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
 Proof. done. Qed.
 
-Instance iprod_map_ne `{Finite A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
+Instance iprod_map_ne `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x) n :
   (∀ x, Proper (dist n ==> dist n) (f x)) →
   Proper (dist n ==> dist n) (iprod_map f).
 Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
@@ -292,10 +295,10 @@ Proof.
     rewrite /iprod_map; apply (cmra_monotone _), Hf.
 Qed.
 
-Definition iprodC_map `{Finite A} {B1 B2 : A → cofeT}
+Definition iprodC_map `{Finite A} {B1 B2 : A → ofeT}
     (f : iprod (λ x, B1 x -n> B2 x)) :
   iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne `{Finite A} {B1 B2 : A → cofeT} n :
+Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} n :
   Proper (dist n ==> dist n) (@iprodC_map A _ _ B1 B2).
 Proof. intros f1 f2 Hf g x; apply Hf. Qed.
 
diff --git a/algebra/list.v b/algebra/list.v
index 5d67d4f74356b886ce2a1366f4060ac5981addd0..5fd0616e8d8a5fe2b1d08665915a36b62d1c6ec6 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -4,7 +4,7 @@ From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
 
 Section cofe.
-Context {A : cofeT}.
+Context {A : ofeT}.
 
 Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 
@@ -42,34 +42,40 @@ Proof. intros ???; by apply dist_option_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n :
   Proper (dist n ==> dist n ==> dist n) (@resize A n) := _.
 
+Definition list_ofe_mixin : OfeMixin (list A).
+Proof.
+  split.
+  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
+    split; induction 1; constructor; intros; try apply equiv_dist; auto.
+  - apply _.
+  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
+Qed.
+Canonical Structure listC := OfeT (list A) list_ofe_mixin.
+
 Program Definition list_chain
-    (c : chain (list A)) (x : A) (k : nat) : chain A :=
+    (c : chain listC) (x : A) (k : nat) : chain A :=
   {| chain_car n := from_option id x (c n !! k) |}.
 Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
-Instance list_compl : Compl (list A) := λ c,
+Definition list_compl `{Cofe A} : Compl listC := λ c,
   match c 0 with
   | [] => []
   | x :: _ => compl ∘ list_chain c x <$> seq 0 (length (c 0))
   end.
-
-Definition list_cofe_mixin : CofeMixin (list A).
-Proof.
-  split.
-  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
-    split; induction 1; constructor; intros; try apply equiv_dist; auto.
-  - apply _.
-  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
-  - intros n c; rewrite /compl /list_compl.
-    destruct (c 0) as [|x l] eqn:Hc0 at 1.
-    { by destruct (chain_cauchy c 0 n); auto with omega. }
-    rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
-    apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
-    destruct (decide (i < length (c n))); last first.
-    { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
-    rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
-    by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
+Global Program Instance list_cofe `{Cofe A} : Cofe listC :=
+  {| compl := list_compl |}.
+Next Obligation.
+  intros ? n c; rewrite /compl /list_compl.
+  destruct (c 0) as [|x l] eqn:Hc0 at 1.
+  { by destruct (chain_cauchy c 0 n); auto with omega. }
+  rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
+  apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
+  destruct (decide (i < length (c n))); last first.
+  { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
+  rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
+  destruct (lookup_lt_is_Some_2 (c n) i) as [? Hcn]; first done.
+  by rewrite Hcn.
 Qed.
-Canonical Structure listC := CofeT (list A) list_cofe_mixin.
+
 Global Instance list_discrete : Discrete A → Discrete listC.
 Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
 
@@ -82,10 +88,10 @@ End cofe.
 Arguments listC : clear implicits.
 
 (** Functor *)
-Lemma list_fmap_ext_ne {A} {B : cofeT} (f g : A → B) (l : list A) n :
+Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A → B) (l : list A) n :
   (∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.
 Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
-Instance list_fmap_ne {A B : cofeT} (f : A → B) n:
+Instance list_fmap_ne {A B : ofeT} (f : A → B) n:
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
 Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
@@ -212,7 +218,7 @@ Section cmra.
           (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto.
         exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
   Qed.
-  Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin.
+  Canonical Structure listR := CMRAT (list A) list_ofe_mixin list_cmra_mixin.
 
   Global Instance empty_list : Empty (list A) := [].
   Definition list_ucmra_mixin : UCMRAMixin (list A).
@@ -223,7 +229,7 @@ Section cmra.
     - by constructor.
   Qed.
   Canonical Structure listUR :=
-    UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin.
+    UCMRAT (list A) list_ofe_mixin list_cmra_mixin list_ucmra_mixin.
 
   Global Instance list_cmra_discrete : CMRADiscrete A → CMRADiscrete listR.
   Proof.
diff --git a/algebra/cofe.v b/algebra/ofe.v
similarity index 69%
rename from algebra/cofe.v
rename to algebra/ofe.v
index f3ab299c94438473d271cdbdb996679983e43950..47d4fb8f8d4454af71bd83966a9e0e8fcfebace5 100644
--- a/algebra/cofe.v
+++ b/algebra/ofe.v
@@ -1,22 +1,12 @@
 From iris.algebra Require Export base.
 
-(** This files defines (a shallow embedding of) the category of COFEs:
+(** This files defines (a shallow embedding of) the category of OFEs:
     Complete ordered families of equivalences. This is a cartesian closed
     category, and mathematically speaking, the entire development lives
     in this category. However, we will generally prefer to work with raw
     Coq functions plus some registered Proper instances for non-expansiveness.
     This makes writing such functions much easier. It turns out that it many 
     cases, we do not even need non-expansiveness.
-
-    In principle, it would be possible to perform a large part of the
-    development on OFEs, i.e., on bisected metric spaces that are not
-    necessary complete. This is because the function space A → B has a
-    completion if B has one - for A, the metric itself suffices.
-    That would result in a simplification of some constructions, becuase
-    no completion would have to be provided. However, on the other hand,
-    we would have to introduce the notion of OFEs into our alebraic
-    hierarchy, which we'd rather avoid. Furthermore, on paper, justifying
-    this mix of OFEs and COFEs is a little fuzzy.
 *)
 
 (** Unbundeled version *)
@@ -40,57 +30,43 @@ Tactic Notation "cofe_subst" :=
   | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
   end.
 
-Record chain (A : Type) `{Dist A} := {
-  chain_car :> nat → A;
-  chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n
-}.
-Arguments chain_car {_ _} _ _.
-Arguments chain_cauchy {_ _} _ _ _ _.
-Class Compl A `{Dist A} := compl : chain A → A.
-
-Record CofeMixin A `{Equiv A, Compl A} := {
+Record OfeMixin A `{Equiv A, Dist A} := {
   mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
   mixin_dist_equivalence n : Equivalence (dist n);
-  mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y;
-  mixin_conv_compl n c : compl c ≡{n}≡ c n
+  mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y
 }.
 Class Contractive `{Dist A, Dist B} (f : A → B) :=
   contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
 
 (** Bundeled version *)
-Structure cofeT := CofeT' {
-  cofe_car :> Type;
-  cofe_equiv : Equiv cofe_car;
-  cofe_dist : Dist cofe_car;
-  cofe_compl : Compl cofe_car;
-  cofe_mixin : CofeMixin cofe_car;
+Structure ofeT := OfeT' {
+  ofe_car :> Type;
+  ofe_equiv : Equiv ofe_car;
+  ofe_dist : Dist ofe_car;
+  ofe_mixin : OfeMixin ofe_car;
   _ : Type
 }.
-Arguments CofeT' _ {_ _ _} _ _.
-Notation CofeT A m := (CofeT' A m A).
-Add Printing Constructor cofeT.
-Hint Extern 0 (Equiv _) => eapply (@cofe_equiv _) : typeclass_instances.
-Hint Extern 0 (Dist _) => eapply (@cofe_dist _) : typeclass_instances.
-Hint Extern 0 (Compl _) => eapply (@cofe_compl _) : typeclass_instances.
-Arguments cofe_car : simpl never.
-Arguments cofe_equiv : simpl never.
-Arguments cofe_dist : simpl never.
-Arguments cofe_compl : simpl never.
-Arguments cofe_mixin : simpl never.
+Arguments OfeT' _ {_ _} _ _.
+Notation OfeT A m := (OfeT' A m A).
+Add Printing Constructor ofeT.
+Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
+Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
+Arguments ofe_car : simpl never.
+Arguments ofe_equiv : simpl never.
+Arguments ofe_dist : simpl never.
+Arguments ofe_mixin : simpl never.
 
 (** Lifting properties from the mixin *)
-Section cofe_mixin.
-  Context {A : cofeT}.
+Section ofe_mixin.
+  Context {A : ofeT}.
   Implicit Types x y : A.
   Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y.
-  Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed.
+  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
   Global Instance dist_equivalence n : Equivalence (@dist A _ n).
-  Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
+  Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
   Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
-  Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
-  Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c n.
-  Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
-End cofe_mixin.
+  Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
+End ofe_mixin.
 
 Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
 
@@ -99,11 +75,26 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
    more sense. *)
 Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
 Arguments timeless {_ _ _} _ {_} _ _.
-Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.
+Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.
+
+(** OFEs with a completion *)
+Record chain (A : ofeT) := {
+  chain_car :> nat → A;
+  chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n
+}.
+Arguments chain_car {_} _ _.
+Arguments chain_cauchy {_} _ _ _ _.
+
+Notation Compl A := (chain A%type → A).
+Class Cofe (A : ofeT) := {
+  compl : Compl A;
+  conv_compl n c : compl c ≡{n}≡ c n;
+}.
+Arguments compl : simpl never.
 
 (** General properties *)
 Section cofe.
-  Context {A : cofeT}.
+  Context {A : ofeT}.
   Implicit Types x y : A.
   Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
   Proof.
@@ -128,29 +119,29 @@ Section cofe.
   Proof. induction 2; eauto using dist_S. Qed.
   Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
   Proof. intros; eauto using dist_le. Qed.
-  Instance ne_proper {B : cofeT} (f : A → B)
+  Instance ne_proper {B : ofeT} (f : A → B)
     `{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100.
   Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
-  Instance ne_proper_2 {B C : cofeT} (f : A → B → C)
+  Instance ne_proper_2 {B C : ofeT} (f : A → B → C)
     `{!∀ n, Proper (dist n ==> dist n ==> dist n) f} :
     Proper ((≡) ==> (≡) ==> (≡)) f | 100.
   Proof.
      unfold Proper, respectful; setoid_rewrite equiv_dist.
      by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
   Qed.
-  Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y :
+  Lemma contractive_S {B : ofeT} (f : A → B) `{!Contractive f} n x y :
     x ≡{n}≡ y → f x ≡{S n}≡ f y.
   Proof. eauto using contractive, dist_le with omega. Qed.
-  Lemma contractive_0 {B : cofeT} (f : A → B) `{!Contractive f} x y :
+  Lemma contractive_0 {B : ofeT} (f : A → B) `{!Contractive f} x y :
     f x ≡{0}≡ f y.
   Proof. eauto using contractive with omega. Qed.
-  Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n :
+  Global Instance contractive_ne {B : ofeT} (f : A → B) `{!Contractive f} n :
     Proper (dist n ==> dist n) f | 100.
   Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
-  Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} :
+  Global Instance contractive_proper {B : ofeT} (f : A → B) `{!Contractive f} :
     Proper ((≡) ==> (≡)) f | 100 := _.
 
-  Lemma conv_compl' n (c : chain A) : compl c ≡{n}≡ c (S n).
+  Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
   Proof.
     transitivity (c n); first by apply conv_compl. symmetry.
     apply chain_cauchy. omega.
@@ -161,17 +152,17 @@ Section cofe.
   Qed.
 End cofe.
 
-Instance const_contractive {A B : cofeT} (x : A) : Contractive (@const A B x).
+Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
 Proof. by intros n y1 y2. Qed.
 
 (** Mapping a chain *)
-Program Definition chain_map `{Dist A, Dist B} (f : A → B)
+Program Definition chain_map {A B : ofeT} (f : A → B)
     `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
   {| chain_car n := f (c n) |}.
-Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
+Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
 
 (** Fixpoint *)
-Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
+Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
 Next Obligation.
   intros A ? f ? n.
@@ -180,14 +171,14 @@ Next Obligation.
   - apply (contractive_S f), IH; auto with omega.
 Qed.
 
-Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A → A)
+Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
   `{!Contractive f} : A := compl (fixpoint_chain f).
 Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed.
-Definition fixpoint {A AiH} f {Hf} := proj1_sig fixpoint_aux A AiH f Hf.
+Definition fixpoint {A AC AiH} f {Hf} := proj1_sig fixpoint_aux A AC AiH f Hf.
 Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
 
 Section fixpoint.
-  Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
+  Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
 
   Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
   Proof.
@@ -217,20 +208,15 @@ Section fixpoint.
 End fixpoint.
 
 (** Function space *)
-(* We make [cofe_fun] a definition so that we can register it as a canonical
+(* We make [ofe_fun] a definition so that we can register it as a canonical
 structure. *)
-Definition cofe_fun (A : Type) (B : cofeT) := A → B.
+Definition ofe_fun (A : Type) (B : ofeT) := A → B.
 
-Section cofe_fun.
-  Context {A : Type} {B : cofeT}.
-  Instance cofe_fun_equiv : Equiv (cofe_fun A B) := λ f g, ∀ x, f x ≡ g x.
-  Instance cofe_fun_dist : Dist (cofe_fun A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Program Definition cofe_fun_chain `(c : chain (cofe_fun A B))
-    (x : A) : chain B := {| chain_car n := c n x |}.
-  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
-  Program Instance cofe_fun_compl : Compl (cofe_fun A B) := λ c x,
-    compl (cofe_fun_chain c x).
-  Definition cofe_fun_cofe_mixin : CofeMixin (cofe_fun A B).
+Section ofe_fun.
+  Context {A : Type} {B : ofeT}.
+  Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, ∀ x, f x ≡ g x.
+  Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+  Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B).
   Proof.
     split.
     - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -240,46 +226,43 @@ Section cofe_fun.
       + by intros f g ? x.
       + by intros f g h ?? x; trans (g x).
     - by intros n f g ? x; apply dist_S.
-    - intros n c x. apply (conv_compl n (cofe_fun_chain c x)).
   Qed.
-  Canonical Structure cofe_funC := CofeT (cofe_fun A B) cofe_fun_cofe_mixin.
-End cofe_fun.
+  Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
 
-Arguments cofe_funC : clear implicits.
+  Program Definition ofe_fun_chain `(c : chain ofe_funC)
+    (x : A) : chain B := {| chain_car n := c n x |}.
+  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
+  Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
+    { compl c x := compl (ofe_fun_chain c x) }.
+  Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
+End ofe_fun.
+
+Arguments ofe_funC : clear implicits.
 Notation "A -c> B" :=
-  (cofe_funC A B) (at level 99, B at level 200, right associativity).
-Instance cofe_fun_inhabited {A} {B : cofeT} `{Inhabited B} :
+  (ofe_funC A B) (at level 99, B at level 200, right associativity).
+Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} :
   Inhabited (A -c> B) := populate (λ _, inhabitant).
 
 (** Non-expansive function space *)
-Record cofe_mor (A B : cofeT) : Type := CofeMor {
-  cofe_mor_car :> A → B;
-  cofe_mor_ne n : Proper (dist n ==> dist n) cofe_mor_car
+Record ofe_mor (A B : ofeT) : Type := CofeMor {
+  ofe_mor_car :> A → B;
+  ofe_mor_ne n : Proper (dist n ==> dist n) ofe_mor_car
 }.
 Arguments CofeMor {_ _} _ {_}.
-Add Printing Constructor cofe_mor.
-Existing Instance cofe_mor_ne.
+Add Printing Constructor ofe_mor.
+Existing Instance ofe_mor_ne.
 
 Notation "'λne' x .. y , t" :=
   (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
   (at level 200, x binder, y binder, right associativity).
 
-Section cofe_mor.
-  Context {A B : cofeT}.
-  Global Instance cofe_mor_proper (f : cofe_mor A B) : Proper ((≡) ==> (≡)) f.
-  Proof. apply ne_proper, cofe_mor_ne. Qed.
-  Instance cofe_mor_equiv : Equiv (cofe_mor A B) := λ f g, ∀ x, f x ≡ g x.
-  Instance cofe_mor_dist : Dist (cofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Program Definition cofe_mor_chain `(c : chain (cofe_mor A B))
-    (x : A) : chain B := {| chain_car n := c n x |}.
-  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
-  Program Instance cofe_mor_compl : Compl (cofe_mor A B) := λ c,
-    {| cofe_mor_car x := compl (cofe_mor_chain c x) |}.
-  Next Obligation.
-    intros c n x y Hx. by rewrite (conv_compl n (cofe_mor_chain c x))
-      (conv_compl n (cofe_mor_chain c y)) /= Hx.
-  Qed.
-  Definition cofe_mor_cofe_mixin : CofeMixin (cofe_mor A B).
+Section ofe_mor.
+  Context {A B : ofeT}.
+  Global Instance ofe_mor_proper (f : ofe_mor A B) : Proper ((≡) ==> (≡)) f.
+  Proof. apply ne_proper, ofe_mor_ne. Qed.
+  Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x.
+  Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+  Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B).
   Proof.
     split.
     - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -289,30 +272,44 @@ Section cofe_mor.
       + by intros f g ? x.
       + by intros f g h ?? x; trans (g x).
     - by intros n f g ? x; apply dist_S.
-    - intros n c x; simpl.
-      by rewrite (conv_compl n (cofe_mor_chain c x)) /=.
   Qed.
-  Canonical Structure cofe_morC := CofeT (cofe_mor A B) cofe_mor_cofe_mixin.
+  Canonical Structure ofe_morC := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
+
+  Program Definition ofe_mor_chain (c : chain ofe_morC)
+    (x : A) : chain B := {| chain_car n := c n x |}.
+  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
+  Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morC := λ c,
+    {| ofe_mor_car x := compl (ofe_mor_chain c x) |}.
+  Next Obligation.
+    intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
+      (conv_compl n (ofe_mor_chain c y)) /= Hx.
+  Qed.
+  Global Program Instance ofe_more_cofe `{Cofe B} : Cofe ofe_morC :=
+    {| compl := ofe_mor_compl |}.
+  Next Obligation.
+    intros ? n c x; simpl.
+    by rewrite (conv_compl n (ofe_mor_chain c x)) /=.
+  Qed.
 
-  Global Instance cofe_mor_car_ne n :
-    Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
+  Global Instance ofe_mor_car_ne n :
+    Proper (dist n ==> dist n ==> dist n) (@ofe_mor_car A B).
   Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
-  Global Instance cofe_mor_car_proper :
-    Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _.
-  Lemma cofe_mor_ext (f g : cofe_mor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
+  Global Instance ofe_mor_car_proper :
+    Proper ((≡) ==> (≡) ==> (≡)) (@ofe_mor_car A B) := ne_proper_2 _.
+  Lemma ofe_mor_ext (f g : ofe_mor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
   Proof. done. Qed.
-End cofe_mor.
+End ofe_mor.
 
-Arguments cofe_morC : clear implicits.
+Arguments ofe_morC : clear implicits.
 Notation "A -n> B" :=
-  (cofe_morC A B) (at level 99, B at level 200, right associativity).
-Instance cofe_mor_inhabited {A B : cofeT} `{Inhabited B} :
+  (ofe_morC A B) (at level 99, B at level 200, right associativity).
+Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
   Inhabited (A -n> B) := populate (λne _, inhabitant).
 
 (** Identity and composition and constant function *)
 Definition cid {A} : A -n> A := CofeMor id.
 Instance: Params (@cid) 1.
-Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x).
+Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x).
 Instance: Params (@cconst) 2.
 
 Definition ccompose {A B C}
@@ -324,54 +321,61 @@ Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
 Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
 
 (* Function space maps *)
-Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
+Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
   (h : A -n> B) : A' -n> B' := g â—Ž h â—Ž f.
-Instance cofe_mor_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B').
+Instance ofe_mor_map_ne {A A' B B'} n :
+  Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map A A' B B').
 Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
 
-Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
-  (A -n> B) -n> (A' -n>  B') := CofeMor (cofe_mor_map f g).
-Instance cofe_morC_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n) (@cofe_morC_map A A' B B').
+Definition ofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
+  (A -n> B) -n> (A' -n>  B') := CofeMor (ofe_mor_map f g).
+Instance ofe_morC_map_ne {A A' B B'} n :
+  Proper (dist n ==> dist n ==> dist n) (@ofe_morC_map A A' B B').
 Proof.
-  intros f f' Hf g g' Hg ?. rewrite /= /cofe_mor_map.
+  intros f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
   by repeat apply ccompose_ne.
 Qed.
 
 (** unit *)
 Section unit.
   Instance unit_dist : Dist unit := λ _ _ _, True.
-  Instance unit_compl : Compl unit := λ _, ().
-  Definition unit_cofe_mixin : CofeMixin unit.
+  Definition unit_ofe_mixin : OfeMixin unit.
   Proof. by repeat split; try exists 0. Qed.
-  Canonical Structure unitC : cofeT := CofeT unit unit_cofe_mixin.
-  Global Instance unit_discrete_cofe : Discrete unitC.
+  Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin.
+  
+  Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
+  Next Obligation. by repeat split; try exists 0. Qed.
+  
+Global Instance unit_discrete_cofe : Discrete unitC.
   Proof. done. Qed.
 End unit.
 
 (** Product *)
 Section product.
-  Context {A B : cofeT}.
+  Context {A B : ofeT}.
 
   Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
   Global Instance pair_ne :
     Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
   Global Instance fst_ne : Proper (dist n ==> dist n) (@fst A B) := _.
   Global Instance snd_ne : Proper (dist n ==> dist n) (@snd A B) := _.
-  Instance prod_compl : Compl (A * B) := λ c,
-    (compl (chain_map fst c), compl (chain_map snd c)).
-  Definition prod_cofe_mixin : CofeMixin (A * B).
+  Definition prod_ofe_mixin : OfeMixin (A * B).
   Proof.
     split.
     - intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
       rewrite !equiv_dist; naive_solver.
     - apply _.
     - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
-    - intros n c; split. apply (conv_compl n (chain_map fst c)).
-      apply (conv_compl n (chain_map snd c)).
   Qed.
-  Canonical Structure prodC : cofeT := CofeT (A * B) prod_cofe_mixin.
+  Canonical Structure prodC : ofeT := OfeT (A * B) prod_ofe_mixin.
+
+  Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodC :=
+    { compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
+  Next Obligation.
+    intros ?? n c; split. apply (conv_compl n (chain_map fst c)).
+    apply (conv_compl n (chain_map snd c)).
+  Qed.
+
   Global Instance prod_timeless (x : A * B) :
     Timeless (x.1) → Timeless (x.2) → Timeless x.
   Proof. by intros ???[??]; split; apply (timeless _). Qed.
@@ -382,7 +386,7 @@ End product.
 Arguments prodC : clear implicits.
 Typeclasses Opaque prod_dist.
 
-Instance prod_map_ne {A A' B B' : cofeT} n :
+Instance prod_map_ne {A A' B B' : ofeT} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
            dist n ==> dist n) (@prod_map A A' B B').
 Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.
@@ -394,12 +398,12 @@ Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
 (** Functors *)
 Structure cFunctor := CFunctor {
-  cFunctor_car : cofeT → cofeT → cofeT;
+  cFunctor_car : ofeT → ofeT → ofeT;
   cFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
   cFunctor_ne {A1 A2 B1 B2} n :
     Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
-  cFunctor_id {A B : cofeT} (x : cFunctor_car A B) :
+  cFunctor_id {A B : ofeT} (x : cFunctor_car A B) :
     cFunctor_map (cid,cid) x ≡ x;
   cFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
@@ -414,10 +418,10 @@ Bind Scope cFunctor_scope with cFunctor.
 Class cFunctorContractive (F : cFunctor) :=
   cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
 
-Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A.
+Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A.
 Coercion cFunctor_diag : cFunctor >-> Funclass.
 
-Program Definition constCF (B : cofeT) : cFunctor :=
+Program Definition constCF (B : ofeT) : cFunctor :=
   {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
 
@@ -450,22 +454,22 @@ Proof.
     by apply prodC_map_ne; apply cFunctor_contractive.
 Qed.
 
-Instance compose_ne {A} {B B' : cofeT} (f : B -n> B') n :
+Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') n :
   Proper (dist n ==> dist n) (compose f : (A -c> B) → A -c> B').
 Proof. intros g g' Hf x; simpl. by rewrite (Hf x). Qed.
 
-Definition cofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
+Definition ofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
   @CofeMor (_ -c> _) (_ -c> _) (compose f) _.
-Instance cofe_funC_map_ne {A B B'} n :
-  Proper (dist n ==> dist n) (@cofe_funC_map A B B').
+Instance ofe_funC_map_ne {A B B'} n :
+  Proper (dist n ==> dist n) (@ofe_funC_map A B B').
 Proof. intros f f' Hf g x. apply Hf. Qed.
 
-Program Definition cofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := cofe_funC T (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := cofe_funC_map (cFunctor_map F fg)
+Program Definition ofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := ofe_funC T (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros ?? A1 A2 B1 B2 n ???; by apply cofe_funC_map_ne; apply cFunctor_ne.
+  intros ?? A1 A2 B1 B2 n ???; by apply ofe_funC_map_ne; apply cFunctor_ne.
 Qed.
 Next Obligation. intros F1 F2 A B ??. by rewrite /= /compose /= !cFunctor_id. Qed.
 Next Obligation.
@@ -473,21 +477,21 @@ Next Obligation.
   by rewrite !cFunctor_compose.
 Qed.
 
-Instance cofe_funCF_contractive (T : Type) (F : cFunctor) :
-  cFunctorContractive F → cFunctorContractive (cofe_funCF T F).
+Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
+  cFunctorContractive F → cFunctorContractive (ofe_funCF T F).
 Proof.
   intros ?? A1 A2 B1 B2 n ???;
-    by apply cofe_funC_map_ne; apply cFunctor_contractive.
+    by apply ofe_funC_map_ne; apply cFunctor_contractive.
 Qed.
 
-Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
+Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
   cFunctor_map A1 A2 B1 B2 fg :=
-    cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
+    ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
 |}.
 Next Obligation.
   intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply cofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
+  apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
 Qed.
 Next Obligation.
   intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
@@ -498,17 +502,17 @@ Next Obligation.
   rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
 Qed.
 
-Instance cofe_morCF_contractive F1 F2 :
+Instance ofe_morCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
-  cFunctorContractive (cofe_morCF F1 F2).
+  cFunctorContractive (ofe_morCF F1 F2).
 Proof.
   intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
+  apply ofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
 Qed.
 
 (** Sum *)
 Section sum.
-  Context {A B : cofeT}.
+  Context {A B : ofeT}.
 
   Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
   Global Instance inl_ne : Proper (dist n ==> dist n) (@inl A B) := _.
@@ -516,33 +520,37 @@ Section sum.
   Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _.
   Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _.
 
-  Program Definition inl_chain (c : chain (A + B)) (a : A) : chain A :=
+  Definition sum_ofe_mixin : OfeMixin (A + B).
+  Proof.
+    split.
+    - intros x y; split=> Hx.
+      + destruct Hx=> n; constructor; by apply equiv_dist.
+      + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).
+    - apply _.
+    - destruct 1; constructor; by apply dist_S.
+  Qed.
+  Canonical Structure sumC : ofeT := OfeT (A + B) sum_ofe_mixin.
+
+  Program Definition inl_chain (c : chain sumC) (a : A) : chain A :=
     {| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
   Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-  Program Definition inr_chain (c : chain (A + B)) (b : B) : chain B :=
+  Program Definition inr_chain (c : chain sumC) (b : B) : chain B :=
     {| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
   Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
 
-  Instance sum_compl : Compl (A + B) := λ c,
+  Definition sum_compl `{Cofe A, Cofe B} : Compl sumC := λ c,
     match c 0 with
     | inl a => inl (compl (inl_chain c a))
     | inr b => inr (compl (inr_chain c b))
     end.
-
-  Definition sum_cofe_mixin : CofeMixin (A + B).
-  Proof.
-    split.
-    - intros x y; split=> Hx.
-      + destruct Hx=> n; constructor; by apply equiv_dist.
-      + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).
-    - apply _.
-    - destruct 1; constructor; by apply dist_S.
-    - intros n c; rewrite /compl /sum_compl.
-      feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-      + rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
-      + rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
+  Global Program Instance sum_cofe `{Cofe A, Cofe B} : Cofe sumC :=
+    { compl := sum_compl }.
+  Next Obligation.
+    intros ?? n c; rewrite /compl /sum_compl.
+    feed inversion (chain_cauchy c 0 n); first by auto with lia; constructor.
+    - rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
+    - rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
   Qed.
-  Canonical Structure sumC : cofeT := CofeT (A + B) sum_cofe_mixin.
 
   Global Instance inl_timeless (x : A) : Timeless x → Timeless (inl x).
   Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
@@ -555,7 +563,7 @@ End sum.
 Arguments sumC : clear implicits.
 Typeclasses Opaque sum_dist.
 
-Instance sum_map_ne {A A' B B' : cofeT} n :
+Instance sum_map_ne {A A' B B' : ofeT} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
            dist n ==> dist n) (@sum_map A A' B B').
 Proof.
@@ -593,20 +601,24 @@ Qed.
 Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
   Instance discrete_dist : Dist A := λ n x y, x ≡ y.
-  Instance discrete_compl : Compl A := λ c, c 0.
-  Definition discrete_cofe_mixin : CofeMixin A.
+  Definition discrete_ofe_mixin : OfeMixin A.
   Proof.
     split.
     - intros x y; split; [done|intros Hn; apply (Hn 0)].
     - done.
     - done.
-    - intros n c. rewrite /compl /discrete_compl /=;
-      symmetry; apply (chain_cauchy c 0 n). omega.
+  Qed.
+  
+  Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
+    { compl c := c 0 }.
+  Next Obligation.
+    intros n c. rewrite /compl /=;
+    symmetry; apply (chain_cauchy c 0 n). omega.
   Qed.
 End discrete_cofe.
 
-Notation discreteC A := (CofeT A discrete_cofe_mixin).
-Notation leibnizC A := (CofeT A (@discrete_cofe_mixin _ equivL _)).
+Notation discreteC A := (OfeT A discrete_ofe_mixin).
+Notation leibnizC A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
 
 Instance discrete_discrete_cofe `{Equiv A, @Equivalence A (≡)} :
   Discrete (discreteC A).
@@ -619,19 +631,13 @@ Canonical Structure boolC := leibnizC bool.
 
 (* Option *)
 Section option.
-  Context {A : cofeT}.
+  Context {A : ofeT}.
 
   Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
   Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
   Proof. done. Qed.
 
-  Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
-    {| chain_car n := from_option id x (c n) |}.
-  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-  Instance option_compl : Compl (option A) := λ c,
-    match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
-
-  Definition option_cofe_mixin : CofeMixin (option A).
+  Definition option_ofe_mixin : OfeMixin (option A).
   Proof.
     split.
     - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
@@ -639,11 +645,23 @@ Section option.
       by intros n; feed inversion (Hxy n).
     - apply _.
     - destruct 1; constructor; by apply dist_S.
-    - intros n c; rewrite /compl /option_compl.
-      feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-      rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
   Qed.
-  Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
+  Canonical Structure optionC := OfeT (option A) option_ofe_mixin.
+
+  Program Definition option_chain (c : chain optionC) (x : A) : chain A :=
+    {| chain_car n := from_option id x (c n) |}.
+  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+  Definition option_compl `{Cofe A} : Compl optionC := λ c,
+    match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
+  Global Program Instance option_cofe `{Cofe A} : Cofe optionC :=
+    { compl := option_compl }.
+  Next Obligation.
+    intros ? n c; rewrite /compl /option_compl.
+    feed inversion (chain_cauchy c 0 n); auto with lia; [].
+    constructor. rewrite (conv_compl n (option_chain c _)) /=.
+    destruct (c n); naive_solver.
+  Qed.
+
   Global Instance option_discrete : Discrete A → Discrete optionC.
   Proof. destruct 2; constructor; by apply (timeless _). Qed.
 
@@ -679,7 +697,7 @@ End option.
 Typeclasses Opaque option_dist.
 Arguments optionC : clear implicits.
 
-Instance option_fmap_ne {A B : cofeT} n:
+Instance option_fmap_ne {A B : ofeT} n:
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
 Proof. intros f f' Hf ?? []; constructor; auto. Qed.
 Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
@@ -716,15 +734,11 @@ Arguments Next {_} _.
 Arguments later_car {_} _.
 
 Section later.
-  Context {A : cofeT}.
+  Context {A : ofeT}.
   Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
   Instance later_dist : Dist (later A) := λ n x y,
     match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end.
-  Program Definition later_chain (c : chain (later A)) : chain A :=
-    {| chain_car n := later_car (c (S n)) |}.
-  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
-  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
-  Definition later_cofe_mixin : CofeMixin (later A).
+  Definition later_ofe_mixin : OfeMixin (later A).
   Proof.
     split.
     - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
@@ -734,9 +748,18 @@ Section later.
       + by intros [x] [y].
       + by intros [x] [y] [z] ??; trans y.
     - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
-    - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
   Qed.
-  Canonical Structure laterC : cofeT := CofeT (later A) later_cofe_mixin.
+  Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin.
+
+  Program Definition later_chain (c : chain laterC) : chain A :=
+    {| chain_car n := later_car (c (S n)) |}.
+  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
+  Global Program Instance later_cofe `{Cofe A} : Cofe laterC := 
+    { compl c := Next (compl (later_chain c)) }.
+  Next Obligation.
+    intros ? [|n] c; [done|by apply (conv_compl n (later_chain c))].
+  Qed.
+
   Global Instance Next_contractive : Contractive (@Next A).
   Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
@@ -747,7 +770,7 @@ Arguments laterC : clear implicits.
 
 Definition later_map {A B} (f : A → B) (x : later A) : later B :=
   Next (f (later_car x)).
-Instance later_map_ne {A B : cofeT} (f : A → B) n :
+Instance later_map_ne {A B : ofeT} (f : A → B) n :
   Proper (dist (pred n) ==> dist (pred n)) f →
   Proper (dist n ==> dist n) (later_map f) | 0.
 Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
@@ -756,12 +779,12 @@ Proof. by destruct x. Qed.
 Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
   later_map (g ∘ f) x = later_map g (later_map f x).
 Proof. by destruct x. Qed.
-Lemma later_map_ext {A B : cofeT} (f g : A → B) x :
+Lemma later_map_ext {A B : ofeT} (f g : A → B) x :
   (∀ x, f x ≡ g x) → later_map f x ≡ later_map g x.
 Proof. destruct x; intros Hf; apply Hf. Qed.
 Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
   CofeMor (later_map f).
-Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
+Instance laterC_map_contractive (A B : ofeT) : Contractive (@laterC_map A B).
 Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
 
 Program Definition laterCF (F : cFunctor) : cFunctor := {|
@@ -789,9 +812,9 @@ Qed.
 
 (** Notation for writing functors *)
 Notation "∙" := idCF : cFunctor_scope.
-Notation "T -c> F" := (cofe_funCF T%type F%CF) : cFunctor_scope.
-Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
+Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
+Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
 Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
 Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
 Notation "â–¶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
-Coercion constCF : cofeT >-> cFunctor.
+Coercion constCF : ofeT >-> cFunctor.
diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 53898bdb6eb83cd45ad707ec76ef1e8c70223fd5..5ac30fc76e235916ebd900675e70c7afd082aaab 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -52,7 +52,7 @@ Section cmra.
   Qed.
 
   Canonical Structure uPredR :=
-    CMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin.
+    CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin.
 
   Instance uPred_empty : Empty (uPred M) := True%I.
 
@@ -64,7 +64,7 @@ Section cmra.
   Qed.
 
   Canonical Structure uPredUR :=
-    UCMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
+    UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
 
   Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
   Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
diff --git a/base_logic/derived.v b/base_logic/derived.v
index f96df2fc73a0c352f826633c62dac27540bef61f..b822512b4897c48ff6a9e73718a3613d92a98137 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -265,12 +265,12 @@ Proof.
   - apply exist_elim=> x. eauto using pure_mono.
 Qed.
 
-Lemma internal_eq_refl' {A : cofeT} (a : A) P : P ⊢ a ≡ a.
+Lemma internal_eq_refl' {A : ofeT} (a : A) P : P ⊢ a ≡ a.
 Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
 Hint Resolve internal_eq_refl'.
-Lemma equiv_internal_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
+Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. by intros ->. Qed.
-Lemma internal_eq_sym {A : cofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
+Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
 Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
 
 Lemma pure_impl_forall φ P : (■ φ → P) ⊣⊢ (∀ _ : φ, P).
@@ -473,7 +473,7 @@ Proof.
   apply impl_intro_l; rewrite -always_and.
   apply always_mono, impl_elim with P; auto.
 Qed.
-Lemma always_internal_eq {A:cofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
+Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)); auto using always_elim.
   apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
@@ -713,7 +713,7 @@ Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
 Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
 Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
 Proof. destruct p; apply _. Qed.
-Global Instance eq_timeless {A : cofeT} (a b : A) :
+Global Instance eq_timeless {A : ofeT} (a b : A) :
   Timeless a → TimelessP (a ≡ b : uPred M)%I.
 Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
 Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
@@ -744,7 +744,7 @@ Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
 Global Instance exist_persistent {A} (Ψ : A → uPred M) :
   (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
 Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
-Global Instance internal_eq_persistent {A : cofeT} (a b : A) :
+Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
   PersistentP (a ≡ b : uPred M)%I.
 Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
diff --git a/base_logic/lib/iprop.v b/base_logic/lib/iprop.v
index 96b7ea91164df204b244040023f4037e12f5bcc5..2c16ae741412f1d8b226fa291285f76f7a59fa4c 100644
--- a/base_logic/lib/iprop.v
+++ b/base_logic/lib/iprop.v
@@ -113,7 +113,7 @@ Qed.
 the construction, this way we are sure we do not use any properties of the
 construction, and also avoid Coq from blindly unfolding it. *)
 Module Type iProp_solution_sig.
-  Parameter iPreProp : gFunctors → cofeT.
+  Parameter iPreProp : gFunctors → ofeT.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
   Notation iProp Σ := (uPredC (iResUR Σ)).
@@ -131,7 +131,7 @@ Module Export iProp_solution : iProp_solution_sig.
   Definition iProp_result (Σ : gFunctors) :
     solution (uPredCF (iResF Σ)) := solver.result _.
 
-  Definition iPreProp (Σ : gFunctors) : cofeT := iProp_result Σ.
+  Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
   Notation iProp Σ := (uPredC (iResUR Σ)).
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 6e9655d7c95b0e37690a22f4ce07c60045057c2f..0b26e7a38203145652cf817b00f9c1a0c6e3b579 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -58,7 +58,7 @@ Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
 Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
 Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
 
-Program Definition uPred_internal_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
+Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
   {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
 Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
 Definition uPred_internal_eq_aux : { x | x = @uPred_internal_eq_def }. by eexists. Qed.
@@ -248,14 +248,14 @@ Proof.
 Qed.
 Global Instance wand_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_wand M) := ne_proper_2 _.
-Global Instance internal_eq_ne (A : cofeT) n :
+Global Instance internal_eq_ne (A : ofeT) n :
   Proper (dist n ==> dist n ==> dist n) (@uPred_internal_eq M A).
 Proof.
   intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
   - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
   - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
 Qed.
-Global Instance internal_eq_proper (A : cofeT) :
+Global Instance internal_eq_proper (A : ofeT) :
   Proper ((≡) ==> (≡) ==> (⊣⊢)) (@uPred_internal_eq M A) := ne_proper_2 _.
 Global Instance forall_ne A n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
@@ -358,16 +358,16 @@ Proof. unseal; split=> n x ??; by exists a. Qed.
 Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
 Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
 
-Lemma internal_eq_refl {A : cofeT} (a : A) : True ⊢ a ≡ a.
+Lemma internal_eq_refl {A : ofeT} (a : A) : True ⊢ a ≡ a.
 Proof. unseal; by split=> n x ??; simpl. Qed.
-Lemma internal_eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
+Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) P
   {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
   unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
   - by symmetry; apply Hab with x.
   - by apply Ha.
 Qed.
-Lemma internal_eq_rewrite_contractive {A : cofeT} a b (Ψ : A → uPred M) P
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
   {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
   unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
@@ -552,25 +552,25 @@ Proof.
 Qed.
 
 (* Products *)
-Lemma prod_equivI {A B : cofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
+Lemma prod_equivI {A B : ofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
 Proof. by unseal. Qed.
 Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by unseal. Qed.
 
 (* Later *)
-Lemma later_equivI {A : cofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
+Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
 Proof. by unseal. Qed.
 
 (* Discrete *)
 Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : ✓ a ⊣⊢ ■ ✓ a.
 Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma timeless_eq {A : cofeT} (a b : A) : Timeless a → a ≡ b ⊣⊢ ■ (a ≡ b).
+Lemma timeless_eq {A : ofeT} (a b : A) : Timeless a → a ≡ b ⊣⊢ ■ (a ≡ b).
 Proof.
   unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (timeless_iff n).
 Qed.
 
 (* Option *)
-Lemma option_equivI {A : cofeT} (mx my : option A) :
+Lemma option_equivI {A : ofeT} (mx my : option A) :
   mx ≡ my ⊣⊢ match mx, my with
              | Some x, Some y => x ≡ y | None, None => True | _, _ => False
              end.
@@ -584,7 +584,7 @@ Proof. unseal. by destruct mx. Qed.
 (* Functions *)
 Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
-Lemma cofe_morC_equivI {A B : cofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma cofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
 End primitive.
 End uPred_primitive.
diff --git a/base_logic/upred.v b/base_logic/upred.v
index 710effb269111b1983712842450e73e5e18b48fa..f943c438818aa3a3ad761839247f08fdc74920be 100644
--- a/base_logic/upred.v
+++ b/base_logic/upred.v
@@ -22,14 +22,7 @@ Section cofe.
   Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
     { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
   Instance uPred_dist : Dist (uPred M) := uPred_dist'.
-  Program Instance uPred_compl : Compl (uPred M) := λ c,
-    {| uPred_holds n x := c n n x |}.
-  Next Obligation. naive_solver eauto using uPred_mono. Qed.
-  Next Obligation.
-    intros c n1 n2 x ???; simpl in *.
-    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
-  Qed.
-  Definition uPred_cofe_mixin : CofeMixin (uPred M).
+  Definition uPred_ofe_mixin : OfeMixin (uPred M).
   Proof.
     split.
     - intros P Q; split.
@@ -41,9 +34,20 @@ Section cofe.
       + intros P Q Q' HP HQ; split=> i x ??.
         by trans (Q i x);[apply HP|apply HQ].
     - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
-    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
   Qed.
-  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
+  Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.
+
+  Program Definition uPred_compl : Compl uPredC := λ c,
+    {| uPred_holds n x := c n n x |}.
+  Next Obligation. naive_solver eauto using uPred_mono. Qed.
+  Next Obligation.
+    intros c n1 n2 x ???; simpl in *.
+    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
+  Qed.
+  Global Program Instance uPred_cofe : Cofe uPredC := {| compl := uPred_compl |}.
+  Next Obligation.
+    intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
+  Qed.
 End cofe.
 Arguments uPredC : clear implicits.
 
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 2c3d37da94e5e21ed34c5ea12214ab2de45622b0..3ea46c969453c7ecd2a64007b343bc12e5b770d3 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export ectx_language ectxi_language.
-From iris.algebra Require Export cofe.
+From iris.algebra Require Export ofe.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
 
diff --git a/program_logic/language.v b/program_logic/language.v
index cd33108da2ea94c753a0081d1361f5565391fca9..a1955ed2fe86387a1aa62dc778d2e8c8c0652ea9 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cofe.
+From iris.algebra Require Export ofe.
 
 Structure language := Language {
   expr : Type;
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 305ba447d24b52c61c62f67b7c9f4e62dd9fe5df..e184e233ff1b26ba8585f16608d6e5d3f2842720 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -23,7 +23,7 @@ Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
 (* IntoPure *)
 Global Instance into_pure_pure φ : @IntoPure M (■ φ) φ.
 Proof. done. Qed.
-Global Instance into_pure_eq {A : cofeT} (a b : A) :
+Global Instance into_pure_eq {A : ofeT} (a b : A) :
   Timeless a → @IntoPure M (a ≡ b) (a ≡ b).
 Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
 Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
@@ -33,7 +33,7 @@ Proof. by rewrite /IntoPure discrete_valid. Qed.
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure M (■ φ) φ.
 Proof. done. Qed.
-Global Instance from_pure_internal_eq {A : cofeT} (a b : A) :
+Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
   @FromPure M (a ≡ b) (a ≡ b).
 Proof.
   rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply internal_eq_refl'.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 2becccbe8c8ebcae99007fc011d783378cee466a..234fa9086b9f79c84657371fe43d96988b56d0e4 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -649,7 +649,7 @@ Qed.
 (** * Rewriting *)
 Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
   envs_lookup i Δ = Some (p, Pxy) →
-  ∀ {A : cofeT} (x y : A) (Φ : A → uPred M),
+  ∀ {A : ofeT} (x y : A) (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (Q ⊣⊢ Φ (if lr then y else x)) →
     (∀ n, Proper (dist n ==> dist n) Φ) →
@@ -663,7 +663,7 @@ Qed.
 Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
-  ∀ {A : cofeT} Δ' x y (Φ : A → uPred M),
+  ∀ {A : ofeT} Δ' x y (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (P ⊣⊢ Φ (if lr then y else x)) →
     (∀ n, Proper (dist n ==> dist n) Φ) →
diff --git a/tests/counter.v b/tests/counter.v
index 62251deb90ef392b7e5dbf72a833453a12c1e3b9..053a5b7ba48c395bbf6a38ed204c6996f226b59b 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -26,7 +26,7 @@ Section M.
   Arguments op _ _ !_ !_/.
   Arguments core _ _ !_/.
 
-  Canonical Structure M_C : cofeT := leibnizC M.
+  Canonical Structure M_C : ofeT := leibnizC M.
 
   Instance M_valid : Valid M := λ x, x ≠ Bot.
   Instance M_op : Op M := λ x y,