diff --git a/Cubical/Categories/Constructions/DisplayedCategory/DisplayedPoset.agda b/Cubical/Categories/Constructions/DisplayedCategory/DisplayedPoset.agda
index f0df58f1..e6e6873b 100644
--- a/Cubical/Categories/Constructions/DisplayedCategory/DisplayedPoset.agda
+++ b/Cubical/Categories/Constructions/DisplayedCategory/DisplayedPoset.agda
@@ -39,7 +39,7 @@ module _ {ℓC ℓC' : Level} {ℓP : Level} (C : Category ℓC ℓC') where
             → (k : D-Hom f [ x , y ]) → (l : D-Hom g [ y , z ])
             → D-Hom (f ⋆⟨ C ⟩ g) [ x , z ]
 
-  DisplayedPoset→Cat : (D : DisplayedPoset) → (DisplayedCategory {_} {_} {ℓP} C)
+  DisplayedPoset→Cat : (D : DisplayedPoset) → (DisplayedCategory C ℓP)
   DisplayedPoset→Cat D = record
     { D-ob = D-ob
     ; D-Hom_[_,_] = D-Hom_[_,_]
diff --git a/Cubical/Categories/Constructions/DisplayedCategory/Grothendieck.agda b/Cubical/Categories/Constructions/DisplayedCategory/Grothendieck.agda
index dd51a5c8..cefbccd7 100644
--- a/Cubical/Categories/Constructions/DisplayedCategory/Grothendieck.agda
+++ b/Cubical/Categories/Constructions/DisplayedCategory/Grothendieck.agda
@@ -23,7 +23,7 @@ module _ {ℓC ℓC' : Level} {ℓP : Level} (C : Category ℓC ℓC') where
 
   -- The Grothendieck construction, or the generalized construction
   -- for a subcategory
-  Grothendieck : DisplayedCategory {_} {_} {ℓP} C → Category _ _
+  Grothendieck : DisplayedCategory C ℓP → Category _ _
   Grothendieck D = record
     { ob =  Σ[ x ∈ C .ob ] D-ob x
     ; Hom[_,_] = λ (x , Dx) (y , Dy) →