diff --git a/Mathlib.lean b/Mathlib.lean
index d7ed81545af8e4..73b412994b9822 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -643,6 +643,7 @@ public import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
 public import Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
 public import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
 public import Mathlib.Algebra.Homology.HomotopyCofiber
+public import Mathlib.Algebra.Homology.HomotopyFiber
 public import Mathlib.Algebra.Homology.ImageToKernel
 public import Mathlib.Algebra.Homology.LeftResolution.Basic
 public import Mathlib.Algebra.Homology.LeftResolution.Reduced
diff --git a/Mathlib/Algebra/Homology/ComplexShape.lean b/Mathlib/Algebra/Homology/ComplexShape.lean
index 66899bc1022026..7db47640aa55dd 100644
--- a/Mathlib/Algebra/Homology/ComplexShape.lean
+++ b/Mathlib/Algebra/Homology/ComplexShape.lean
@@ -94,6 +94,13 @@ def symm (c : ComplexShape ι) : ComplexShape ι where
   next_eq w w' := c.prev_eq w w'
   prev_eq w w' := c.next_eq w w'
 
+/-- If `c : ComplexShape α` is such that `c.Rel` is decidable, it is also the
+case of `c.symm.Rel`. -/
+@[implicit_reducible]
+def decidableRelSymm {α : Type*} (c : ComplexShape α) [DecidableRel c.Rel] :
+    DecidableRel c.symm.Rel :=
+  fun a b ↦ decidable_of_iff (c.Rel b a) Iff.rfl
+
 @[simp]
 theorem symm_symm (c : ComplexShape ι) : c.symm.symm = c := rfl
 
diff --git a/Mathlib/Algebra/Homology/HomotopyCofiber.lean b/Mathlib/Algebra/Homology/HomotopyCofiber.lean
index 099b803017cf36..da1b6d6fafc5a4 100644
--- a/Mathlib/Algebra/Homology/HomotopyCofiber.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCofiber.lean
@@ -79,6 +79,16 @@ noncomputable def XIso (i : ι) (hi : ¬ c.Rel i (c.next i)) :
     X φ i ≅ G.X i :=
   eqToIso (dif_neg hi)
 
+lemma isZero_X (i : ι) (hG : IsZero (G.X i))
+    (hF : ∀ (j : ι), c.Rel i j → IsZero (F.X j)) :
+    IsZero (X φ i) := by
+  by_cases h : c.Rel i (c.next i)
+  · haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ h
+    refine IsZero.of_iso ?_ (XIsoBiprod φ _ _ h)
+    simp only [biprod_isZero_iff]
+    exact ⟨hF _ h, hG⟩
+  · exact hG.of_iso (XIso φ i h)
+
 /-- The second projection `(homotopyCofiber φ).X i ⟶ G.X i`. -/
 noncomputable def sndX (i : ι) : X φ i ⟶ G.X i :=
   if hi : c.Rel i (c.next i)
@@ -376,7 +386,13 @@ section
 
 variable (K)
 variable [∀ i, HasBinaryBiproduct (K.X i) (K.X i)]
-  [HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))]
+
+/-- Given a homological complex `K`, this is the property that the morphism
+`K ⟶ K ⊞ K` induced by `𝟙 K` and `-𝟙 K` has a cofiber, which allows
+to define `K.cylinder` as this cofiber. -/
+abbrev HasCylinder : Prop := HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
+
+variable [K.HasCylinder]
 
 /-- The cylinder object of a homological complex `K` is the homotopy cofiber
 of the morphism  `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`. -/
@@ -525,6 +541,7 @@ noncomputable def πCompι₀Homotopy : Homotopy (π K ≫ ι₀ K) (𝟙 K.cyli
       (πCompι₀Homotopy.nullHomotopy K))
 
 /-- The homotopy equivalence between `K.cylinder` and `K`. -/
+@[simps]
 noncomputable def homotopyEquiv : HomotopyEquiv K.cylinder K where
   hom := π K
   inv := ι₀ K
