diff --git a/theories/examples/delim_lang/hom.v b/theories/examples/delim_lang/hom.v
index 74b28da..7aad45a 100644
--- a/theories/examples/delim_lang/hom.v
+++ b/theories/examples/delim_lang/hom.v
@@ -16,6 +16,11 @@ Section hom.
   Notation IT := (IT F R).
   Notation ITV := (ITV F R).
 
+  Program Definition 𝒫_HOM : HOM (A:=natO) := exist _ 𝒫 _.
+  Next Obligation.
+    apply _.
+  Qed.
+
   Program Definition AppContRSCtx_HOM {S : Set}
     (α : @interp_scope F R _ S -n> IT)
     (env : @interp_scope F R _ S)
diff --git a/theories/examples/delim_lang/logpred.v b/theories/examples/delim_lang/logpred.v
index 7401ef7..f1ae73e 100644
--- a/theories/examples/delim_lang/logpred.v
+++ b/theories/examples/delim_lang/logpred.v
@@ -213,11 +213,6 @@ Section logrel.
     iApply "H".
   Qed.
 
-  Program Definition 𝒫_HOM : @HOM sz CtxDep R _ rs := exist _ 𝒫 _.
-  Next Obligation.
-    apply _.
-  Qed.
-
   Lemma compat_shift {S : Set} (Γ : S -> ty) e σ α τ β :
     ⊢ valid (Γ ▹ (Tcont τ α)) e σ σ β -∗ valid Γ (interp_shift _ e) τ α β.
   Proof.
diff --git a/theories/examples/delim_lang/logrel.v b/theories/examples/delim_lang/logrel.v
index f52634c..5d29269 100644
--- a/theories/examples/delim_lang/logrel.v
+++ b/theories/examples/delim_lang/logrel.v
@@ -314,11 +314,6 @@ Section logrel.
     assumption.
   Qed.
 
-  Program Definition 𝒫_HOM : @HOM sz CtxDep R _ rs := exist _ 𝒫 _.
-  Next Obligation.
-    apply _.
-  Qed.
-
   Lemma compat_shift {S : Set} (Γ : S -> ty) e (e' : exprO (inc S)) σ α τ β :
     ⊢ valid (Γ ▹ (τ ⤑ α)) e e' σ σ β -∗ valid Γ (interp_shift _ e) (shift/cc e') τ α β.
   Proof.
diff --git a/theories/examples/input_lang_callcc/hom.v b/theories/examples/input_lang_callcc/hom.v
index 5b332f3..0b5e227 100644
--- a/theories/examples/input_lang_callcc/hom.v
+++ b/theories/examples/input_lang_callcc/hom.v
@@ -1,5 +1,4 @@
-(** In this module, we package up IT homomorphism in a sigma type, and
-we will use it as a domain for logical relations on continuations *)
+(** Particular homomorphisms for the call/cc lang *)
 From gitrees Require Import gitree lang_generic.
 From gitrees Require Export hom.
 From gitrees.examples.input_lang_callcc Require Import lang interp.
@@ -74,8 +73,8 @@ Section hom.
   Qed.
 
   Program Definition OutputSCtx_HOM {S : Set}
-    (env : @interp_scope F A _ S)
-    : @HOM _ _ A _ _ := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
+    (env : @interp_scope F A _ S) : HOM (A:=natO)
+    := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
   Next Obligation.
     intros; simpl.
     apply _.
diff --git a/theories/hom.v b/theories/hom.v
index fa20f10..178179b 100644
--- a/theories/hom.v
+++ b/theories/hom.v
@@ -1,3 +1,5 @@
+(** In this module, we package up IT homomorphism in a sigma type, and
+we will use it as a domain for logical relations on continuations *)
 From gitrees Require Import gitree lang_generic.
 Require Import Binding.Lib Binding.Set Binding.Env.