diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index bb073f09eec4d48b033c5d34c3654dd8272f7753..f6760860b749efffeffde2fc390c5e401a70acd1 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -16,10 +16,10 @@ Instance subG_relocPreG {Σ} : subG relocΣ Σ → relocPreG Σ.
 Proof. solve_inG. Qed.
 
 Definition pure_lty2 `{relocG Σ} (P : val → val → Prop) :=
-  Lty2 (λ v v', ⌜P v v'⌝)%I.
+  @Lty2 Σ (λ v v', ⌜P v v'⌝)%I _.
 
 Lemma refines_adequate Σ `{relocPreG Σ}
-  (A : ∀ `{relocG Σ}, lty2)
+  (A : ∀ `{relocG Σ}, lty2 Σ)
   (P : val → val → Prop) e e' σ :
   (∀ `{relocG Σ}, ∀ v v', A v v' -∗ pure_lty2 P v v') →
   (∀ `{relocG Σ}, {⊤;∅} ⊨ e << e' : A) →
@@ -65,7 +65,7 @@ Proof.
 Qed.
 
 Theorem refines_typesafety Σ `{relocPreG Σ} e e' e1
-        (A : ∀ `{relocG Σ}, lty2) thp σ σ' :
+        (A : ∀ `{relocG Σ}, lty2 Σ) thp σ σ' :
   (∀ `{relocG Σ}, {⊤;∅} ⊨ e << e' : A) →
   rtc erased_step ([e], σ) (thp, σ') → e1 ∈ thp →
   is_Some (to_val e1) ∨ reducible e1 σ'.
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index 0c7f4ea940ddb48da0c0085f3c0d7954d4b78b53..d64938843bad863d0f5a37461ec384cb3502e622 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -8,7 +8,7 @@ From reloc.logic Require Export model rules.
 
 Section rules.
   Context `{relocG Σ}.
-  Implicit Types A : lty2.
+  Implicit Types A : lty2 Σ.
 
   Lemma refines_weaken E Γ e1 e2 A A' :
     (∀ v1 v2, A v1 v2 ={⊤}=∗ A' v1 v2) -∗
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 4685a86bf81fc4aab72ffde865531f177104e25c..ab777056cf5e8bb10838b54985cf952ef0e6b5f2 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -11,29 +11,29 @@ From reloc Require Import prelude.tactics logic.spec_rules prelude.ctx_subst.
 From reloc Require Export logic.spec_ra.
 
 (** Semantic intepretation of types *)
-Record lty2 `{invG Σ} := Lty2 {
+Record lty2 Σ := Lty2 {
   lty2_car :> val → val → iProp Σ;
   lty2_persistent v1 v2 : Persistent (lty2_car v1 v2)
 }.
-Arguments Lty2 {_ _} _%I {_}.
-Arguments lty2_car {_ _} _ _ _ : simpl never.
+Arguments Lty2 {_} _%I {_}.
+Arguments lty2_car {_} _ _ _ : simpl never.
 Bind Scope lty_scope with lty2.
 Delimit Scope lty_scope with lty2.
 Existing Instance lty2_persistent.
 
 (* The COFE structure on semantic types *)
 Section lty2_ofe.
-  Context `{invG Σ}.
+  Context `{Σ : gFunctors}.
 
-  Instance lty2_equiv : Equiv lty2 := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
-  Instance lty2_dist : Dist lty2 := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
-  Lemma lty2_ofe_mixin : OfeMixin lty2.
-  Proof. by apply (iso_ofe_mixin (lty2_car : lty2 → (val -c> val -c> iProp Σ))). Qed.
-  Canonical Structure lty2C := OfeT lty2 lty2_ofe_mixin.
+  Instance lty2_equiv : Equiv (lty2 Σ) := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
+  Instance lty2_dist : Dist (lty2 Σ) := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
+  Lemma lty2_ofe_mixin : OfeMixin (lty2 Σ).
+  Proof. by apply (iso_ofe_mixin (lty2_car : lty2 Σ → (val -c> val -c> iProp Σ))). Qed.
+  Canonical Structure lty2C := OfeT (lty2 Σ) lty2_ofe_mixin.
 
   Global Instance lty2_cofe : Cofe lty2C.
   Proof.
-    apply (iso_cofe_subtype' (λ A : val -c> val -c> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@Lty2 _ _) lty2_car)=>//.
+    apply (iso_cofe_subtype' (λ A : val -c> val -c> iProp Σ, ∀ w1 w2, Persistent (A w1 w2)) (@Lty2 _) lty2_car)=>//.
     - apply _.
     - apply limit_preserving_forall=> w1.
       apply limit_preserving_forall=> w2.
@@ -41,7 +41,7 @@ Section lty2_ofe.
       intros n P Q HPQ. apply (HPQ w1 w2).
   Qed.
 
-  Global Instance lty2_inhabited : Inhabited lty2 := populate (Lty2 inhabitant).
+  Global Instance lty2_inhabited : Inhabited (lty2 Σ) := populate (Lty2 inhabitant).
 
   Global Instance lty2_car_ne n : Proper (dist n ==> (=) ==> (=) ==> dist n) lty2_car.
   Proof. by intros A A' ? w1 w2 <- ? ? <-. Qed.
@@ -49,13 +49,16 @@ Section lty2_ofe.
   Proof. solve_proper_from_ne. Qed.
 End lty2_ofe.
 
+Arguments lty2C : clear implicits.
+
 Section semtypes.
   Context `{relocG Σ}.
 
-  Implicit Types A B : lty2.
+  Implicit Types e : expr.
+  Implicit Types E : coPset.
+  Implicit Types A B : lty2 Σ.
 
-  Definition interp_expr (E : coPset) (e e' : expr)
-             (A : lty2) : iProp Σ :=
+  Definition interp_expr E e e' A : iProp Σ :=
     (∀ j K, j ⤇ fill K e'
     ={E,⊤}=∗ WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }})%I.
 
@@ -67,26 +70,26 @@ Section semtypes.
     Proper ((≡) ==> (≡)) (interp_expr E e e').
   Proof. apply ne_proper=>n. apply _. Qed.
 
-  Definition lty2_unit : lty2 := Lty2 (λ w1 w2, ⌜ w1 = #() ∧ w2 = #() ⌝%I).
-  Definition lty2_bool : lty2 := Lty2 (λ w1 w2, ∃ b : bool, ⌜ w1 = #b ∧ w2 = #b ⌝)%I.
-  Definition lty2_int : lty2 := Lty2 (λ w1 w2, ∃ n : Z, ⌜ w1 = #n ∧ w2 = #n ⌝)%I.
+  Definition lty2_unit : lty2 Σ := Lty2 (λ w1 w2, ⌜ w1 = #() ∧ w2 = #() ⌝%I).
+  Definition lty2_bool : lty2 Σ := Lty2 (λ w1 w2, ∃ b : bool, ⌜ w1 = #b ∧ w2 = #b ⌝)%I.
+  Definition lty2_int : lty2 Σ := Lty2 (λ w1 w2, ∃ n : Z, ⌜ w1 = #n ∧ w2 = #n ⌝)%I.
 
-  Definition lty2_arr (A1 A2 : lty2) : lty2 := Lty2 (λ w1 w2,
+  Definition lty2_arr (A1 A2 : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
     □ ∀ v1 v2, A1 v1 v2 -∗ interp_expr ⊤ (App w1 v1) (App w2 v2) A2)%I.
 
-  Definition lty2_ref (A : lty2) : lty2 := Lty2 (λ w1 w2,
+  Definition lty2_ref (A : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
     ∃ l1 l2: loc, ⌜w1 = #l1⌝ ∧ ⌜w2 = #l2⌝ ∧
       inv (relocN .@ "ref" .@ (l1,l2)) (∃ v1 v2, l1 ↦ v1 ∗ l2 ↦ₛ v2 ∗ A v1 v2))%I.
 
-  Definition lty2_prod (A B : lty2) : lty2 := Lty2 (λ w1 w2,
+  Definition lty2_prod (A B : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
     ∃ v1 v2 v1' v2', ⌜w1 = (v1,v1')%V⌝ ∧ ⌜w2 = (v2,v2')%V⌝ ∧
         A v1 v2 ∗ B v1' v2')%I.
 
-  Definition lty2_sum (A B : lty2) : lty2 := Lty2 (λ w1 w2,
+  Definition lty2_sum (A B : lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
     ∃ v1 v2, (⌜w1 = InjLV v1⌝ ∧ ⌜w2 = InjLV v2⌝ ∧ A v1 v2)
           ∨  (⌜w1 = InjRV v1⌝ ∧ ⌜w2 = InjRV v2⌝ ∧ B v1 v2))%I.
 
-  Definition lty2_rec1 (C : lty2C -n> lty2C) (rec : lty2) : lty2 :=
+  Definition lty2_rec1 (C : lty2C Σ -n> lty2C Σ) (rec : lty2 Σ) : lty2 Σ :=
     Lty2 (λ w1 w2, ▷ C rec w1 w2)%I.
   Instance lty2_rec1_contractive C : Contractive (lty2_rec1 C).
   Proof.
@@ -97,10 +100,10 @@ Section semtypes.
     simpl in HPQ; simpl. f_equiv. by apply C.
   Qed.
 
-  Definition lty2_rec (C : lty2C -n> lty2C) : lty2 := fixpoint (lty2_rec1 C).
+  Definition lty2_rec (C : lty2C Σ -n> lty2C Σ) : lty2 Σ := fixpoint (lty2_rec1 C).
 
-  Definition lty2_exists (C : lty2 → lty2) : lty2 := Lty2 (λ w1 w2,
-    ∃ A : lty2, C A w1 w2)%I.
+  Definition lty2_exists (C : lty2 Σ → lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+    ∃ A, C A w1 w2)%I.
 
   (** The lty2 constructors are non-expansive *)
   Instance lty2_prod_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_prod.
@@ -113,7 +116,7 @@ Section semtypes.
   Proof. solve_proper. Qed.
 
   Instance lty2_rec_ne n : Proper (dist n ==> dist n)
-                                   (lty2_rec : (lty2C -n> lty2C) -> lty2C).
+                                   (lty2_rec : (lty2C Σ -n> lty2C Σ) -> lty2C Σ).
   Proof.
     intros F F' HF.
     unfold lty2_rec, lty2_car.
@@ -123,7 +126,7 @@ Section semtypes.
     apply lty2_car_ne; eauto.
   Qed.
 
-  Lemma lty_rec_unfold (C : lty2C -n> lty2C) : lty2_rec C ≡ lty2_rec1 C (lty2_rec C).
+  Lemma lty_rec_unfold (C : lty2C Σ -n> lty2C Σ) : lty2_rec C ≡ lty2_rec1 C (lty2_rec C).
   Proof. apply fixpoint_unfold. Qed.
 
 End semtypes.
@@ -134,7 +137,7 @@ Infix "→" := lty2_arr : lty_scope.
 Notation "'ref' A" := (lty2_ref A) : lty_scope.
 
 (* The semantic typing judgment *)
-Definition env_ltyped2 `{relocG Σ} (Γ : gmap string lty2)
+Definition env_ltyped2 `{relocG Σ} (Γ : gmap string (lty2 Σ))
     (vs : gmap string (val*val)) : iProp Σ :=
   (⌜ ∀ x, is_Some (Γ !! x) ↔ is_Some (vs !! x) ⌝ ∧
   [∗ map] i ↦ Avv ∈ map_zip Γ vs, lty2_car Avv.1 Avv.2.1 Avv.2.2)%I.
@@ -221,8 +224,8 @@ Section refinement.
   Context `{relocG Σ}.
 
   Definition refines_def  (E : coPset)
-           (Γ : gmap string lty2)
-           (e e' : expr) (A : lty2) : iProp Σ :=
+           (Γ : gmap string (lty2 Σ))
+           (e e' : expr) (A : lty2 Σ) : iProp Σ :=
     (∀ vvs ρ, spec_ctx ρ -∗
               env_ltyped2 Γ vvs -∗
               interp_expr E (subst_map (fst <$> vvs) e)
@@ -253,7 +256,7 @@ Section semtypes_properties.
 
   (* The reference type relation is functional and injective.
      Thanks to Amin. *)
-  Lemma interp_ref_funct E (A : lty2) (l l1 l2 : loc) :
+  Lemma interp_ref_funct E (A : lty2 Σ) (l l1 l2 : loc) :
     ↑relocN ⊆ E →
     (ref A)%lty2 #l #l1 ∗ (ref A)%lty2 #l #l2
     ={E}=∗ ⌜l1 = l2⌝.
@@ -269,7 +272,7 @@ Section semtypes_properties.
     compute in Hfoo. eauto.
   Qed.
 
-  Lemma interp_ref_inj E (A : lty2) (l l1 l2 : loc) :
+  Lemma interp_ref_inj E (A : lty2 Σ) (l l1 l2 : loc) :
     ↑relocN ⊆ E →
     (ref A)%lty2 #l1 #l ∗ (ref A)%lty2 #l2 #l
     ={E}=∗ ⌜l1 = l2⌝.
@@ -285,7 +288,7 @@ Section semtypes_properties.
     compute in Hfoo. eauto.
   Qed.
 
-  Lemma interp_ret (A : lty2) E e1 e2 v1 v2 :
+  Lemma interp_ret (A : lty2 Σ) E e1 e2 v1 v2 :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     (|={E,⊤}=> A v1 v2)%I -∗ interp_expr E e1 e2 A.
@@ -298,8 +301,8 @@ End semtypes_properties.
 
 Section environment_properties.
   Context `{relocG Σ}.
-  Implicit Types A B : lty2.
-  Implicit Types Γ : gmap string lty2.
+  Implicit Types A B : lty2 Σ.
+  Implicit Types Γ : gmap string (lty2 Σ).
 
   Lemma env_ltyped2_lookup Γ vs x A :
     Γ !! x = Some A →
@@ -433,7 +436,7 @@ Section monadic.
     by rewrite !subst_map_fill /=.
   Qed.
 
-  Lemma refines_ret E Γ e1 e2 v1 v2 (A : lty2) :
+  Lemma refines_ret E Γ e1 e2 v1 v2 (A : lty2 Σ) :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     (|={E,⊤}=> A v1 v2) -∗ {E;Γ} ⊨ e1 << e2 : A.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index c6e7265100893183affdad5d95068f34d887a711..aaeb81b87240c018d87a9d1571ece0156a1f2aaa 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -9,7 +9,7 @@ From reloc.prelude Require Import ctx_subst.
 
 Section rules.
   Context `{relocG Σ}.
-  Implicit Types A : lty2.
+  Implicit Types A : lty2 Σ.
   Implicit Types e t : expr.
   Implicit Types v w : val.
 
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index 5dabd4f228cfddf7851251722bcae7429b68cfc3..6bce1bc7d06cce309f12575f46b910867fb0dd48 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -5,7 +5,7 @@ From iris.heap_lang Require Import lang notation.
 Section test.
 Context `{relocG Σ}.
 
-Definition EqI : lty2 := Lty2 (λ v1 v2, ⌜v1 = v2⌝)%I.
+Definition EqI : lty2 Σ := Lty2 (λ v1 v2, ⌜v1 = v2⌝)%I.
 (* Pure reductions *)
 Lemma test1 Γ A P t :
   ▷ P -∗
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index fe5b2c6649657ee73cad44813a0a9ed0d068cc03..25bcb575bf9a496278bf88d9faecfff8a35b6536 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -10,7 +10,7 @@ From Autosubst Require Import Autosubst.
 
 Section fundamental.
   Context `{relocG Σ}.
-  Implicit Types Δ : listC lty2C.
+  Implicit Types Δ : listC (lty2C Σ).
   Hint Resolve to_of_val.
 
   (** TODO: actually use this folding tactic *)
@@ -287,7 +287,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_tlam Δ Γ (e e' : expr) τ :
-    (∀ (A : lty2),
+    (∀ (A : lty2 Σ),
       □ ({(A::Δ);⤉Γ} ⊨ e ≤log≤ e' : τ)) -∗
     {Δ;Γ} ⊨ (Λ: e) ≤log≤ (Λ: e') : TForall τ.
   Proof.
@@ -395,7 +395,7 @@ Section fundamental.
     by rewrite -interp_subst.
   Qed.
 
-  Lemma bin_log_related_tapp (τi : lty2) Δ Γ e e' τ :
+  Lemma bin_log_related_tapp (τi : lty2 Σ) Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : TForall τ) -∗
     {τi::Δ;⤉Γ} ⊨ (TApp e) ≤log≤ (TApp e') : τ.
   Proof.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index c92a1ec053f6fb71131e61b6051534a13801e407..3520d593177833720295756baede2824047d3672 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -11,12 +11,12 @@ Section semtypes.
   Context `{relocG Σ}.
   (** Type-level lambdas are interpreted as closures *)
   (** DF: lty2_forall is defined here because it depends on TApp *)
-  Definition lty2_forall (C : lty2 → lty2) : lty2 := Lty2 (λ w1 w2,
-    □ ∀ A : lty2, interp_expr ⊤ (TApp w1) (TApp w2) (C A))%I.
-  Definition lty2_true : lty2 := Lty2 (λ w1 w2, True)%I.
+  Definition lty2_forall (C : lty2 Σ → lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+    □ ∀ A : lty2 Σ, interp_expr ⊤ (TApp w1) (TApp w2) (C A))%I.
+  Definition lty2_true : lty2 Σ := Lty2 (λ w1 w2, True)%I.
 
-  Program Definition ctx_lookup (x : var) : listC lty2C -n> lty2C := λne Δ,
-    (from_option id lty2_true (Δ !! x))%I.
+  Program Definition ctx_lookup (x : var) : listC (lty2C Σ) -n> (lty2C Σ)
+    := λne Δ, (from_option id lty2_true (Δ !! x))%I.
   Next Obligation.
     intros x n Δ Δ' HΔ.
     destruct (Δ !! x) as [P|] eqn:HP; cbn in *.
@@ -29,8 +29,8 @@ Section semtypes.
       rewrite HP in HP'. inversion HP'.
   Qed.
 
-  Program Fixpoint interp (Ï„ : type) : listC lty2C -n> lty2C :=
-    match Ï„ as _ return listC lty2C -n> lty2C with
+  Program Fixpoint interp (τ : type) : listC (lty2C Σ) -n> lty2C Σ :=
+    match τ as _ return listC (lty2C Σ) -n> lty2C Σ with
     | TUnit => λne _, lty2_unit
     | TNat => λne _, lty2_int
     | TBool => λne _, lty2_bool
@@ -80,7 +80,7 @@ Section semtypes.
   Qed.
 
   Definition bin_log_related (E : coPset)
-             (Δ : list lty2) (Γ : stringmap type)
+             (Δ : list (lty2 Σ)) (Γ : stringmap type)
              (e e' : expr) (τ : type) : iProp Σ :=
     {E;fmap (λ τ, interp τ Δ) Γ} ⊨ e << e' : (interp τ Δ).
 
@@ -111,10 +111,10 @@ Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 1
 
 Section interp_ren.
   Context `{relocG Σ}.
-  Implicit Types Δ : list lty2.
+  Implicit Types Δ : list (lty2 Σ).
 
   (* TODO: why do I need to unfold lty2_car here? *)
-  Lemma interp_ren_up (Δ1 Δ2 : list lty2) τ τi :
+  Lemma interp_ren_up (Δ1 Δ2 : list (lty2 Σ)) τ τi :
     interp τ (Δ1 ++ Δ2) ≡ interp (τ.[upn (length Δ1) (ren (+1)%nat)]) (Δ1 ++ τi :: Δ2).
   Proof.
     revert Δ1 Δ2. induction τ => Δ1 Δ2; simpl; eauto;
@@ -145,7 +145,7 @@ Section interp_ren.
     symmetry. apply (interp_ren_up []).
   Qed.
 
-  Lemma interp_weaken (Δ1 Π Δ2 : list lty2) τ :
+  Lemma interp_weaken (Δ1 Π Δ2 : list (lty2 Σ)) τ :
     interp (τ.[upn (length Δ1) (ren (+ length Π))]) (Δ1 ++ Π ++ Δ2)
     ≡ interp τ (Δ1 ++ Δ2).
   Proof.
@@ -165,7 +165,7 @@ Section interp_ren.
         by apply (IHÏ„ (_ :: _)).
   Qed.
 
-  Lemma interp_subst_up (Δ1 Δ2 : list lty2) τ τ' :
+  Lemma interp_subst_up (Δ1 Δ2 : list (lty2 Σ)) τ τ' :
     interp τ (Δ1 ++ interp τ' Δ2 :: Δ2)
     ≡ interp (τ.[upn (length Δ1) (τ' .: ids)]) (Δ1 ++ Δ2).
   Proof.