diff --git a/Mathlib/Algebra/Homology/HomotopyFiber.lean b/Mathlib/Algebra/Homology/HomotopyFiber.lean
new file mode 100644
index 00000000000000..e5efe421ca2e24
--- /dev/null
+++ b/Mathlib/Algebra/Homology/HomotopyFiber.lean
@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2023 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.HomotopyCofiber
+public import Mathlib.Algebra.Homology.Opposite
+
+/-!
+# The homotopy fiber of a morphism of homological complexes
+
+In this file, we construct the homotopy fiber of a morphism `φ : F ⟶ G`
+between homological complexes. Moreover, we dualise the definition
+of the cylinder (which is a particular case of a homotopy cofiber)
+in order to define the path object of a homological complex.
+
+-/
+
+@[expose] public section
+
+open CategoryTheory Category Limits Preadditive Opposite
+
+variable {C : Type*} [Category* C] [Preadditive C]
+
+namespace HomologicalComplex
+
+attribute [local instance] ComplexShape.decidableRelSymm
+
+variable {α : Type*} {c : ComplexShape α} {F G K : HomologicalComplex C c} (φ : F ⟶ G)
+
+variable [DecidableRel c.Rel]
+
+section
+
+/-- A morphism of homological complexes `φ : F ⟶ G` has a homotopy fiber if for all
+indices `i` and `j` such that `c.Rel i j`, the binary biproduct `F.X i ⊞ G.X j` exists. -/
+class HasHomotopyFiber (φ : F ⟶ G) : Prop where
+  hasBinaryBiproduct (φ) (i j : α) (hij : c.Rel i j) : HasBinaryBiproduct (G.X i) (F.X j)
+
+instance [HasBinaryBiproducts C] : HasHomotopyFiber φ where
+  hasBinaryBiproduct _ _ _ := inferInstance
+
+variable [HasHomotopyFiber φ] [DecidableRel c.Rel]
+
+instance : HasHomotopyCofiber ((opFunctor C c).map φ.op) where
+  hasBinaryBiproduct i j hij := by
+    have := HasHomotopyFiber.hasBinaryBiproduct φ j i hij
+    dsimp
+    infer_instance
+
+/-- The homotopy fiber of a morphism between homological complexes. -/
+noncomputable def homotopyFiber : HomologicalComplex C c :=
+  (unopFunctor C c.symm).obj (op (homotopyCofiber ((opFunctor C c).map φ.op)))
+
+end
+
+variable (K) [∀ i, HasBinaryBiproduct (K.X i) (K.X i)]
+
+instance (i : α) : HasBinaryBiproduct (K.op.X i) (K.op.X i) := by
+  dsimp; infer_instance
+
+/-- The property that a homological complex `K` has a path object,
+i.e. that the morphism `K ⟶ K ⊞ K` induced by `𝟙 K` and `-𝟙 K`
+has a homotopy fiber. -/
+abbrev HasPathObject := HasHomotopyFiber (biprod.desc (𝟙 K) (-𝟙 K))
+
+instance [K.HasPathObject] :
+    HasHomotopyCofiber (biprod.lift (𝟙 K.op) (-𝟙 K.op)) where
+  hasBinaryBiproduct i j hij := by
+    have := HasHomotopyFiber.hasBinaryBiproduct (biprod.desc (𝟙 K) (-𝟙 K)) j i hij
+    exact hasBinaryBiproduct_of_iso (Iso.refl _ : op (K.X j) ≅ K.op.X j)
+      (show op ((K ⊞ K).X i) ≅ (K.op ⊞ K.op).X i from
+        ((eval _ _ i).mapBiprod K K).op.symm ≪≫ biprod.opIso _ _ ≪≫
+          ((eval _ _ i).mapBiprod K.op K.op).symm)
+
+variable [K.HasPathObject]
+
+/-- The path object of a homological complex is defined here by dualizing
+the cylinder object of `K.op`. -/
+@[no_expose]
+noncomputable def pathObject := (unopFunctor C c.symm).obj (op K.op.cylinder)
+
+namespace pathObject
+
+lemma isZero_X (i : α) (h₁ : IsZero (K.X i)) (h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)) :
+    IsZero (K.pathObject.X i) := by
+  apply IsZero.unop
+  dsimp [pathObject]
+  refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ IsZero.op (h₂ _ hj))
+  exact IsZero.of_iso (by simpa using h₁.op)
+    ((eval Cᵒᵖ c.symm i).mapBiprod K.op K.op)
+
+/-- The first projection `K.pathObject ⟶ K`. -/
+@[no_expose]
+noncomputable def π₀ : K.pathObject ⟶ K :=
+  (unopFunctor C c.symm).map (cylinder.ι₀ K.op).op
+
+/-- The second projection `K.pathObject ⟶ K`. -/
+@[no_expose]
+noncomputable def π₁ : K.pathObject ⟶ K :=
+  (unopFunctor C c.symm).map (cylinder.ι₁ K.op).op
+
+/-- The inclusion `K ⟶ K.pathObject`. -/
+@[no_expose]
+noncomputable def ι : K ⟶ K.pathObject :=
+  (unopFunctor C c.symm).map (cylinder.π K.op).op
+
+@[reassoc (attr := simp)]
+lemma π₀_ι : ι K ≫ π₀ K = 𝟙 K :=
+  Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₀_π K.op))
+
+@[reassoc (attr := simp)]
+lemma π₁_ι : ι K ≫ π₁ K = 𝟙 K :=
+  Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₁_π K.op))
+
+/-- The homotopy between `π₀ K ≫ ι K` and `𝟙 K.pathObject`. -/
+@[no_expose]
+noncomputable def π₀CompιHomotopy (hc : ∀ (i : α), ∃ j, c.Rel i j) :
+    Homotopy (π₀ K ≫ ι K) (𝟙 K.pathObject) :=
+  (cylinder.πCompι₀Homotopy K.op hc).unop
+
+/-- The homotopy equivalence between `K` and `K.pathObject`. -/
+@[simps]
+noncomputable def homotopyEquiv (hc : ∀ (i : α), ∃ j, c.Rel i j) :
+    HomotopyEquiv K K.pathObject where
+  hom := ι K
+  inv := π₀ K
+  homotopyHomInvId := Homotopy.ofEq (by simp)
+  homotopyInvHomId := π₀CompιHomotopy K hc
+
+/-- The homotopy between `pathObject.ι₀ K` and `pathObject.ι₁ K`. -/
+@[no_expose]
+noncomputable def homotopy₀₁ (hc : ∀ (i : α), ∃ j, c.Rel i j) : Homotopy (π₀ K) (π₁ K) :=
+  (cylinder.homotopy₀₁ K.op hc).unop
+
+section
+
+variable {K} (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁)
+
+/-- The morphism `F ⟶ K.pathObject` that is induced by two morphisms `φ₀ φ₁ : F ⟶ K`
+and a homotopy `h : Homotopy φ₀ φ₁`. -/
+@[no_expose]
+noncomputable def lift : F ⟶ K.pathObject :=
+  letI φ : K.op.cylinder ⟶ (opFunctor C c).obj (op F) :=
+    cylinder.desc ((opFunctor C c).map φ₀.op)
+      ((opFunctor C c).map φ₁.op) h.op
+  (unopFunctor C c.symm).map φ.op
+
+@[reassoc (attr := simp)]
+lemma lift_π₀ : lift φ₀ φ₁ h ≫ π₀ K = φ₀ :=
+  Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₀_desc _ _ _))
+
+@[reassoc (attr := simp)]
+lemma lift_π₁ : lift φ₀ φ₁ h ≫ π₁ K = φ₁ :=
+  Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₁_desc _ _ _))
+
+end
+
+end pathObject
+
+end HomologicalComplex
diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean
index 10e5d2d49f745b..6810dd4cd77228 100644
--- a/Mathlib/Algebra/Homology/Opposite.lean
+++ b/Mathlib/Algebra/Homology/Opposite.lean
@@ -160,6 +160,9 @@ def opEquivalence : (HomologicalComplex V c)ᵒᵖ ≌ HomologicalComplex Vᵒ
       opFunctor_map_f, Hom.isoOfComponents_hom_f]
     exact Category.comp_id _
 
