diff --git a/LeanCondensed/Projects/InternallyProjective.lean b/LeanCondensed/Projects/InternallyProjective.lean
index b01c86e..6eac5b7 100644
--- a/LeanCondensed/Projects/InternallyProjective.lean
+++ b/LeanCondensed/Projects/InternallyProjective.lean
@@ -40,30 +40,14 @@ section MonoidalClosed
 
 variable (R : Type u) [CommRing R] -- might need some more assumptions
 
-/- This should be done in much greater generality for sheaf categories, or even reflective
-subcategories satisfying some extra properties. -/
-instance : MonoidalCategory (LightCondMod.{u} R) where
-  tensorObj A B := (presheafToSheaf _ _).obj (A.val ⊗ B.val)
-  tensorHom α β := (presheafToSheaf _ _).map (α.val ⊗ β.val)
-  whiskerLeft A _ _ β := (presheafToSheaf _ _).map (A.val ◁ β.val)
-  whiskerRight α B := (presheafToSheaf _ _).map (α.val ▷ B.val)
-  tensorUnit := (presheafToSheaf _ _).obj tensorUnit
-  associator X Y Z := sorry
-  leftUnitor := sorry
-  rightUnitor := sorry
-  tensorHom_def := sorry
-  tensor_id := sorry
-  tensor_comp := sorry
-  whiskerLeft_id := sorry
-  id_whiskerRight := sorry
-  associator_naturality := sorry
-  leftUnitor_naturality := sorry
-  rightUnitor_naturality := sorry
-  pentagon := sorry
-  triangle := sorry
-
-/- This should be done in much greater generality for sheaf categories, or even reflective
-subcategories satisfying some extra properties. -/
+/- This is the monoidal structure on localized categories. -/
+instance : MonoidalCategory (LightCondMod.{u} R) := sorry
+
+instance : MonoidalPreadditive (LightCondMod.{u} R) := sorry
+
+instance : SymmetricCategory (LightCondMod.{u} R) := sorry
+
+/- Constructed using Day's reflection theorem. -/
 instance : MonoidalClosed (LightCondMod.{u} R) := sorry
 
 variable (A : LightCondMod R) (S : LightProfinite)
@@ -84,9 +68,11 @@ def tensorFreeIso' (S T : LightProfinite) :
       (free R).obj (S ⨯ T).toCondensed := tensorFreeIso R S.toCondensed T.toCondensed ≪≫
         (free R).mapIso (Limits.PreservesLimitPair.iso lightProfiniteToLightCondSet _ _).symm
 
+instance (A : LightCondMod R) : PreservesColimits (tensorRight A) := sorry
+
 def tensorCokerIso {A B C : LightCondMod R} (f : A ⟶ B) : cokernel f ⊗ C ≅ cokernel (f ▷ C) :=
-  sorry
--- In general the tensor product commutes with colimits
+  preservesColimitIso (tensorRight C) _ ≪≫
+    HasColimit.isoOfNatIso (parallelPair.ext (Iso.refl _) (Iso.refl _) rfl (by simp))
 
 end MonoidalClosed
 
diff --git a/LeanCondensed/Projects/LightSolid.lean b/LeanCondensed/Projects/LightSolid.lean
index 1690d36..efed25f 100644
--- a/LeanCondensed/Projects/LightSolid.lean
+++ b/LeanCondensed/Projects/LightSolid.lean
@@ -97,28 +97,8 @@ instance : (solidToCondensed R).IsRightAdjoint := (solidificationAdjunction R).i
 
 open MonoidalCategory
 
--- This should be constructed using the same general machinery we need to develop to
--- construct the monoidal structure on `LightCondMod R`.
-instance : MonoidalCategory (Solid R) where
-  tensorObj A B := (A.1 ⊗ B.1).solidify
-  tensorHom α β := (solidification R).map (α ⊗ β)
-  whiskerLeft A _ _ β := (solidification R).map (A.1 ◁ β)
-  whiskerRight α B := sorry
-    -- why doesn't `(solidification R).map (α ▷ B.1)` work like `whiskerLeft` here?
-  tensorUnit := (solidification R).obj tensorUnit
-  associator := sorry
-  leftUnitor := sorry
-  rightUnitor := sorry
-  tensorHom_def := sorry
-  tensor_id := sorry
-  tensor_comp := sorry
-  whiskerLeft_id := sorry
-  id_whiskerRight := sorry
-  associator_naturality := sorry
-  leftUnitor_naturality := sorry
-  rightUnitor_naturality := sorry
-  pentagon := sorry
-  triangle := sorry
+/- This is the monoidal structure on localized categories -/
+instance : MonoidalCategory (Solid R) := sorry
 
 instance : HasLimitsOfSize.{u, 0} Type := inferInstance