fix broken uses of DisplayedCaetgory

maxsnew · Jul 1, 2023 · b7a6b78 · b7a6b78
1 parent 2f0f9b3
commit b7a6b78
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
@@ -21,7 +21,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) →  Σ[ f ∈ C [ x , y ] ] D-Hom f [ Dx , Dy ]