From 7ffb9265303f12dd3b63a2beb9830240e4f71fbc Mon Sep 17 00:00:00 2001 From: Max New Date: Sat, 1 Jul 2023 17:32:02 -0400 Subject: [PATCH] fix broken uses of DisplayedCaetgory --- .../Constructions/DisplayedCategory/DisplayedPoset.agda | 2 +- .../Constructions/DisplayedCategory/Grothendieck.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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) →