+instance : (opFunctor V c).IsEquivalence := (opEquivalence V c).isEquivalence_functor
+instance : (opInverse V c).IsEquivalence := (opEquivalence V c).isEquivalence_inverse
+
 set_option backward.isDefEq.respectTransparency false in
 /-- Auxiliary definition for `unopEquivalence`. -/
 @[simps]
@@ -211,6 +214,9 @@ def unopEquivalence : (HomologicalComplex Vᵒᵖ c)ᵒᵖ ≌ HomologicalComple
     simp only [comp_f]
     exact Category.comp_id _
 
+instance : (unopFunctor V c).IsEquivalence := (unopEquivalence V c).isEquivalence_functor
+instance : (unopInverse V c).IsEquivalence := (unopEquivalence V c).isEquivalence_inverse
+
 instance (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] :
     K.op.HasHomology i :=
   inferInstanceAs <| (K.sc i).op.HasHomology
@@ -435,3 +441,36 @@ instance unopFunctor_additive : (@unopFunctor ι V _ c _).Additive where
 end
 
 end HomologicalComplex
+
+namespace Homotopy
+
+open HomologicalComplex
+
+variable {V : Type*} [Category* V] {ι : Type*} {c : ComplexShape ι} [Preadditive V]
+
+/-- The opposite of a homotopy between morphisms of homological complexes. -/
+@[simps]
+def op {F G : HomologicalComplex V c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) :
+    Homotopy ((opFunctor V c).map φ₁.op) ((opFunctor V c).map φ₂.op) where
+  hom i j := (h.hom j i).op
+  zero i j hij := Quiver.Hom.unop_inj (h.zero _ _ hij)
+  comm n := Quiver.Hom.unop_inj (by
+    dsimp
+    rw [h.comm n]
+    nth_rw 2 [add_comm]
+    rfl)
+
+/-- The homotopy between morphisms of homological complexes that is deduced
+from a homotopy in the opposite category. -/
+@[simps]
+def unop {F G : HomologicalComplex Vᵒᵖ c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) :
+    Homotopy ((unopFunctor V c).map φ₁.op) ((unopFunctor V c).map φ₂.op) where
+  hom i j := (h.hom j i).unop
+  zero i j hij := Quiver.Hom.op_inj (h.zero _ _ hij)
+  comm n := Quiver.Hom.op_inj (by
+    dsimp
+    rw [h.comm n]
+    nth_rw 2 [add_comm]
+    rfl)
+
+end Homotopy