diff --git a/LeanCondensed/Mathlib/CategoryTheory/Countable.lean b/LeanCondensed/Mathlib/CategoryTheory/Countable.lean
new file mode 100644
index 0000000..0fe12f6
--- /dev/null
+++ b/LeanCondensed/Mathlib/CategoryTheory/Countable.lean
@@ -0,0 +1,13 @@
+import Mathlib.CategoryTheory.Countable
+
+universe u
+
+noncomputable section
+
+open CategoryTheory Quiver Countable
+
+instance {J : Type u} [ctble : Countable J] [Category J] [thin : Quiver.IsThin J]: CountableCategory J :=
+  CountableCategory.mk ctble (fun _ _ ↦ ⟨fun _ ↦ 0, fun _ _ _ ↦ (thin _ _).elim _ _⟩)
+
+noncomputable instance {J : Type u} [fin : Finite J] [Category J] [thin : Quiver.IsThin J] : FinCategory J := by
+  apply FinCategory.mk (Fintype.ofFinite J) (fun j j' ↦ Fintype.ofFinite (j ⟶ j'))
diff --git a/LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean b/LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean
new file mode 100644
index 0000000..3ca04a5
--- /dev/null
+++ b/LeanCondensed/Mathlib/CategoryTheory/Functor/EpiMono.lean
@@ -0,0 +1,27 @@
+import Mathlib
+
+open CategoryTheory
+
+variable {C : Type*} [Category C] {D : Type*} [Category D] {F G : C ⥤ D}
+
+lemma epi_of_Retract {f g : Arrow C} (π : f ⟶ g) [Epi f.hom] [Epi π.right] : Epi g.hom :=
+  have : Epi (π.left ≫ g.hom) := by
+    rw [←Functor.id_map π.left, π.w, Functor.id_map]
+    exact epi_comp f.hom π.right
+  epi_of_epi (π.left) _
+
+lemma preservesEpi_of_Epi (f : F ⟶ G) (hf : ∀ X, Epi (f.app X)) (preserves : F.PreservesEpimorphisms)
+  : G.PreservesEpimorphisms where
+    preserves {X Y} π hπ :=
+      have : Epi (f.app X ≫ G.map π) := by
+        rw [←f.naturality π]
+        exact epi_comp (F.map π) (f.app Y)
+      epi_of_epi (f.app X) (G.map π)
+
+lemma preservesEpi_ofRetract (r : Retract G F) (preserves : F.PreservesEpimorphisms)
+  : G.PreservesEpimorphisms where
+    preserves := (
+      preservesEpi_of_Epi _
+        (fun _ ↦ (SplitEpi.mk (r.i.app _) (by rw [←NatTrans.comp_app, r.retract, NatTrans.id_app])).epi)
+        preserves
+    ).preserves
diff --git a/LeanCondensed/Projects/Epi.lean b/LeanCondensed/Projects/Epi.lean
new file mode 100644
index 0000000..f6624ae
--- /dev/null
+++ b/LeanCondensed/Projects/Epi.lean
@@ -0,0 +1,161 @@
+import Mathlib
+
+import LeanCondensed.Mathlib.CategoryTheory.Countable
+
+open Function CategoryTheory Limits Opposite
+
+universe u
+
+lemma surj_pullback' {X Y Z : LightProfinite.{u}} (f : X ⟶ Z) {g : Y ⟶ Z}
+    (hf : Function.Surjective f) : Function.Surjective ↑(pullback.snd f g) := by
+  intro y
+
+  let point : LightProfinite.{u} := LightProfinite.of PUnit
+  let point_map : point ⟶ Y := TopCat.ofHom ⟨fun _ ↦ y, continuous_const⟩
+
+  rcases hf (g y) with ⟨z, hz⟩
+
+  let point_map' : point ⟶ X := TopCat.ofHom ⟨fun _ ↦ z, continuous_const⟩
+
+  use pullback.lift point_map' point_map (by ext; erw [hz]; rfl) PUnit.unit
+
+  rw [←ConcreteCategory.comp_apply, pullback.lift_snd]
+  rfl
+
+instance surj_widePullback {J : Type*} (B : LightProfinite.{u}) (objs : J → LightProfinite)
+  (arrows: (j : J) → (objs j ⟶ B)) (hepi : ∀ j, Epi (arrows j)) [HasWidePullback B objs arrows]
+    : ∀ j, Epi (WidePullback.π arrows j) := by
+  classical
+  intro i
+  simp [LightProfinite.epi_iff_surjective] at ⊢ hepi
+  intro xi
+  let point : LightProfinite.{u} := LightProfinite.of PUnit
+  let base_pt : B := arrows i xi
+  have choice : ∀ j, ∃ xj, arrows j xj = base_pt := fun j ↦ hepi j base_pt
+  let point_maps : (j : J) → (point ⟶ objs j) := (fun j ↦
+    if h : i = j then
+      CompHausLike.ofHom _ (ContinuousMap.const point (h ▸ xi))
+    else
+      (CompHausLike.ofHom _ (ContinuousMap.const point (choice j).choose))
+  )
+  let lift : point ⟶ widePullback B objs arrows :=
+    WidePullback.lift (CompHausLike.ofHom _ (ContinuousMap.const point base_pt)) point_maps
+    (
+      by
+        intro j
+        unfold point_maps
+        by_cases h : i = j
+        · rw [dif_pos h]
+          subst h
+          rfl
+        · rw [dif_neg h]
+          ext x
+          simp only [ConcreteCategory.comp_apply, CompHausLike.hom_ofHom, ContinuousMap.const_apply]
+          exact (choice j).choose_spec
+    )
+  use lift PUnit.unit
+  rw [←ConcreteCategory.comp_apply, WidePullback.lift_π]
+  simp [point_maps]
+
+
+
+
+instance : lightProfiniteToLightCondSet.PreservesEpimorphisms := {
+  preserves f hf := (LightCondSet.epi_iff_locallySurjective_on_lightProfinite _).mpr
+    fun _ g ↦
+      ⟨
+        pullback f g,
+        pullback.snd _ _,
+        surj_pullback' f ((LightProfinite.epi_iff_surjective f).mp hf),
+        pullback.fst _ _,
+        pullback.condition
+      ⟩
+}
+
+lemma stupid {A : Type u} {s : Set A} {x y : A} {px : x ∈ s} {py : y ∈ s} (h : (⟨x, px⟩ : s) = ⟨y, py⟩) : x = y
+  := by
+    rwa [Subtype.ext_iff] at h
+
+noncomputable def πpair {X Y : LightProfinite} (π : X ⟶ Y) : WalkingParallelPair ⥤ LightCondSet :=
+  parallelPair
+    (lightProfiniteToLightCondSet.map <| pullback.fst π π)
+    (lightProfiniteToLightCondSet.map <| pullback.snd π π)
+
+noncomputable def regular {X Y : LightProfinite} (π : X ⟶ Y)
+    : Cofork (lightProfiniteToLightCondSet.map <| pullback.fst π π) (lightProfiniteToLightCondSet.map <| pullback.snd π π) := Cofork.ofπ (lightProfiniteToLightCondSet.map <| π) (by
+  rw [
+    ←lightProfiniteToLightCondSet.map_comp,
+    ←lightProfiniteToLightCondSet.map_comp,
+    pullback.condition
+  ])
+
+def cfork {X Y : LightProfinite} (π : X ⟶ Y)
+  := Cofork (lightProfiniteToLightCondSet.map (pullback.fst π π)) (lightProfiniteToLightCondSet.map (pullback.snd π π))
+
+noncomputable def regularLiftElem {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π]
+      (cone : cfork π) : cone.pt.val.obj (op Y)
+    :=
+  let fX := yonedaEquiv cone.π.val
+  have : cone.pt.val.map (pullback.fst π π).op fX = cone.pt.val.map (pullback.snd π π).op fX := by
+    have this : (lightProfiniteToLightCondSet.map (pullback.fst π π) ≫ cone.π).val = (yoneda.map (pullback.fst π π) ≫ cone.π.val) := rfl
+    have this' : (lightProfiniteToLightCondSet.map (pullback.snd π π) ≫ cone.π).val = (yoneda.map (pullback.snd π π) ≫ cone.π.val) := rfl
+
+    erw [
+        yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.fst π π),
+        yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.snd π π),
+        ←this, ←this',
+        cone.condition,
+    ]
+  (((LightCondensed.equalizerCondition cone.pt).bijective_mapToEqualizer_pullback _ _ _ π).surjective ⟨fX, this⟩).choose
+
+private lemma cone_elem {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+    : cone.pt.val.map (pullback.fst π π).op (yonedaEquiv cone.π.val) = cone.pt.val.map (pullback.snd π π).op (yonedaEquiv cone.π.val) := by
+  have this : (lightProfiniteToLightCondSet.map (pullback.fst π π) ≫ cone.π).val = (yoneda.map (pullback.fst π π) ≫ cone.π.val) := rfl
+  have this' : (lightProfiniteToLightCondSet.map (pullback.snd π π) ≫ cone.π).val = (yoneda.map (pullback.snd π π) ≫ cone.π.val) := rfl
+  erw [
+      yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.fst π π),
+      yonedaEquiv_naturality (F := cone.pt.val) cone.π.val (pullback.snd π π),
+      ←this, ←this',
+      cone.condition,
+  ]
+
+noncomputable def regularLift {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π) : lightProfiniteToLightCondSet.obj Y ⟶ cone.pt
+  := ⟨ yonedaEquiv.symm (regularLiftElem π cone) ⟩
+
+private lemma regularLift_prop {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+    : regularTopology.MapToEqualizer cone.pt.val π (pullback.fst π π) (pullback.snd π π) pullback.condition (regularLiftElem π cone) = ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩
+  := (((LightCondensed.equalizerCondition cone.pt).bijective_mapToEqualizer_pullback _ _ _ π).surjective ⟨yonedaEquiv cone.π.val, cone_elem π cone⟩).choose_spec
+
+lemma regularLift_comp {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+    : (regular π).π ≫ regularLift π cone = cone.π := by
+  refine Sheaf.Hom.ext (yonedaEquiv.injective ?_)
+  erw [←yonedaEquiv_naturality (F := cone.pt.val), Equiv.apply_symm_apply]
+  exact stupid (s := {x : cone.pt.val.obj (Opposite.op X) | cone.pt.val.map (pullback.fst π π).op x = cone.pt.val.map (pullback.snd π π).op x}) (regularLift_prop π cone)
+
+lemma regularLift_unique {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π] (cone : cfork π)
+      (m : (lightProfiniteToLightCondSet.obj Y) ⟶ cone.pt) (hm : (regular π).π ≫ m = cone.π)
+    : m = regularLift π cone := by
+  erw [Cofork.π_ofπ, ←regularLift_comp π cone] at hm
+  exact Epi.left_cancellation _ _ hm
+
+noncomputable abbrev regular_IsColimit {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π]
+    : IsColimit (regular π)
+  := Cofork.IsColimit.mk _ (regularLift π) (regularLift_comp π) (regularLift_unique π)
+
+noncomputable abbrev regular_RegularEpi {X Y : LightProfinite} (π : X ⟶ Y) [EffectiveEpi π]
+    : RegularEpi (lightProfiniteToLightCondSet.map π) where
+  W := lightProfiniteToLightCondSet.obj (pullback π π)
+  left := lightProfiniteToLightCondSet.map (pullback.fst π π)
+  right := lightProfiniteToLightCondSet.map (pullback.snd π π)
+  w := by
+    rw [
+      ←lightProfiniteToLightCondSet.map_comp,
+      ←lightProfiniteToLightCondSet.map_comp,
+      pullback.condition
+    ]
+  isColimit := regular_IsColimit π
+
+instance : lightProfiniteToLightCondSet.PreservesEffectiveEpis where
+  preserves π _ :=
+    have : RegularEpi (lightProfiniteToLightCondSet.map π) := regular_RegularEpi π
+    inferInstance
diff --git a/LeanCondensed/Projects/Initial.lean b/LeanCondensed/Projects/Initial.lean
new file mode 100644
index 0000000..095fd87
--- /dev/null
+++ b/LeanCondensed/Projects/Initial.lean
@@ -0,0 +1,28 @@
+import Mathlib
+
+open CategoryTheory Limits Condensed
+
+universe u
+
+def empty_elim {p : Sort u} {X : LightProfinite} (hX : ¬Nonempty X) (x : X) : p := (hX ⟨x⟩).elim
+
+def empty_subset {X : LightProfinite} (hX : ¬Nonempty X) (s : Set X) : s = ⊤ := by
+  ext x
+  exact empty_elim hX x
+
+def empty_map {X Y : LightProfinite} (hY : ¬Nonempty Y) (f : X ⟶ Y) : ¬Nonempty X
+  := fun h ↦ h.elim (fun x ↦ hY ⟨f x⟩)
+
+def empty_iso {X Y : LightProfinite} (hY : ¬Nonempty Y) (f : X ⟶ Y) : IsIso f := by
+  let finv : Y ⟶ X := CompHausLike.ofHom _ {
+    toFun y := empty_elim hY y
+    continuous_toFun := by
+      apply Continuous.mk
+      intro s empty_elim
+      rw [empty_subset hY ((fun y ↦ _root_.empty_elim hY y) ⁻¹' s)]
+      exact TopologicalSpace.isOpen_univ
+  }
+  refine IsIso.mk ⟨finv, ?_⟩
+  constructor <;> ext x
+  exact empty_elim hY (f x)
+  exact empty_elim hY x
diff --git a/LeanCondensed/Projects/InternallyProjective.lean b/LeanCondensed/Projects/InternallyProjective.lean
index 9a7167f..ccf2e84 100644
--- a/LeanCondensed/Projects/InternallyProjective.lean
+++ b/LeanCondensed/Projects/InternallyProjective.lean
@@ -5,6 +5,7 @@ Authors: Dagur Asgeirsson
 -/
 import Mathlib.Condensed.Light.Epi
 import LeanCondensed.LightCondensed.Yoneda
+import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono
 import LeanCondensed.Mathlib.Condensed.Light.Limits
 import LeanCondensed.Mathlib.Condensed.Light.Monoidal
 import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts
@@ -30,6 +31,16 @@ variable {C : Type*} [Category C] [MonoidalCategory C] [MonoidalClosed C]
 class InternallyProjective (P : C) : Prop where
   preserves_epi : (ihom P).PreservesEpimorphisms
 
+theorem ofRetract {X Y : C} (r : Retract Y X) (proj : InternallyProjective X)
+    : InternallyProjective Y :=
+  haveI : Retract (ihom Y) (ihom X) := {
+    i := MonoidalClosed.pre r.r
+    r := MonoidalClosed.pre r.i
+    retract := by
+      rw [←MonoidalClosed.pre_map, r.retract, MonoidalClosed.pre_id]
+  }
+  InternallyProjective.mk <| preservesEpi_ofRetract this proj.preserves_epi
+
 end InternallyProjective
 
 open CategoryTheory LightProfinite OnePoint Limits LightCondensed MonoidalCategory MonoidalClosed
@@ -48,6 +59,9 @@ def ihomPoints (A B : LightCondMod.{u} R) (S : LightProfinite) :
 -- We have an `R`-module structure on `M ⟶ N` for condensed `R`-modules `M`, `N`,
 -- and this could be made an `≅`. But it's not needed in this proof.
 
+
+lemma tensorLeft_obj (X Y : LightCondMod.{u} R) : (tensorLeft X).obj Y = X ⊗ Y := rfl
+
 lemma ihom_map_val_app (A B P : LightCondMod.{u} R) (S : LightProfinite) (e : A ⟶ B) :
     ∀ x, ConcreteCategory.hom (((ihom P).map e).val.app ⟨S⟩) x =
         (ihomPoints R P B S).symm (ihomPoints R P A S x ≫ e) := by
diff --git a/LeanCondensed/Projects/LightSolid.lean b/LeanCondensed/Projects/LightSolid.lean
index a05da03..48503ac 100644
--- a/LeanCondensed/Projects/LightSolid.lean
+++ b/LeanCondensed/Projects/LightSolid.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
 import LeanCondensed.Projects.InternallyProjective
+import LeanCondensed.Projects.Proj
+import LeanCondensed.Projects.Sequence
 /-!
 
 # Project: light solid abelian groups
@@ -47,7 +49,7 @@ def shift : ℕ∪{∞} ⟶ ℕ∪{∞} := TopCat.ofHom {
     intro U h hU
     simp only [isOpen_iff_of_mem h, isClosed_discrete, isCompact_iff_finite, true_and] at hU
     refine ⟨sSup (Option.some ⁻¹' U)ᶜ + 1, fun n hn ↦ by
-      simpa using not_mem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩ }
+      simpa using notMem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩ }
 
 end LightProfinite
 
@@ -56,20 +58,10 @@ namespace LightCondensed
 variable (R : Type _) [CommRing R]
 -- might need some more assumptions eventually, finite type over `ℤ`?
 
-def P_map :
-    (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed :=
-  (lightProfiniteToLightCondSet ⋙ free R).map (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩)
+instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) :=
+  internallyProjective_ℕinfty _
 
-def P : LightCondMod R := cokernel (P_map R)
-
-def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _
-
-def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A)
-    (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf
-
-instance : InternallyProjective (P R) := sorry
-
-instance : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := sorry
+instance : InternallyProjective (P R) := ofRetract (P_retract _) inferInstance
 
 variable (R : Type) [CommRing R]
 
@@ -82,7 +74,9 @@ def oneMinusShift' : (free R).obj (ℕ∪{∞}).toCondensed ⟶ (free R).obj (
 
 def oneMinusShift : P R ⟶ P R := by
   refine P_homMk R _ (oneMinusShift' R) ?_ ≫ P_proj R
-  sorry
+  erw [Preadditive.comp_sub, Category.comp_id]
+  simp only [sub_eq_zero, P_map, ←Functor.map_comp]
+  rfl
 
 variable {R : Type} [CommRing R]
 
diff --git a/LeanCondensed/Projects/LocalizedMonoidal.lean b/LeanCondensed/Projects/LocalizedMonoidal.lean
index 9c9e13b..d35603c 100644
--- a/LeanCondensed/Projects/LocalizedMonoidal.lean
+++ b/LeanCondensed/Projects/LocalizedMonoidal.lean
@@ -93,7 +93,7 @@ def coreMonoidalTransport {F G : C ⥤ D} [F.Monoidal] (i : F ≅ G) : G.CoreMon
     simp only [tensor_whiskerLeft, Functor.LaxMonoidal.associativity, Category.assoc,
       Iso.inv_hom_id_assoc]
     rw [← tensorHom_id, associator_naturality_assoc]
-    simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp, ← tensor_comp_assoc]
+    simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp_assoc]
   left_unitality X := by
     simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom,
       μIso_hom, Category.assoc, ← tensor_comp_assoc, Iso.hom_inv_id_app, Category.comp_id,
diff --git a/LeanCondensed/Projects/PreservesCoprod.lean b/LeanCondensed/Projects/PreservesCoprod.lean
new file mode 100644
index 0000000..f1a85ba
--- /dev/null
+++ b/LeanCondensed/Projects/PreservesCoprod.lean
@@ -0,0 +1,122 @@
+import Mathlib
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
+import LeanCondensed.LightCondensed.Yoneda
+
+open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed
+  MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom
+  Topology Function
+
+universe u
+
+attribute [local instance] Types.instFunLike Types.instConcreteCategory
+
+instance {n : ℕ} (S : Fin n → LightProfinite.{u}) :
+    PreservesColimit (Discrete.functor S) lightProfiniteToLightCondSet.{u} := by
+  have : HasColimitsOfSize.{u} (LightCondSet.{u}) :=
+    inferInstanceAs (HasColimitsOfSize.{u} (Sheaf _ _))
+  apply (config := { allowSynthFailures := true}) PreservesCoproduct.of_iso_comparison
+  rw [isIso_iff_isIso_coyoneda_map]
+  intro X
+  rw [isIso_iff_bijective]
+  have := instIsIsoPiComparison X.val (fun i ↦ ⟨S i⟩)
+
+  let map : ((∐ S).toCondensed ⟶ X) → ((∐ fun i ↦ (S i).toCondensed) ⟶ X) :=
+    (inv (piComparison (yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩))
+      ≫ (CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv)
+      ∘ (Types.productIso (fun i ↦ (S i).toCondensed ⟶ X)).inv
+      ∘ (Pi.map (fun i ↦ (LightCondensed.yoneda (S i) X).symm))
+      ∘ (
+          (X.val.mapIso (opCoproductIsoProduct S)).hom
+            ≫ (piComparison X.val (fun i ↦ ⟨S i⟩))
+            ≫ (Types.productIso (fun i ↦ X.val.obj (op (S i)))).hom
+        )
+      ∘ (LightCondensed.yoneda (∐ S) X)
+
+  have map_bij : Bijective map := by
+    refine Bijective.comp ?_
+      (
+        Bijective.comp ?_
+          (Bijective.comp ?_ (Bijective.comp ?_ ?_))
+      )
+    repeat {rw [←isIso_iff_bijective]; infer_instance}
+    exact Bijective.piMap (fun i ↦ (LightCondensed.yoneda _ _).symm.bijective)
+    rw [←isIso_iff_bijective]; infer_instance
+    exact (LightCondensed.yoneda _ _).bijective
+
+  have : Injective ((CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom
+      ≫ (piComparison (yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩))) := by
+    apply Bijective.injective
+    rw [←isIso_iff_bijective]
+    infer_instance
+
+  suffices ((coyoneda.map (sigmaComparison lightProfiniteToLightCondSet S).op).app X) = map by
+    rw [this]
+    exact map_bij
+
+  apply this.comp_left
+  simp only [mapIso_hom, map]
+  rw [
+      ←Function.comp_assoc,
+  ]
+  erw [
+      ←coe_comp
+        (f := (CategoryTheory.inv (piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed)
+          ≫ (CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).inv))
+        (g := ((CategoryTheory.yoneda.obj X).map (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom
+          ≫ piComparison (CategoryTheory.yoneda.obj X) fun i ↦ op (S i).toCondensed)),
+  ]
+  ext1 f
+  ext1 ⟨i⟩
+  simp only [yoneda_obj_obj, Discrete.functor_obj_eq_as, coyoneda_obj_obj, Function.comp_apply,
+    coyoneda_map_app, Quiver.Hom.unop_op, types_comp_apply, yoneda_obj_map, Category.assoc,
+    Iso.map_inv_hom_id_assoc, IsIso.inv_hom_id, yoneda_apply, CategoryTheory.id_apply]
+
+  change
+    (
+      piComparison (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)
+        ≫ Pi.π (fun i ↦ (S i).toCondensed ⟶ X) i
+    )
+    (
+      (opCoproductIsoProduct fun i ↦ (S i).toCondensed).hom.unop
+        ≫ sigmaComparison lightProfiniteToLightCondSet S
+        ≫ f
+    ) =
+    (
+      (Types.productIso fun i ↦ (S i).toCondensed ⟶ X).inv
+        ≫ Pi.π (fun i ↦ (S i).toCondensed ⟶ X) i
+    ) _
+
+  erw [piComparison_comp_π (CategoryTheory.yoneda.obj X) (fun i ↦ ⟨(S i).toCondensed⟩)]
+  rw [Types.productIso_inv_comp_π]
+  simp only [Pi.map_apply, Types.productIso_hom_comp_eval_apply]
+
+  change
+    _ =
+    (LightCondensed.yoneda (S i) X).symm (
+      (
+        (X.val.map (opCoproductIsoProduct S).hom)
+          ≫ piComparison X.val (fun i ↦ ⟨S i⟩)
+          ≫ Pi.π (fun i ↦ X.val.obj ⟨S i⟩) i
+      )
+      (LightCondensed.yoneda (∐ S) X f)
+    )
+
+  rw [
+    piComparison_comp_π,
+    ←X.val.map_comp,
+    opCoproductIsoProduct_hom_comp_π,
+    yoneda_obj_map,
+    ←unop_comp_assoc,
+    opCoproductIsoProduct_hom_comp_π,
+    Quiver.Hom.unop_op,
+    ι_comp_sigmaComparison_assoc,
+    ←yoneda_symm_naturality,
+    (yoneda _ _).symm_apply_apply
+  ]
+
+instance : PreservesFiniteCoproducts lightProfiniteToLightCondSet.{u} where
+  preserves n :=
+    { preservesColimit {S} := by
+        let i : S ≅ Discrete.functor (fun i ↦ S.obj ⟨i⟩) := Discrete.natIso (fun _ ↦ Iso.refl _)
+        exact preservesColimit_of_iso_diagram lightProfiniteToLightCondSet i.symm
+    }
diff --git a/LeanCondensed/Projects/Proj.lean b/LeanCondensed/Projects/Proj.lean
new file mode 100644
index 0000000..d42e8e1
--- /dev/null
+++ b/LeanCondensed/Projects/Proj.lean
@@ -0,0 +1,551 @@
+import LeanCondensed.Projects.Epi
+import LeanCondensed.Projects.LightProfiniteInjective
+import LeanCondensed.Projects.Initial
+import LeanCondensed.Projects.InternallyProjective
+import LeanCondensed.Projects.PreservesCoprod
+import LeanCondensed.Mathlib.CategoryTheory.Countable
+import LeanCondensed.Mathlib.Topology.Category.LightProfinite.ChosenFiniteProducts
+import LeanCondensed.Projects.Pullbacks
+import Mathlib
+
+open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed
+  MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom
+  CartesianMonoidalCategory Topology
+
+universe u
+
+variable (R : Type) [CommRing R]
+
+instance : TotallyDisconnectedSpace PUnit := by
+  have := TotallySeparatedSpace.of_discrete
+  apply TotallySeparatedSpace.totallyDisconnectedSpace
+
+@[simps!]
+def CategoryTheory.Limits.parallelPair.hom {C : Type*} [Category C]
+    {F G : WalkingParallelPair ⥤ C} (zero : F.obj zero ⟶ G.obj zero)
+    (one : F.obj one ⟶ G.obj one) (left : F.map left ≫ one = zero ≫ G.map left)
+    (right : F.map right ≫ one = zero ≫ G.map right) : F ⟶ G := {
+      app := (by
+      rintro ⟨j⟩
+      exacts [zero, one])
+      naturality := (by rintro _ _ ⟨_⟩ <;> simp [left, right])
+    }
+
+lemma isClosed_fibres {T : LightProfinite} (f : T ⟶ ℕ∪{∞}) (s : ℕ → Set T)
+  (hs : ∀ n (x : s n), f x = n) (hs' : ∀ n, IsClosed (s n)) : IsClosed ({t | f t = ∞} ∪ ⋃ n, s n) := by
+  apply IsClosed.mk
+  let fibre : ℕ → Set T := fun n ↦ f ⁻¹' {OnePoint.some n}
+  have clopen : ∀ n, IsClopen (fibre n) := by
+    intro n
+    refine IsClopen.preimage ⟨isClosed_singleton, ?_⟩ f.1.continuous
+    exact ⟨fun h ↦ by simp at h, trivial⟩
+
+  suffices ({t | f t = ∞} ∪ ⋃ n, s n)ᶜ = ⋃ n, (s n)ᶜ ∩ fibre n by
+    rw [this]
+    exact isOpen_iUnion (fun i ↦ IsOpen.inter (hs' i).1 (clopen i).2)
+
+  ext x
+  simp only [Set.compl_union, Set.compl_iUnion, Set.mem_inter_iff, Set.mem_compl_iff,
+    Set.mem_setOf_eq, Set.mem_iInter, Set.mem_iUnion]
+  constructor
+  · intro ⟨h, h'⟩
+    obtain ⟨n', hn⟩ := Option.ne_none_iff_exists'.mp h
+    exact ⟨n', h' n', hn⟩
+  · intro ⟨n, hn, hn'⟩
+    refine ⟨?_, ?_⟩
+    · rw [hn']
+      exact OnePoint.coe_ne_infty _
+    intro i
+    by_cases h : i = n
+    exact h ▸ hn
+    intro h'
+    have := hs i ⟨x, h'⟩
+    apply h
+    rw [hn', OnePoint.coe_eq_coe,] at this
+    exact Eq.symm this
+
+
+set_option maxHeartbeats 500000
+noncomputable def smart_cover {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) : coprod T (explicitPullback (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)) ⟶ explicitPullback π π :=
+  coprod.desc
+    (explicitPullback.diagonal π : T ⟶ explicitPullback π π)
+    (
+        explicitPullback.map
+        (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
+        π π
+        (fibre_incl ∞ (π ≫ snd S ℕ∪{∞})) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞})) (𝟙 _)
+            (by rw [Category.comp_id]) (by rw [Category.comp_id])
+        : explicitPullback (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (fibre_incl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ⟶ explicitPullback π π
+    )
+
+lemma subspaceCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [hepi : Epi π]
+  {σ' : ℕ∪{∞} → (S ⟶ T)} (hσ : ∀ n, σ' n ≫ π ≫ fst _ _ = 𝟙 _)
+  (hσ' : ∀ n s, (σ' n ≫ π ≫ snd S ℕ∪{∞}) s = ↑n)
+    : ∃ (T' : LightProfinite) (i : T' ⟶ T),
+      Epi (i ≫ π) ∧ Epi (smart_cover (i ≫ π))
+        ∧ IsSplitEpi
+          (fibre_incl ∞ ((i ≫ π) ≫ snd _ _) ≫ i ≫ π ≫ fst S ℕ∪{∞}) := by
+
+  let space : Set T :=
+    Set.iUnion (fun (n : ℕ) ↦ Set.range (σ' (OnePoint.some n))) ∪ {t : T | (π ≫ snd _ _) t = ∞}
+  have : IsClosed space := by
+    unfold space
+    rw [Set.union_comm]
+    exact isClosed_fibres _ _
+      (fun n ⟨x, ⟨s, hs⟩⟩ ↦ by simp only [←hs, ←ConcreteCategory.comp_apply, hσ' _ _])
+      (fun n ↦ IsCompact.isClosed (isCompact_range (σ' n).1.continuous))
+
+  let T' : LightProfinite := ⟨TopCat.of space, inferInstance, inferInstance⟩
+
+  let i : T' ⟶ T :=
+    CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩
+
+  have : Mono i := by
+    rw [CompHausLike.mono_iff_injective]
+    exact Subtype.val_injective
+
+  let σ : ℕ∪{∞} → (S ⟶ T') := fun n ↦ (CompHausLike.ofHom _
+    ⟨
+      fun s ↦ ⟨σ' n s,
+        by
+          rcases n with (n | n)
+          · exact Or.inr (hσ' ∞ s)
+          · apply Or.inl
+            rw [Set.mem_iUnion]
+            exact ⟨n, s, rfl⟩
+      ⟩,
+      by continuity
+    ⟩)
+
+  have hσ'' : ∀ (n : ℕ∪{∞}) (t : T'), t ∈ Set.range (σ n) → (i ≫ π ≫ fst _ _ ≫ σ n) t = t := by
+    intro n t ht
+    obtain ⟨s, hs⟩ := ht
+    rw (config := { occs := .pos [1]}) [←hs]
+    rw [
+        ←ConcreteCategory.comp_apply,
+        ←Category.assoc π,
+        ←Category.assoc i,
+        ←Category.assoc (σ n),
+    ]
+    erw [hσ]
+    rw [Category.id_comp, hs]
+
+  have coe_i : ∀ (t : T'), ↑t = i t := fun _ ↦ rfl
+  have σ_i : ∀ n, σ' n = σ n ≫ i := fun _ ↦ rfl
+
+  have hT' : ∀ (n : ℕ) t, t ∈ Set.range (σ n) ↔ (i ≫ π ≫ snd _ _) t = n := by
+    intro n t'
+    constructor <;> intro h
+    · obtain ⟨_, ht⟩ := h
+      rw [←ht, ←ConcreteCategory.comp_apply]
+      erw [hσ']
+    · rcases t'.2 with (fin | inf)
+      · rw [Set.mem_iUnion] at fin
+        obtain ⟨j, ⟨s, hs⟩⟩ := fin
+        suffices h' : j = n by
+          rw [h'] at hs
+          use s
+          exact Subtype.ext hs
+        rw [coe_i] at hs
+        rw [ConcreteCategory.comp_apply, ←hs, ←ConcreteCategory.comp_apply, hσ'] at h
+        rw [←OnePoint.coe_eq_coe]
+        exact h
+      · simp only [Set.mem_setOf_eq] at inf
+        erw [inf] at h
+        exact (Option.some_ne_none n (Eq.symm h)).elim
+
+  refine ⟨T', i, ?_, ?_, ?_⟩
+  · rw [LightProfinite.epi_iff_surjective]
+    rintro ⟨s, (n | n)⟩
+    obtain ⟨t, ht⟩ := (LightProfinite.epi_iff_surjective π).mp hepi ⟨s, none⟩
+    have : t ∈ space := by apply Or.inr; rw [Set.mem_setOf_eq, ConcreteCategory.comp_apply, ht]; rfl
+    use ⟨t, this⟩
+    rw [←ht]
+    rfl
+    · use σ n s
+      apply Prod.ext
+      change ConcreteCategory.hom (σ' n ≫ π ≫ fst _ _) s = s
+      rw [hσ]; rfl
+      change ConcreteCategory.hom (σ' n ≫ π ≫ snd _ _) s = (OnePoint.some n)
+      rw [hσ']
+  · rw [LightProfinite.epi_iff_surjective]
+    intro ⟨⟨t,t'⟩, ht⟩
+    by_cases h : (i ≫ π ≫ snd _ _) t = ∞
+    · have : (i ≫ π ≫ snd _ _) t' = ∞ := by
+        rw [←Category.assoc, ConcreteCategory.comp_apply, ←ht,
+          ←ConcreteCategory.comp_apply, Category.assoc, h
+        ]
+      let x : explicitPullback (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π)
+        (fibre_incl ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) ≫ i ≫ π) :=
+        ⟨⟨⟨t, h⟩, ⟨t', this⟩⟩,
+        by
+          simp only [Set.mem_setOf_eq]
+          rw [ConcreteCategory.comp_apply (fibre_incl _ _), ConcreteCategory.comp_apply (fibre_incl _ _)]
+          unfold fibre_incl
+          simp only [CompHausLike.hom_ofHom, ContinuousMap.coe_mk]
+          exact ht
+      ⟩
+      let p := coprod.inr (X := T') (Y := (explicitPullback _ _)) x
+      use coprod.inr (X := T') (Y := (explicitPullback _ _)) x
+      rw [smart_cover, ←ConcreteCategory.comp_apply]
+      simp only [coprod.inr_desc]
+      rfl
+    · rw [←ne_eq, OnePoint.ne_infty_iff_exists] at h
+      obtain ⟨n, hn⟩ := h
+      symm at hn
+      use coprod.inl (X := T') (Y := (explicitPullback _ _)) ((i ≫ π ≫ fst _ _ ≫ σ n) t)
+      simp only [smart_cover, ←ConcreteCategory.comp_apply, Category.assoc, coprod.inl_desc]
+      rw [
+        ←Category.assoc (fst _ _), ←Category.assoc π,  ←Category.assoc i,
+        ConcreteCategory.comp_apply
+      ]
+      rw [hσ'']
+      · apply Subtype.ext
+        apply Prod.ext (by rfl)
+        change t = t'
+        have hn' : (ConcreteCategory.hom (i ≫ π ≫ snd S ℕ∪{∞})) t' = n := by
+          rw [←hn]
+          rw [
+            ←Category.assoc,
+            ConcreteCategory.comp_apply, ConcreteCategory.comp_apply (i ≫ π),
+            ht
+          ]
+        rw [←hT'] at hn hn'
+        obtain ⟨s, hs⟩ := hn
+        obtain ⟨s', hs'⟩ := hn'
+        rw [←hs, ←hs']
+        apply congr_arg
+        rw [←ConcreteCategory.id_apply s, ←ConcreteCategory.id_apply s']
+        erw [←hσ n, σ_i]
+        simp only [Category.assoc]
+        erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply (σ n),
+          hs, hs'
+        ]
+        erw [←Category.assoc, ConcreteCategory.comp_apply,
+          ConcreteCategory.comp_apply (i ≫ π), ht]
+        rfl
+      · exact (hT' _ _).mpr hn
+  · have : σ ∞ ≫ i = σ' ∞ := rfl
+
+    let σσ : S ⟶ fibre ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) :=
+      fibreLift ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞)
+
+    exact ⟨⟨
+        σσ,
+        by
+          simp only [←Category.assoc]
+          rw [
+            fibreLift_comp ∞ ((i ≫ π) ≫ snd S ℕ∪{∞}) (σ ∞) (by exact hσ' ∞),
+          ]
+          erw [hσ]
+    ⟩⟩
+
+lemma refinedCover { S T : LightProfinite } (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π]
+    : ∃ (S' T' : LightProfinite) (y' : S' ⟶ S) (π' : T' ⟶ S' ⊗ ℕ∪{∞}) (g' : T' ⟶ T),
+      Epi π'
+        ∧ Epi y'
+        ∧ π' ≫ MonoidalCategoryStruct.tensorHom y' (𝟙 _) = g' ≫ π
+        ∧ IsSplitEpi (fibre_incl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
+        ∧ Epi (
+          smart_cover π'
+        )
+    := by
+  have : Countable (WidePullbackShape ↑ℕ∪{∞}.toTop) := by
+    have : Countable ℕ∪{∞} := Option.instCountable
+    apply Option.instCountable
+  let S' := widePullback S (fun (n : ℕ∪{∞}) ↦ fibre n (π ≫ snd _ _))
+    (fun n ↦ fibre_incl n (π ≫ snd _ _) ≫ π ≫ fst _ _)
+  let y' : S' ⟶ S := WidePullback.base (fun n ↦ fibre_incl n (π ≫ snd _ _) ≫ π ≫ fst _ _)
+
+
+  let Ttilde := explicitPullback π (MonoidalCategoryStruct.tensorHom y' (𝟙 ℕ∪{∞}))
+  let π_tilde : Ttilde ⟶ S' ⊗ ℕ∪{∞} := explicitPullback.snd _ _
+
+  let σ' : ℕ∪{∞} → (S' ⟶ Ttilde) := fun n ↦
+    PullbackCone.IsLimit.lift explicitPullback.IsLimit
+      ((WidePullback.π _ n) ≫ fibre_incl n (π ≫ snd _ _))
+      (lift (𝟙 S') (CompHausLike.ofHom _ <| ContinuousMap.const S' n))
+      (
+        by
+          simp only [Category.assoc, limit.cone_x]
+          apply CartesianMonoidalCategory.hom_ext
+          · simp [y']
+          · ext
+            simp only [Category.assoc, fibre_condition, tensorHom_id, lift_whiskerRight,
+              Category.id_comp, lift_snd, CompHausLike.hom_ofHom, ContinuousMap.const_apply]
+            rfl
+      )
+  have hσ : ∀ n, σ' n ≫ π_tilde ≫ fst _ _ = 𝟙 _ := by
+    intro n
+    simp only [←Category.assoc, σ']
+    erw [PullbackCone.IsLimit.lift_snd]
+    exact lift_fst _ _
+  have hσ' : ∀ n s, (σ' n ≫ π_tilde ≫ snd S' ℕ∪{∞}) s = n := by
+    intro n s
+    simp only [←Category.assoc, σ']
+    erw [PullbackCone.IsLimit.lift_snd]
+    simp
+
+  obtain ⟨T', i, _, _, split⟩ := subspaceCover π_tilde hσ hσ'
+
+  refine ⟨
+    S', T', y',
+    i ≫ π_tilde,
+    i ≫ explicitPullback.fst _ _,
+    inferInstance,
+    ?_,
+    ?_,
+    split,
+    inferInstance
+  ⟩
+  unfold y'
+  · rw [←WidePullback.π_arrow _ (OnePoint.some 0)]
+    have : ∀ j, Epi (fibre_incl j (π ≫ snd S ℕ∪{∞}) ≫ π ≫ fst S ℕ∪{∞}) := by
+      simp_rw [LightProfinite.epi_iff_surjective]
+      intro j s
+      have epi : Epi π := inferInstance
+      rw [LightProfinite.epi_iff_surjective] at epi
+      obtain ⟨t, ht⟩ := epi ⟨s, j⟩
+      use ⟨
+        t,
+        by
+          simp only [Set.mem_preimage, ConcreteCategory.comp_apply, ht,
+            Set.mem_singleton_iff]
+          rfl
+      ⟩
+      rw [ConcreteCategory.comp_apply]
+      change (ConcreteCategory.hom (π ≫ fst S ℕ∪{∞})) t = s
+      rw [ConcreteCategory.comp_apply, ht]
+      rfl
+    have := surj_widePullback S (fun (n : ℕ∪{∞}) ↦ fibre n (π ≫ snd _ _))
+      (fun n ↦ fibre_incl n (π ≫ snd _ _) ≫ π ≫ fst _ _) this
+    apply epi_comp
+  simp only [π_tilde, Category.assoc,explicitPullback.condition]
+
+section
+
+variable {X Y : LightProfinite} (y : Y) (f : X ⟶ Y)
+
+instance (S : Set Y) [IsClosed S] : IsClosed (f ⁻¹' S) := by
+  exact IsClosed.preimage f.1.continuous inferInstance
+
+instance : IsClosed (f ⁻¹' {y}) :=
+  inferInstance
+
+instance (S : Set X) [IsClosed S] : CompactSpace S := by
+  exact isCompact_iff_compactSpace.mp (IsClosed.isCompact inferInstance)
+
+instance : CompactSpace (f ⁻¹' {y}) := inferInstance
+end
+
+
+lemma prod_epi (X Y : LightProfinite.{u}) [hempty : Nonempty X] : Epi (snd X Y) := by
+  rw [LightProfinite.epi_iff_surjective]
+  exact fun y ↦ ⟨⟨Classical.choice hempty, y⟩, rfl⟩
+
+private lemma comm_sq {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite}
+  (f : (free R).obj (S).toCondensed ⟶ Y)
+    : ∃ (T : LightProfinite) (π : T ⟶ S) (g : ((free R).obj T.toCondensed) ⟶ X), Epi π
+      ∧ g ≫ p = (lightProfiniteToLightCondSet ⋙ (free R)).map π ≫ f := by
+  have : Epi ((LightCondensed.forget _).map p) := inferInstance
+  rw [LightCondSet.epi_iff_locallySurjective_on_lightProfinite] at this
+
+  let y : Y.val.obj (op S) := (coherentTopology LightProfinite).yonedaEquiv <|
+    (Adjunction.homEquiv (freeForgetAdjunction R) (S).toCondensed Y f)
+
+  obtain ⟨T, π, hπ, x, hx⟩ := this S y
+
+  let g : (free R).obj T.toCondensed ⟶ X :=
+    ((freeForgetAdjunction R).homEquiv T.toCondensed X).symm ((coherentTopology LightProfinite).yonedaEquiv.symm x)
+
+  have comm : g ≫ p = (lightProfiniteToLightCondSet ⋙ (LightCondensed.free R)).map π ≫ f := by
+    symm
+    rw [
+      Functor.comp_map,
+      ←Adjunction.homEquiv_naturality_left_square_iff (freeForgetAdjunction R),
+      Equiv.apply_symm_apply,
+      Sheaf.hom_ext_iff,
+      (coherentTopology LightProfinite).yonedaEquiv_symm_naturality_right,
+      hx,
+      (coherentTopology LightProfinite).map_yonedaEquiv',
+      ←(coherentTopology LightProfinite).yonedaEquiv_symm_naturality_right
+    ]
+    rfl
+
+  exact ⟨T, π, g, (LightProfinite.epi_iff_surjective π).mpr hπ, comm⟩
+
+instance : PreservesFiniteCoproducts (lightProfiniteToLightCondSet ⋙ (free R)) := by
+  have : PreservesFiniteCoproducts lightProfiniteToLightCondSet :=
+    instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet_leanCondensed
+  have : IsLeftAdjoint (free R) := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩
+  infer_instance
+
+noncomputable def hc {S T : LightProfinite} (π : T ⟶ S) [Epi π]
+    : IsColimit ((free R).mapCocone (explicitPullback.explicitRegular π)) := by
+  have : IsLeftAdjoint (free R) := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩
+  exact isColimitOfPreserves _ (explicitPullback.explicitRegularIsColimit _)
+
+noncomputable def c {X : LightCondMod R} {S T : LightProfinite} (π : T ⟶ (S ⊗ ℕ∪{∞}))
+    [Epi ((lightProfiniteToLightCondSet ⋙ (free R)).map <| smart_cover π)]
+    (g : ((lightProfiniteToLightCondSet ⋙ free R).obj T) ⟶ X)
+    (r_inf : T ⟶ (fibre ∞ (π ≫ snd _ _))) (σ : S ⟶ (fibre ∞ (π ≫ snd _ _)))
+    (hr : fibre_incl ∞ (π ≫ snd _ _) ≫ r_inf = 𝟙 (fibre ∞ (π ≫ snd _ _)))
+    : Cocone ((parallelPair (lightProfiniteToLightCondSet.map (explicitPullback.fst π π))
+  (lightProfiniteToLightCondSet.map (explicitPullback.snd π π))) ⋙ (free R)) := {
+    pt := X
+    ι :=  by
+      let ι_inf := fibre_incl ∞ (π ≫ snd _ _)
+      let π_inf := (fibre_incl ∞ (π ≫ snd _ _) ≫ π ≫ fst _ _)
+
+      let g_tilde : (lightProfiniteToLightCondSet ⋙ (free R)).obj T ⟶ X :=
+        g - (lightProfiniteToLightCondSet ⋙ (free R)).map (r_inf ≫ ι_inf) ≫ g
+            + (lightProfiniteToLightCondSet ⋙ (free R)).map (r_inf ≫ π_inf ≫ σ ≫ ι_inf) ≫ g
+      refine parallelPair.hom (_ ≫ g_tilde) g_tilde ?_ (by rfl)
+
+      rw [←cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map <| smart_cover π)]
+
+      let hcc := isColimitOfHasBinaryCoproductOfPreservesColimit
+        (lightProfiniteToLightCondSet ⋙ (free R)) T
+        (explicitPullback (fibre_incl ∞ (π ≫ snd _ _) ≫ π) (fibre_incl ∞ (π ≫ snd _ _) ≫ π))
+
+      apply hcc.hom_ext
+      rintro (j | j)
+      · simp only [const_obj_obj, Functor.comp_map, BinaryCofan.mk_pt,
+        BinaryCofan.ι_app_left, BinaryCofan.mk_inl, smart_cover, parallelPair_obj_zero,
+        parallelPair_obj_one, parallelPair_map_left, parallelPair_map_right, const_obj_map,
+        Category.comp_id]
+        simp only [comp_obj, pair_obj_left, explicitPullback.diagonal, parallelPair_obj_zero,
+          parallelPair_obj_one, ← map_comp_assoc, ← Functor.map_comp, coprod.desc_comp,
+          colimit.ι_desc, BinaryCofan.mk_pt, BinaryCofan.ι_app_left, BinaryCofan.mk_inl]
+        erw [PullbackCone.IsLimit.lift_fst]
+      · simp only [comp_obj, pair_obj_right, const_obj_obj, Functor.comp_map,
+        BinaryCofan.mk_pt, BinaryCofan.ι_app_right, BinaryCofan.mk_inr,
+        smart_cover, parallelPair_obj_zero, parallelPair_obj_one, parallelPair_map_left,
+        parallelPair_map_right, const_obj_map, Category.comp_id]
+        simp only [←Functor.comp_map]
+        simp only [←Category.assoc]
+        simp only [←Functor.map_comp]
+        rw [coprod.inr_desc]
+        simp only [Preadditive.comp_add, Preadditive.comp_sub, g_tilde]
+        simp [←Category.assoc, ←Functor.map_comp]
+        rw [
+          explicitPullback.map_fst, explicitPullback.map_snd,
+          Category.assoc _ (fibre_incl ∞ (π ≫ snd _ _)) r_inf, hr, Category.comp_id,
+          Category.assoc _ (fibre_incl ∞ (π ≫ snd _ _)) r_inf, hr, Category.comp_id,
+          sub_self, zero_add,
+          sub_self, zero_add,
+        ]
+        unfold π_inf
+        rw [
+          ←Category.assoc _ π _,
+          ←Category.assoc _ (fibre_incl ∞ (π ≫ snd _ _) ≫ π) _,
+          explicitPullback.condition
+        ]
+        rfl
+  }
+
+-- set_option maxHeartbeats 500000
+private theorem proj_explicit {X Y : LightCondMod R} (p : X ⟶ Y) [hp : Epi p] {S : LightProfinite}
+    (f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y) :
+      ∃ (S' : LightProfinite)
+        (ψ : S' ⟶ S)
+          (g : (free R).obj (S' ⊗ ℕ∪{∞}).toCondensed ⟶ X), Epi ψ
+            ∧ ((free R).map (lightProfiniteToLightCondSet.map (MonoidalCategoryStruct.tensorHom ψ (𝟙 ℕ∪{∞}))) ≫ f = g ≫ p) := by
+
+  obtain ⟨T, π, g, hπ, comm⟩ := comm_sq R p f
+  obtain ⟨S', T', y', π', g', hπ', hy', comp, ⟨⟨split⟩⟩, epi⟩ := refinedCover π
+
+  use S', y'
+
+  have : PreservesEpimorphisms (lightProfiniteToLightCondSet ⋙ (free R)) := by
+    have : IsLeftAdjoint (free R) := (freeForgetAdjunction R).isLeftAdjoint
+    infer_instance
+
+  by_cases hS' : Nonempty S'
+  -- The argument below only works if S' is non-empty. If S' is empty, the proof
+  -- is easier anyway.
+  · let hc : IsColimit ((free R).mapCocone (explicitPullback.explicitRegular π')) := hc R π'
+
+    let ι_inf := fibre_incl ∞ (π' ≫ snd _ _)
+    have : Mono ι_inf := fibre_incl_mono _ _
+    have : Nonempty (fibre ∞ (π' ≫ snd _ _)) := by
+      have : Epi (snd S' ℕ∪{∞}) := by
+        apply prod_epi
+      exact fibre_nonempty _ _
+
+    have fibre_injective : Injective (fibre ∞ (π' ≫ snd _ _)) := injective_of_light _
+    obtain ⟨r_inf, hr⟩ := fibre_injective.factors (𝟙 _) ι_inf
+
+    simp only [ι_inf] at hr
+
+    let π_inf := (fibre_incl ∞ (π' ≫ snd _ _) ≫ π' ≫ fst _ _)
+    let σ := split.section_
+    let hσ := split.id
+
+    let gg := (lightProfiniteToLightCondSet ⋙ (free R)).map g' ≫ g
+
+    let c' := c R π' gg r_inf σ hr
+
+    have : fibre_incl ∞ (π' ≫ snd _ _) ≫ π'
+        = fibre_incl ∞ (π' ≫ snd _ _) ≫ π'
+          ≫ fst _ _
+          ≫ lift (𝟙 _)
+            (CompHausLike.ofHom _ (ContinuousMap.const S' (∞ : ℕ∪{∞}))) :=
+      CartesianMonoidalCategory.hom_ext _ _ (by simp) (by ext; simp)
+
+    have : c'.ι.app WalkingParallelPair.one ≫ p
+      = (lightProfiniteToLightCondSet ⋙ (free R)).map (π' ≫ MonoidalCategoryStruct.tensorHom y' (𝟙 ℕ∪{∞})) ≫ f := by
+        simp only [gg, comp_obj, parallelPair_obj_one, c, Functor.comp_map,
+          const_obj_obj, Functor.map_comp, Category.assoc,
+          Preadditive.comp_add, Preadditive.comp_sub, parallelPair.hom_app,
+          Preadditive.add_comp, Preadditive.sub_comp, c']
+        rw [comm]
+        simp only [←Functor.map_comp, ←Functor.comp_map, ←Category.assoc, ←comp]
+        simp only [Category.assoc]
+        rw [
+          sub_add,
+          sub_eq_self,
+          sub_eq_zero,
+          ←Category.assoc _ π' _,
+          this,
+          ←Category.assoc _ (fst _ _),
+          ←Category.assoc _ (π' ≫ fst _ _),
+          ←Category.assoc σ,
+          ←Category.assoc σ,
+          hσ,
+          Category.id_comp
+        ]
+        rfl
+
+    let desc_map : ((free R).obj (S' ⊗ ℕ∪{∞}).toCondensed) ⟶ X := hc.desc c'
+    refine ⟨desc_map, inferInstance, ?_⟩
+
+    rw [
+      ←cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map π'),
+      ←Functor.comp_map, ←Functor.map_comp_assoc
+    ]
+    change _ = (((free R).mapCocone (explicitPullback.explicitRegular π')).ι.app one ≫ hc.desc c') ≫ p
+    erw [hc.fac]
+    rw [this]
+  · have : ¬Nonempty (S' ⊗ ℕ∪{∞} : LightProfinite) := empty_map hS' (fst _ _)
+    have : IsIso π' := empty_iso this _
+    obtain ⟨π'inv, h, _⟩ := this
+    use (lightProfiniteToLightCondSet ⋙ (free R)).map (π'inv ≫ g') ≫ g
+    refine ⟨hy', ?_⟩
+    rw [←cancel_epi ((lightProfiniteToLightCondSet ⋙ (free R)).map π')]
+    simp only [← Category.assoc, ← Functor.map_comp]
+    rw [h, Category.id_comp]
+    simp only [Category.assoc]
+    rw [comm]
+    simp only [← Category.assoc, ← Functor.map_comp]
+    rw [←comp]
+    simp
+
+theorem internallyProjective_ℕinfty : InternallyProjective ((free R).obj (ℕ∪{∞}).toCondensed) := by
+  rw [free_lightProfinite_internallyProjective_iff_tensor_condition' R ℕ∪{∞}]
+  intro X Y p hp S f
+  obtain ⟨S', π, g, hπ, comm⟩ := proj_explicit R p f
+  rw [LightProfinite.epi_iff_surjective] at hπ
+  use S', π, hπ, g, comm
+
+#print axioms internallyProjective_ℕinfty
diff --git a/LeanCondensed/Projects/Pullbacks.lean b/LeanCondensed/Projects/Pullbacks.lean
new file mode 100644
index 0000000..8c1a7c5
--- /dev/null
+++ b/LeanCondensed/Projects/Pullbacks.lean
@@ -0,0 +1,270 @@
+import Mathlib
+import LeanCondensed.Projects.Epi
+
+open CategoryTheory Functor Opposite LightProfinite OnePoint Limits LightCondensed
+  MonoidalCategory MonoidalClosed WalkingParallelPair WalkingParallelPairHom Topology
+
+universe u
+
+variable {X Y : LightProfinite} (y : Y) (f : X ⟶ Y)
+
+section
+
+instance (x : X) : IsClosed {x} := isClosed_singleton
+
+instance (S : Set Y) [IsClosed S] : IsClosed (f ⁻¹' S) := by
+  exact IsClosed.preimage f.1.continuous inferInstance
+
+instance : IsClosed (f ⁻¹' {y}) :=
+  inferInstance
+
+instance (S : Set X) [IsClosed S] : CompactSpace S := by
+  exact isCompact_iff_compactSpace.mp (IsClosed.isCompact inferInstance)
+
+instance : CompactSpace (f ⁻¹' {y}) := inferInstance
+
+end
+
+instance : TotallyDisconnectedSpace PUnit := by
+  have := TotallySeparatedSpace.of_discrete
+  apply TotallySeparatedSpace.totallyDisconnectedSpace
+
+def fibre : LightProfinite :=
+  ⟨
+    TopCat.of (f ⁻¹' {y}),
+    Subtype.totallyDisconnectedSpace,
+    TopologicalSpace.Subtype.secondCountableTopology (f ⁻¹' {y})
+  ⟩
+
+def fibre_incl : fibre y f ⟶ X :=
+  CompHausLike.ofHom _ ⟨Subtype.val, continuous_subtype_val⟩
+
+@[simp]
+def fibre_condition
+  : fibre_incl y f ≫ f = (CompHausLike.ofHom _  <| ContinuousMap.const (fibre y f) y)
+    := by ext x; exact x.2
+
+lemma fibre_incl_mono : Mono (fibre_incl y f) := by
+  rw [CompHausLike.mono_iff_injective]
+  exact Subtype.val_injective
+
+lemma fibre_incl_embedding : IsEmbedding (fibre_incl y f) := IsEmbedding.subtypeVal
+
+lemma fibre_nonempty [hepi : Epi f] : Nonempty (fibre y f) := by
+  rw [epi_iff_surjective f] at hepi
+  obtain ⟨x, hx⟩ := hepi y
+  exact ⟨x, hx⟩
+
+def point : LightProfinite := LightProfinite.of PUnit
+
+def fibreCone : PullbackCone (CompHausLike.ofHom _ <| ContinuousMap.const point y) f
+    :=
+  let space := f ⁻¹' {y}
+  have : IsClosed space :=  IsClosed.preimage f.1.continuous isClosed_singleton
+  have : IsCompact space := this.isCompact
+  have : CompactSpace space := by
+    exact isCompact_iff_compactSpace.mp this
+  PullbackCone.mk (CompHausLike.ofHom _ <| ContinuousMap.const (fibre y f) PUnit.unit) (fibre_incl y f)
+    (by ext x; simp only [fibre_incl, ConcreteCategory.comp_apply, CompHausLike.hom_ofHom,
+      ContinuousMap.const_apply, ContinuousMap.coe_mk]; rw [x.2])
+
+def fibreConeIsLimit : IsLimit (fibreCone y f) := by
+  refine PullbackCone.IsLimit.mk (fibreCone _ _).condition ?_ ?_ ?_ ?_
+  · intro cone
+    have : ∀ z : cone.pt, f (cone.snd z) = y := by
+      intro z
+      rw [
+        ←ConcreteCategory.comp_apply,
+        ←cone.condition,
+        ConcreteCategory.comp_apply
+      ]
+      rfl
+    refine CompHausLike.ofHom _ <| ⟨fun z ↦ ⟨cone.snd z, this z⟩, ?_⟩
+    rw [IsInducing.continuous_iff (fibre_incl_embedding y f).1]
+    exact cone.snd.1.continuous
+  repeat {exact fun cone ↦ rfl}
+  · intro cone m hm hm'
+    have := fibre_incl_mono y f
+    erw [←cancel_mono (fibre_incl y f), hm']
+    rfl
+
+def fibreLift {Z : LightProfinite} (g : Z ⟶ X) (hg : ∀ z, f (g z) = y) : Z ⟶ fibre y f :=
+  let space := f ⁻¹' {y}
+  have : IsClosed space :=  IsClosed.preimage f.1.continuous isClosed_singleton
+  have : IsCompact space := this.isCompact
+  have : CompactSpace space := by
+    exact isCompact_iff_compactSpace.mp this
+  CompHausLike.ofHom _ <| ⟨fun z ↦ ⟨g z, hg z⟩, by rw [IsInducing.continuous_iff (fibre_incl_embedding y f).1]; exact g.1.continuous⟩
+
+@[simp]
+lemma fibreLift_comp {Z : LightProfinite} (g : Z ⟶ X) (hg : ∀ z, f (g z) = y)
+  : fibreLift y f g hg ≫ fibre_incl y f = g := rfl
+
+section
+
+variable {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z)
+
+instance : IsClosed {⟨x,y⟩ : X × Y | f x = g y} := by
+  apply IsClosed.mk
+  rw [isOpen_prod_iff]
+  intro a b hab
+  obtain ⟨u, v, hu, hv, ha, hb, huv⟩ := t2_separation hab
+  refine ⟨
+      f⁻¹'u, g⁻¹'v,
+      f.1.continuous.isOpen_preimage _ hu,
+      g.1.continuous.isOpen_preimage _ hv,
+      ha, hb, ?_
+  ⟩
+  intro ⟨x, y⟩ ⟨hx, hy⟩ hxy
+  simp only [Set.mem_preimage] at hx hy
+  rw [hxy] at hx
+  exact (Set.disjoint_iff (s := u) (t := v)).mp huv ⟨hx, hy⟩
+
+instance : IsCompact {⟨x,y⟩ : X × Y | f x = g y} := by
+  apply IsClosed.isCompact
+  infer_instance
+
+instance : CompactSpace {⟨x,y⟩ : X × Y | f x = g y} := by
+  rw [←isCompact_iff_compactSpace]
+  exact
+    instIsCompactProdCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologySetOfMatch_1PropEqCoeContinuousMapHomLightProfinite
+      f g
+
+end
+
+def explicitPullback {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) : LightProfinite
+    :=
+  ⟨TopCat.of {⟨x,y⟩ : X × Y | f x = g y}, inferInstance, inferInstance⟩
+
+namespace explicitPullback
+
+variable {X Y Z : LightProfinite} {f : X ⟶ Z} {g : Y ⟶ Z}
+
+def fst (f : X ⟶ Z) (g : Y ⟶ Z) : explicitPullback f g ⟶ X :=
+  TopCat.ofHom
+    ⟨
+      (Prod.fst : X × Y → X) ∘ (Subtype.val : _ → X × Y),
+      Continuous.comp continuous_fst continuous_subtype_val
+    ⟩
+
+def snd (f : X ⟶ Z) (g : Y ⟶ Z) : explicitPullback f g ⟶ Y :=
+  TopCat.ofHom
+    ⟨
+      (Prod.snd : X × Y → Y) ∘ (Subtype.val : _ → X × Y),
+      Continuous.comp continuous_snd continuous_subtype_val
+    ⟩
+
+instance epi_pullback [hepi : Epi f] : Epi (snd (f := f) (g := g)) := by
+  rw [LightProfinite.epi_iff_surjective] at hepi ⊢
+  intro y
+  obtain ⟨x, hx⟩ := hepi (g y)
+  exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩
+
+
+lemma condition : fst (f := f) (g := g) ≫ f = snd (f := f) (g := g) ≫ g := by
+  ext ⟨_,hxy⟩
+  exact hxy
+
+def Cone (f : X ⟶ Z) (g : Y ⟶ Z) : PullbackCone f g :=
+  PullbackCone.mk (fst _ _) (snd _ _) condition
+
+lemma Cone.fst_eq : (Cone f g).fst = fst _ _ := rfl
+lemma Cone.snd_eq : (Cone f g).snd = snd _ _ := rfl
+
+def IsLimit : IsLimit (Cone f g) := by
+  let space := {⟨x,y⟩ : X × Y | f x = g y}
+  have : IsClosed space := by
+    apply IsClosed.mk
+    rw [isOpen_prod_iff]
+    intro a b hab
+    obtain ⟨u, v, hu, hv, ha, hb, huv⟩ := t2_separation hab
+    refine ⟨
+      f⁻¹'u, g⁻¹'v,
+      f.1.continuous.isOpen_preimage _ hu,
+      g.1.continuous.isOpen_preimage _ hv,
+      ha, hb, ?_
+    ⟩
+    intro ⟨x, y⟩ ⟨hx, hy⟩
+    simp only [Set.mem_preimage] at hx hy
+    intro hxy
+    rw [hxy] at hx
+    exact (Set.disjoint_iff (s := u) (t := v)).mp huv ⟨hx, hy⟩
+  have : IsCompact space := this.isCompact
+  have : CompactSpace space := by
+    exact isCompact_iff_compactSpace.mp this
+
+  refine PullbackCone.IsLimit.mk ?_ ?_ ?_ ?_ ?_
+  · intro cone
+    have : ∀ z, ⟨cone.fst z, cone.snd z⟩ ∈ space := by
+      intro z
+      simp only [Set.mem_setOf_eq, space]
+      rw [←ConcreteCategory.comp_apply, cone.condition]
+      rfl
+    refine TopCat.ofHom ⟨fun z ↦ ⟨⟨cone.fst z, cone.snd z⟩, this z⟩, ?_⟩
+    rw [(IsInducing.continuous_iff IsEmbedding.subtypeVal.1)]
+    exact Continuous.prodMk cone.fst.1.continuous cone.snd.1.continuous
+  repeat {intro cone; ext z; rfl}
+  · intro cone m hm hm'
+    ext z
+    apply Subtype.ext
+    apply Prod.ext
+    change fst _ _ (↑((ConcreteCategory.hom m) z)) = _
+    rw [←ConcreteCategory.comp_apply, hm]
+    rfl
+    change snd _ _ (↑((ConcreteCategory.hom m) z)) = _
+    rw [←ConcreteCategory.comp_apply, hm']
+    rfl
+
+def diagonal (f : X ⟶ Y) : X ⟶ explicitPullback f f
+  := PullbackCone.IsLimit.lift IsLimit (𝟙 _) (𝟙 _) rfl
+
+def map {X' Y' Z' : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : X' ⟶ Z')
+  (g' : Y' ⟶ Z') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : Z ⟶ Z')
+  (eq₁ : f ≫ i₃ = i₁ ≫ f') (eq₂ : g ≫ i₃ = i₂ ≫ g')
+  : explicitPullback f g ⟶ explicitPullback f' g' :=
+    PullbackCone.IsLimit.lift IsLimit (fst _ _ ≫ i₁) (snd _ _ ≫ i₂)
+      (by rw [Category.assoc, Category.assoc, ←eq₁, ←eq₂, ←Cone.fst_eq,
+              PullbackCone.condition_assoc, Cone.snd_eq])
+
+lemma map_fst {X' Y' Z' : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : X' ⟶ Z')
+  (g' : Y' ⟶ Z') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : Z ⟶ Z')
+  (eq₁ : f ≫ i₃ = i₁ ≫ f') (eq₂ : g ≫ i₃ = i₂ ≫ g') : map f g f' g' i₁ i₂ i₃ eq₁ eq₂ ≫ fst f' g' = fst f g ≫ i₁ := rfl
+
+lemma map_snd {X' Y' Z' : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : X' ⟶ Z')
+  (g' : Y' ⟶ Z') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : Z ⟶ Z')
+  (eq₁ : f ≫ i₃ = i₁ ≫ f') (eq₂ : g ≫ i₃ = i₂ ≫ g') : map f g f' g' i₁ i₂ i₃ eq₁ eq₂ ≫ snd f' g' = snd f g ≫ i₂ := rfl
+
+def explicitPair  {X Y : LightProfinite} (π : X ⟶ Y) : WalkingParallelPair ⥤ LightCondSet
+  := parallelPair
+    (lightProfiniteToLightCondSet.map (fst π π)) (lightProfiniteToLightCondSet.map (snd π π))
+
+noncomputable def explicitPullbackIsoPullback {X Y : LightProfinite} (π : X ⟶ Y) : explicitPullback π π ≅ pullback π π :=
+  Limits.IsLimit.conePointUniqueUpToIso (IsLimit (f := π) (g := π)) (pullback.isLimit π π)
+
+noncomputable def explicitPairIsoPair {X Y : LightProfinite} (π : X ⟶ Y) : explicitPair π ≅ πpair π :=
+  parallelPair.ext
+    (lightProfiniteToLightCondSet.mapIso (explicitPullbackIsoPullback π) : (explicitPair π).obj zero ≅ (πpair π).obj zero)
+    (Iso.refl _)
+    (
+        by simp [←Functor.map_comp, explicitPair, πpair, explicitPullbackIsoPullback]; rfl
+    )
+    (
+        by simp [←Functor.map_comp, explicitPair, πpair, explicitPullbackIsoPullback]; rfl
+    )
+
+def explicitRegular {X Y : LightProfinite} (π : X ⟶ Y)
+    : Cofork (lightProfiniteToLightCondSet.map <| fst π π)
+      (lightProfiniteToLightCondSet.map <| snd π π) :=
+  Cofork.ofπ (lightProfiniteToLightCondSet.map π)
+    (by simp only [←Functor.map_comp, condition])
+
+noncomputable def explicitRegularIsColimit {X Y : LightProfinite} (π : X ⟶ Y) [hepi : Epi π]
+    : IsColimit (explicitRegular π) := by
+  rw [LightProfinite.epi_iff_surjective, ←LightProfinite.effectiveEpi_iff_surjective] at hepi
+  exact (
+    IsColimit.equivOfNatIsoOfIso
+      (explicitPairIsoPair _)
+      _
+      (regular _)
+      (Cofork.ext (Iso.refl _) rfl)
+  ).symm (regular_IsColimit _)
diff --git a/LeanCondensed/Projects/Sequence.lean b/LeanCondensed/Projects/Sequence.lean
new file mode 100644
index 0000000..9bf1c71
--- /dev/null
+++ b/LeanCondensed/Projects/Sequence.lean
@@ -0,0 +1,53 @@
+import Mathlib
+
+open CategoryTheory Limits LightProfinite OnePoint
+
+namespace LightCondensed
+
+noncomputable section
+
+variable (R : Type _) [CommRing R]
+
+def ι : LightProfinite.of PUnit.{1} ⟶ ℕ∪{∞} :=
+  (TopCat.ofHom ⟨fun _ ↦ ∞, continuous_const⟩)
+
+def ι_split : SplitMono ι where
+  retraction := (TopCat.ofHom ⟨fun _ ↦ PUnit.unit, continuous_const⟩)
+  id := rfl
+
+def P_map :
+    (free R).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free R).obj (ℕ∪{∞}).toCondensed :=
+  (lightProfiniteToLightCondSet ⋙ free R).map ι
+
+def P : LightCondMod R := cokernel (P_map R)
+
+def P_proj : (free R).obj (ℕ∪{∞}).toCondensed ⟶ P R := cokernel.π _
+
+def PSequence : ShortComplex (LightCondMod R) :=
+  ShortComplex.mk (P_map R) (P_proj R) (cokernel.condition _)
+
+lemma PSequence_exact : (PSequence R).ShortExact := by
+  refine ShortComplex.ShortExact.mk' ?_
+    (SplitMono.mono ((ι_split).map (lightProfiniteToLightCondSet ⋙ free R)))
+    coequalizer.π_epi
+  rw [ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero,
+    ←kernel.condition (P_proj R)]
+  rfl
+
+def PSequence_split : (PSequence R).Splitting :=
+  ShortComplex.Splitting.ofExactOfRetraction _
+    (PSequence_exact R).exact _
+    ((ι_split).map (lightProfiniteToLightCondSet ⋙ free R)).id
+    coequalizer.π_epi
+
+def P_proj_split : SplitEpi (P_proj R) where
+  section_ := (PSequence_split R).s
+  id := (PSequence_split R).s_g
+
+def P_retract : Retract (P R) ((free R).obj (ℕ∪{∞}).toCondensed) where
+  i := _
+  r := _
+  retract := (PSequence_split R).s_g
+
+def P_homMk (A : LightCondMod R) (f : (free R).obj (ℕ∪{∞}).toCondensed ⟶ A)
+    (hf : P_map R ≫ f = 0) : P R ⟶ A := cokernel.desc _ f hf
diff --git a/LeanCondensed/Projects/SheafMonoidal.lean b/LeanCondensed/Projects/SheafMonoidal.lean
index ea6b060..0be9898 100644
--- a/LeanCondensed/Projects/SheafMonoidal.lean
+++ b/LeanCondensed/Projects/SheafMonoidal.lean
@@ -13,7 +13,7 @@ import LeanCondensed.Projects.LocalizedMonoidal
 
 universe v u
 
-open CategoryTheory MonoidalCategory
+open CategoryTheory MonoidalCategory Functor
 
 namespace CategoryTheory.Functor.Monoidal
 
@@ -37,11 +37,11 @@ variable {A B : Type*} [Category A] [Category B]
 
 attribute [local instance] monoidalCategory
 
--- noncomputable instance : (presheafToSheaf _ _ ⋙ composeAndSheafify J F).Monoidal :=
---   monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm
+noncomputable instance : (presheafToSheaf _ _ ⋙ composeAndSheafify J F).Monoidal :=
+  monoidalTransport (presheafToSheafCompComposeAndSheafifyIso J F).symm
 
--- noncomputable instance : (composeAndSheafify J F).Monoidal :=
---   Localization.Monoidal.functorMonoidalOfComp (presheafToSheaf _ _) J.W (Iso.refl _) _
+noncomputable instance : (composeAndSheafify J F).Monoidal :=
+  Localization.Monoidal.functorMonoidalOfComp (presheafToSheaf _ _) J.W (Iso.refl _) _
 
 end
 
diff --git a/lake-manifest.json b/lake-manifest.json
index de149b2..ab3c7be 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c30c25bf81ec9a1983c7381a45be6287c13953ed",
+   "rev": "287febc23a1ff0df9c02d934fb82934e8bc90a85",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5",
+   "rev": "304c5e2f490d546134c06bf8919e13b175272084",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873",
+   "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
+   "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.67",
+   "inputRev": "v0.0.59",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244",
+   "rev": "9264d548cf1ccf0ba454b82f931f44c37c299fc1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "867d9dc77534341321179c9aa40fceda675c50d4",
+   "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3cabaef23886b82ba46f07018f2786d9496477d6",
+   "rev": "78e1181c4752c7e10874d2ed5a6a15063f4a35b6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
+   "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",