that weaken gives a CartesianCategoryᴰ is already in cd1fb53

in PR #117
maxsnew · Dec 10, 2024 · 274ceb4 · 274ceb4
1 parent d7e1dbd
commit 274ceb4
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Cartesian.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Cartesian.agda
@@ -26,6 +26,8 @@ module _ (C : CartesianCategory ℓC ℓC') (D : CartesianCategory ℓD ℓD') w
   private
     module C = CartesianCategoryNotation C
     module D = CartesianCategoryNotation D
+  -- TODO: this is Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda
+  -- in PR #117
   weaken : CartesianCategoryᴰ C ℓD ℓD'
   weaken .fst = Weaken.weaken (C .fst) (D .fst)
   weaken .snd .fst .vertexᴰ = D.𝟙