fix broken uses of DisplayedCaetgory

maxsnew · Jul 5, 2023 · 7ffb926 · 7ffb926
1 parent 9bdb1a8
commit 7ffb926
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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) →