diff --git a/theories/examples/generative.v b/theories/examples/generative.v
index d064b772ffa6f7816cfa07484ed77daef4de204f..8a1183b49fc3fc78e972427b99f694dbd3c37097 100644
--- a/theories/examples/generative.v
+++ b/theories/examples/generative.v
@@ -41,7 +41,7 @@ Section namegen_refinement.
                         end)%I.
 
   Lemma nameGen_ref1 :
-    REL nameGen1 << nameGen2 : ∃ α, (() → α) × (α → α → lty2_bool).
+    REL nameGen1 << nameGen2 : ∃ α, (() → α) * (α → α → lty2_bool).
   Proof.
     unlock nameGen1 nameGen2.
     rel_alloc_r c as "Hc".
@@ -164,7 +164,7 @@ Section cell_refinement.
      ∗ cellInt R r1 r2 r3 l r)%I.
 
   Lemma cell2_cell1_refinement :
-    REL cell2 << cell1 : ∀ α, ∃ β, (α → β) × (β → α) × (β → α → ()).
+    REL cell2 << cell1 : ∀ α, ∃ β, (α → β) * (β → α) * (β → α → ()).
   Proof.
     unlock cell2 cell1.
     (* TODO: this uuugly *)
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 4f20284953a0e8dfc301c893665e51309368d788..802e198ec72a195f819da02ac4c056b797c5097d 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -15,8 +15,8 @@ From reloc.typing Require Import interp soundness.
 (** * Symbol table *)
 Definition lty_symbol `{relocG Σ} : lty2 Σ :=
   ∃ α, (α → α → lty2_bool)    (* equality check *)
-     × (lty2_int → α)          (* insert *)
-     × (α → lty2_int).         (* lookup *)
+     * (lty2_int → α)          (* insert *)
+     * (α → lty2_int).         (* lookup *)
 
 Definition eqKey : val := λ: "n" "m", "n" = "m".
 Definition symbol1 : val := λ: <>,
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index 7b7e23174736a18727b6a04392c2664db8a096fa..e02c6500732823155beadd9b9ff914ca553a1fce 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -194,7 +194,7 @@ Section CG_Counter.
   Qed.
 
   Lemma FG_CG_counter_refinement :
-    REL FG_counter << CG_counter : (() → (() → lty2_int) × (() → lty2_int))%lty2.
+    REL FG_counter << CG_counter : () → (() → lty2_int) * (() → lty2_int).
   Proof.
     unfold FG_counter, CG_counter. unlock.
     iApply refines_arrow_val.
diff --git a/theories/lib/list.v b/theories/lib/list.v
index deed975e1fc6262e25690b2ec6158181592961cc..a6a7b475306032c15bd79ca23c6ef74208948ce7 100644
--- a/theories/lib/list.v
+++ b/theories/lib/list.v
@@ -14,10 +14,8 @@ Fixpoint is_list (hd : val) (xs : list val) : Prop :=
   | x :: xs => ∃ hd', hd = CONSV x hd' ∧ is_list hd' xs
   end.
 
-(* TODO: is it possible to do this without `Program Definition`? *)
-(* TODO: notation for lty_sum *)
 Program Definition lty_list `{relocG Σ} (A : lty2 Σ) : lty2 Σ :=
-  lty2_rec (λne B, lty2_sum () (A × B))%lty2.
+  lty2_rec (λne B, () + (A * B))%lty2.
 Next Obligation. solve_proper. Qed.
 
 Definition nth : val := rec: "nth" "l" "n" :=
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 57e11a9a0626cb0ff3ee4fbd59dea0da137f4d68..b34bfb6e87195a4b62ac0f1d6720dc5ff5604e1b 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -22,7 +22,7 @@ Section compatibility.
   Lemma refines_pair e1 e2 e1' e2' A B :
     (REL e1 << e1' : A) -∗
     (REL e2 << e2' : B) -∗
-    REL (e1, e2) << (e1', e2') : A × B.
+    REL (e1, e2) << (e1', e2') : A * B.
   Proof.
     iIntros "IH1 IH2".
     rel_bind_ap e2 e2' "IH2" v2 v2' "Hvv2".
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 3f88adf863359caf9458c2e6f0f4a2d252145abf..a46721f3354d2623a7f4fbeec5abca7f18a6a448 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -142,7 +142,8 @@ End semtypes.
 (** Nice notations *)
 Notation "()" := lty2_unit : lty_scope.
 Infix "→" := lty2_arr : lty_scope.
-Infix "×" := lty2_prod (at level 80) : lty_scope.
+Infix "*" := lty2_prod : lty_scope.
+Infix "+" := lty2_sum : lty_scope.
 Notation "'ref' A" := (lty2_ref A) : lty_scope.
 Notation "∃ A1 .. An , C" :=
   (lty2_exists (λ A1, .. (lty2_exists (λ An, C%lty2)) ..)) : lty_scope.