diff --git a/Mathlib.lean b/Mathlib.lean
index cd72d6d36a5d31..0578f774d3598e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2752,6 +2752,7 @@ public import Mathlib.CategoryTheory.Limits.Shapes.Products
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
+public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
@@ -3119,6 +3120,7 @@ public import Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
 public import Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
 public import Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
 public import Mathlib.CategoryTheory.Sites.Descent.DescentData
+public import Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
 public import Mathlib.CategoryTheory.Sites.Descent.IsPrestack
 public import Mathlib.CategoryTheory.Sites.Descent.IsStack
 public import Mathlib.CategoryTheory.Sites.Descent.Precoverage
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean
new file mode 100644
index 00000000000000..d5321aa9547e29
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean
@@ -0,0 +1,255 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Christian Merten
+-/
+module
+
+public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
+
+/-!
+# Chosen pullbacks
+
+Given two morphisms `f₁ : X₁ ⟶ S` and `f₂ : X₂ ⟶ S`, we introduce
+a structure `ChosenPullback f₁ f₂` which contains the data of
+pullback of `f₁` and `f₂`.
+
+## TODO
+* relate this to `ChosenPullbacksAlong` which is defined in
+`LocallyCartesianClosed.ChosenPullbacksAlong`.
+
+-/
+
+@[expose] public section
+
+universe v u
+
+namespace CategoryTheory.Limits
+
+variable {C : Type u} [Category.{v} C]
+
+/-- Given two morphisms `f₁ : X₁ ⟶ S` and `f₂ : X₂ ⟶ S`, this is the choice
+of a pullback of `f₁` and `f₂`. -/
+structure ChosenPullback {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) where
+  /-- the pullback -/
+  pullback : C
+  /-- the first projection -/
+  p₁ : pullback ⟶ X₁
+  /-- the second projection -/
+  p₂ : pullback ⟶ X₂
+  condition : p₁ ≫ f₁ = p₂ ≫ f₂
+  /-- `pullback` is a pullback of `f₁` and `f₂` -/
+  isLimit : IsLimit (PullbackCone.mk _ _ condition)
+  /-- the projection `pullback ⟶ S` -/
+  p : pullback ⟶ S := p₁ ≫ f₁
+  hp₁ : p₁ ≫ f₁ = p := by cat_disch
+
+namespace ChosenPullback
+
+section
+
+variable {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
+  (h : ChosenPullback f₁ f₂)
+
+attribute [reassoc] condition
+
+lemma isPullback : IsPullback h.p₁ h.p₂ f₁ f₂ where
+  w := h.condition
+  isLimit' := ⟨h.isLimit⟩
+
+attribute [reassoc (attr := simp)] hp₁
+
+@[reassoc (attr := simp)]
+lemma hp₂ : h.p₂ ≫ f₂ = h.p := by rw [← h.condition, hp₁]
+
+/-- Given `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S`, `h : ChosenPullback f₁ f₂` and morphisms
+`g₁ : Y ⟶ X₁`, `g₂ : Y ⟶ X₂` and `b : Y ⟶ S`, this structure contains a morphism
+`Y ⟶ h.pullback` such that `f ≫ h.p₁ = g₁`, `f ≫ h.p₂ = g₂` and `f ≫ h.p = b`.
+(This is nonempty only when `g₁ ≫ f₁ = g₂ ≫ f₂ = b`.) -/
+structure LiftStruct {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (b : Y ⟶ S) where
+  /-- a lifting to the pullback -/
+  f : Y ⟶ h.pullback
+  f_p₁ : f ≫ h.p₁ = g₁
+  f_p₂ : f ≫ h.p₂ = g₂
+  f_p : f ≫ h.p = b
+
+namespace LiftStruct
+
+attribute [reassoc (attr := simp)] f_p₁ f_p₂ f_p
+
+variable {h} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (l : h.LiftStruct g₁ g₂ b)
+
+include l in
+@[reassoc]
+lemma w : g₁ ≫ f₁ = g₂ ≫ f₂ := by
+  simp only [← l.f_p₁, ← l.f_p₂, Category.assoc, h.condition]
+
+instance : Subsingleton (h.LiftStruct g₁ g₂ b) where
+  allEq := by
+    rintro ⟨f, f_p₁, f_p₂, _⟩ ⟨f', f'_p₁, f'_p₂, _⟩
+    obtain rfl : f = f' := by
+      apply h.isPullback.hom_ext
+      · rw [f_p₁, f'_p₁]
+      · rw [f_p₂, f'_p₂]
+    rfl
+
+lemma nonempty (w : g₁ ≫ f₁ = g₂ ≫ f₂) (hf₁ : g₁ ≫ f₁ = b) :
+    Nonempty (h.LiftStruct g₁ g₂ b) := by
+  obtain ⟨l, h₁, h₂⟩ := h.isPullback.exists_lift g₁ g₂ w
+  exact ⟨{
+    f := l
+    f_p₁ := h₁
+    f_p₂ := h₂
+    f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁]
+  }⟩
+
+end LiftStruct
+
+end
+
+variable {X S : C} {f : X ⟶ S} (h : ChosenPullback f f)
+
+/-- Given `f : X ⟶ S` and `h : ChosenPullback f f`, this is the type of
+morphisms `l : X ⟶ h.pullback` that are equal to the diagonal map. -/
+abbrev Diagonal := h.LiftStruct (𝟙 X) (𝟙 X) f
+
+instance : Nonempty h.Diagonal := by apply LiftStruct.nonempty <;> cat_disch
+
+end ChosenPullback
+
+variable {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
+  (h₁₂ : ChosenPullback f₁ f₂) (h₂₃ : ChosenPullback f₂ f₃) (h₁₃ : ChosenPullback f₁ f₃)
+
+/-- Given three morphisms `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S` and `f₃ : X₃ ⟶ S`, and chosen
+pullbacks for `(f₁, f₂)`, `(f₂, f₃)` and `(f₁, f₃)`, this structure contains the data
+of a wide pullback of the three morphisms `f₁`, `f₂` and `f₃`. -/
+structure ChosenPullback₃ where
+  /-- A chosen pullback of `h₁₂.pullback` and `h₂₃.pullback` over `X₂`. -/
+  chosenPullback : ChosenPullback h₁₂.p₂ h₂₃.p₁
+  /-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `S`. -/
+  p : chosenPullback.pullback ⟶ S := chosenPullback.p₁ ≫ h₁₂.p
+  /-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₁`. -/
+  p₁ : chosenPullback.pullback ⟶ X₁ := chosenPullback.p₁ ≫ h₁₂.p₁
+  /-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₃`. -/
+  p₃ : chosenPullback.pullback ⟶ X₃ := chosenPullback.p₂ ≫ h₂₃.p₂
+  /-- A morphism from the wide pullback `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₃`
+  that is compatible with projections. -/
+  l : h₁₃.LiftStruct p₁ p₃ p
+  hp₁ : chosenPullback.p₁ ≫ h₁₂.p₁ = p₁ := by cat_disch
+  hp₃ : chosenPullback.p₂ ≫ h₂₃.p₂ = p₃ := by cat_disch
+
+namespace ChosenPullback₃
+
+variable {h₁₂ h₂₃ h₁₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃)
+
+/-- The chosen wide pullback of `(f₁, f₂, f₃)`. -/
+abbrev pullback := h.chosenPullback.pullback
+
+/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₃`. -/
+def p₁₃ : h.pullback ⟶ h₁₃.pullback := h.l.f
+
+/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₂`. -/
+def p₁₂ : h.pullback ⟶ h₁₂.pullback := h.chosenPullback.p₁
+
+/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₂` and `f₃`. -/
+def p₂₃ : h.pullback ⟶ h₂₃.pullback := h.chosenPullback.p₂
+
+/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₂`. -/
+def p₂ : h.pullback ⟶ X₂ := h.chosenPullback.p
+
+@[reassoc (attr := simp)]
+lemma p₁₂_p₁ : h.p₁₂ ≫ h₁₂.p₁ = h.p₁ := by simp [p₁₂, hp₁]
+
+@[reassoc (attr := simp)]
+lemma p₁₂_p₂ : h.p₁₂ ≫ h₁₂.p₂ = h.p₂ := by simp [p₁₂, p₂]
+
+@[reassoc (attr := simp)]
+lemma p₂₃_p₂ : h.p₂₃ ≫ h₂₃.p₁ = h.p₂ := by simp [p₂₃, p₂]
+
+@[reassoc (attr := simp)]
+lemma p₂₃_p₃ : h.p₂₃ ≫ h₂₃.p₂ = h.p₃ := by simp [p₂₃, hp₃]
+
+@[reassoc (attr := simp)]
+lemma p₁₃_p₁ : h.p₁₃ ≫ h₁₃.p₁ = h.p₁ := by simp [p₁₃]
+
+@[reassoc (attr := simp)]
+lemma p₁₃_p₃ : h.p₁₃ ≫ h₁₃.p₂ = h.p₃ := by simp [p₁₃]
+
+@[reassoc (attr := simp)]
+lemma w₁ : h.p₁ ≫ f₁ = h.p := by
+  simpa only [← hp₁, Category.assoc, h₁₃.hp₁, h.l.f_p] using h.l.f_p₁.symm =≫ f₁
+
+@[reassoc (attr := simp)]
+lemma w₃ : h.p₃ ≫ f₃ = h.p := by
+  simpa only [← hp₃, Category.assoc, h₁₃.hp₂, h.l.f_p] using h.l.f_p₂.symm =≫ f₃
+
+@[reassoc (attr := simp)]
+lemma w₂ : h.p₂ ≫ f₂ = h.p := by
+  rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc]
+
+@[reassoc (attr := simp)]
+lemma p₁₂_p : h.p₁₂ ≫ h₁₂.p = h.p := by
+  rw [← h₁₂.hp₂, p₁₂_p₂_assoc, w₂]
+
+@[reassoc (attr := simp)]
+lemma p₂₃_p : h.p₂₃ ≫ h₂₃.p = h.p := by
+  rw [← h₂₃.hp₂, p₂₃_p₃_assoc, w₃]
+
+@[reassoc (attr := simp)]
+lemma p₁₃_p : h.p₁₃ ≫ h₁₃.p = h.p := by
+  rw [← h₁₃.hp₁, p₁₃_p₁_assoc, w₁]
+
+lemma p₁₂_eq_lift : h.p₁₂ = h₁₂.isPullback.lift h.p₁ h.p₂ (by simp) := by
+  apply h₁₂.isPullback.hom_ext <;> simp
+
+lemma p₂₃_eq_lift : h.p₂₃ = h₂₃.isPullback.lift h.p₂ h.p₃ (by simp) := by
+  apply h₂₃.isPullback.hom_ext <;> simp
+
+lemma p₁₃_eq_lift : h.p₁₃ = h₁₃.isPullback.lift h.p₁ h.p₃ (by simp) := by
+  apply h₁₃.isPullback.hom_ext <;> simp
+
+lemma exists_lift {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (g₃ : Y ⟶ X₃) (b : Y ⟶ S)
+    (hg₁ : g₁ ≫ f₁ = b) (hg₂ : g₂ ≫ f₂ = b) (hg₃ : g₃ ≫ f₃ = b) :
+    ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃ := by
+  obtain ⟨φ₁₂, w₁, w₂⟩ := h₁₂.isPullback.exists_lift g₁ g₂ (by cat_disch)
+  obtain ⟨φ₂₃, w₂', w₃⟩ := h₂₃.isPullback.exists_lift g₂ g₃ (by cat_disch)
+  obtain ⟨φ, w₁₂, w₂₃⟩ := h.chosenPullback.isPullback.exists_lift φ₁₂ φ₂₃ (by cat_disch)
+  refine ⟨φ, ?_, ?_, ?_⟩
+  · rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁]
+  · rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂]
+  · rw [← w₃, ← w₂₃, Category.assoc, ← p₂₃, p₂₃_p₃]
+
+lemma isPullback₂ : IsPullback h.p₁₂ h.p₂₃ h₁₂.p₂ h₂₃.p₁ := h.chosenPullback.isPullback
+
+lemma hom_ext {Y : C} {φ φ' : Y ⟶ h.pullback}
+    (h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁) (h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂)
+    (h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃) : φ = φ' := by
+  apply h.isPullback₂.hom_ext
+  · apply h₁₂.isPullback.hom_ext <;> simpa
+  · apply h₂₃.isPullback.hom_ext <;> simpa
+
+lemma isPullback₁ : IsPullback h.p₁₂ h.p₁₃ h₁₂.p₁ h₁₃.p₁ :=
+  .mk' (by simp) (fun _ _ _ h₁ h₂ ↦ h.hom_ext (by simpa using h₁ =≫ h₁₂.p₁)
+      (by simpa using h₁ =≫ h₁₂.p₂) (by simpa using h₂ =≫ h₁₃.p₂))
+    (fun _ a b w ↦ by
+      obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ :=
+        h.exists_lift (a ≫ h₁₂.p₁) (a ≫ h₁₂.p₂) (b ≫ h₁₃.p₂) _ rfl
+          (by simp) (by simpa using w.symm =≫ f₁)
+      refine ⟨φ, ?_, ?_⟩
+      · apply h₁₂.isPullback.hom_ext <;> simpa
+      · apply h₁₃.isPullback.hom_ext <;> cat_disch)
+
+lemma isPullback₃ : IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂ :=
+  .mk' (by simp) (fun _ _ _ h₁ h₂ ↦ h.hom_ext (by simpa using h₁ =≫ h₁₃.p₁)
+      (by simpa using h₂ =≫ h₂₃.p₁) (by simpa using h₁ =≫ h₁₃.p₂))
+    (fun _ a b w ↦ by
+      obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ :=
+        h.exists_lift (a ≫ h₁₃.p₁) (b ≫ h₂₃.p₁) (a ≫ h₁₃.p₂) _ rfl
+          (by simpa using w.symm =≫ f₃) (by simp)
+      refine ⟨φ, ?_, ?_⟩
+      · apply h₁₃.isPullback.hom_ext <;> simpa
+      · apply h₂₃.isPullback.hom_ext <;> cat_disch)
+
+end ChosenPullback₃
+
+end CategoryTheory.Limits
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
index d31bfc36f73ccc..8a0bf56663ecc2 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean
@@ -356,6 +356,24 @@ lemma of_isLimit_binaryFan_of_isTerminal
         rfl)⟩
 end
 
+lemma mk' {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
+    (w : fst ≫ f = snd ≫ g)
+    (hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄ (_ : φ ≫ fst = φ' ≫ fst)
+      (_ : φ ≫ snd = φ' ≫ snd), φ = φ')
+    (exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y)
+      (_ : a ≫ f = b ≫ g), ∃ (l : T ⟶ P), l ≫ fst = a ∧ l ≫ snd = b) :
+    IsPullback fst snd f g where
+  w := w
+  isLimit' := by
+    let l (s : PullbackCone f g) := exists_lift _ _ s.condition
+    exact ⟨PullbackCone.IsLimit.mk _
+      (fun s ↦ (l s).choose)
+      (fun s ↦ (l s).choose_spec.1)
+      (fun s ↦ (l s).choose_spec.2)
+      (fun s m h₁ h₂ ↦ hom_ext
+        (h₁.trans (l s).choose_spec.1.symm)
+        (h₂.trans (l s).choose_spec.2.symm))⟩
+
 end IsPullback
 namespace IsPushout
 
diff --git a/Mathlib/CategoryTheory/Sites/Descent/DescentDataPrime.lean b/Mathlib/CategoryTheory/Sites/Descent/DescentDataPrime.lean
new file mode 100644
index 00000000000000..96ff616744858a
--- /dev/null
+++ b/Mathlib/CategoryTheory/Sites/Descent/DescentDataPrime.lean
@@ -0,0 +1,275 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Christian Merten
+-/
+module
+
+public import Mathlib.CategoryTheory.Sites.Descent.DescentData
+public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
+
+/-!
+# Descent data when we have pullbacks
+
+In this file, given a pseudofunctor `F` from `LocallyDiscrete Cᵒᵖ` to `Cat`,
+a family of maps `f i : X i ⟶ S` in the category `C`, chosen pullbacks `sq`
+and threefold wide pullbacks `sq₃` for these morphisms, we define a
+category `F.DescentData' sq sq₃` of objects over the `X i`
+equipped with a descent data relative to the morphisms `f i : X i ⟶ S`, where
+the data and compatibilities are expressed using the chosen pullbacks.
+
+## TODO
+* show that this category is equivalent to `F.DescentData f`.
+
+-/
+
+@[expose] public section
+
+universe t v' v u' u
+
+namespace CategoryTheory
+
+open Opposite Limits
+
+namespace Pseudofunctor
+
+open LocallyDiscreteOpToCat
+
+variable {C : Type u} [Category.{v} C] (F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v', u'})
+  {ι : Type t} {S : C} {X : ι → C} {f : ∀ i, X i ⟶ S}
+  (sq : ∀ i j, ChosenPullback (f i) (f j))
+  (sq₃ : ∀ (i₁ i₂ i₃ : ι), ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
+
+namespace DescentData'
+
+variable {F sq}
+
+section
+
+variable {obj obj' : ∀ (i : ι), F.obj (.mk (op (X i)))}
+  (hom : ∀ (i j : ι), (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶
+    (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
+
+/-- Variant of `Pseudofunctor.LocallyDiscreteOpToCat.pullHom` when we have
+chosen pullbacks. -/
+noncomputable def pullHom' ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
+    (hf₁ : f₁ ≫ f i₁ = q := by cat_disch) (hf₂ : f₂ ≫ f i₂ = q := by cat_disch) :
+    (F.map f₁.op.toLoc).toFunctor.obj (obj i₁) ⟶ (F.map f₂.op.toLoc).toFunctor.obj (obj' i₂) :=
+  pullHom (hom i₁ i₂) ((sq i₁ i₂).isPullback.lift f₁ f₂ (by cat_disch)) f₁ f₂
+
+@[reassoc]
+lemma pullHom'_eq_pullHom ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
+    (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q) (p : Y ⟶ (sq i₁ i₂).pullback)
+    (hp₁ : p ≫ (sq i₁ i₂).p₁ = f₁) (hp₂ : p ≫ (sq i₁ i₂).p₂ = f₂) :
+  pullHom' hom q f₁ f₂ hf₁ hf₂ =
+    pullHom (hom i₁ i₂) p f₁ f₂ := by
+  obtain rfl : p = (sq i₁ i₂).isPullback.lift f₁ f₂ (by rw [hf₁, hf₂]) := by
+    apply (sq i₁ i₂).isPullback.hom_ext <;> cat_disch
+  rfl
+
+@[reassoc]
+lemma pullHom'₁₂_eq_pullHom_of_chosenPullback₃ (i₁ i₂ i₃ : ι) :
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ =
+      pullHom (hom i₁ i₂) (sq₃ i₁ i₂ i₃).p₁₂ _ _ :=
+  pullHom'_eq_pullHom _ _ _ _ _ _ _ (by simp) (by simp)
+
+@[reassoc]
+lemma pullHom'₁₃_eq_pullHom_of_chosenPullback₃ (i₁ i₂ i₃ : ι) :
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ =
+      pullHom (hom i₁ i₃) (sq₃ i₁ i₂ i₃).p₁₃ _ _ :=
+  pullHom'_eq_pullHom _ _ _ _ _ _ _ (by simp) (by simp)
+
+@[reassoc]
+lemma pullHom'₂₃_eq_pullHom_of_chosenPullback₃ (i₁ i₂ i₃ : ι) :
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ =
+      pullHom (hom i₂ i₃) (sq₃ i₁ i₂ i₃).p₂₃ _ _ :=
+  pullHom'_eq_pullHom _ _ _ _ _ _ _ (by simp) (by simp)
+
+@[reassoc]
+  lemma pullHom_pullHom' ⦃Y Y' : C⦄ (g : Y' ⟶ Y) (q : Y ⟶ S) (q' : Y' ⟶ S) (hq : g ≫ q = q')
+    ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q)
+    (gf₁ : Y' ⟶ X i₁) (gf₂ : Y' ⟶ X i₂) (hgf₁ : g ≫ f₁ = gf₁) (hgf₂ : g ≫ f₂ = gf₂) :
+    pullHom (pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ =
+      pullHom' hom q' gf₁ gf₂ := by
+  let p := (sq i₁ i₂).isPullback.lift f₁ f₂ (by cat_disch)
+  rw [pullHom'_eq_pullHom _ _ _ _ _ _ p (by cat_disch) (by cat_disch),
+    pullHom'_eq_pullHom _ _ _ _ _ _ (g ≫ p) (by cat_disch) (by cat_disch)]
+  dsimp [pullHom]
+  simp only [Functor.map_comp, Category.assoc]
+  rw [F.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc
+    _ _ _ _ _ _ (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst]) rfl
+    (by cat_disch),
+    F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app _ _ _ _ _ _
+      (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]) rfl (by cat_disch)]
+  simp
+
+end
+
+
+section
+
+variable {obj : ∀ (i : ι), F.obj (.mk (op (X i)))}
+  (hom : ∀ (i j : ι), (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶
+    (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j))
+
+@[simp]
+lemma pullHom'_p₁_p₂ (i₁ i₂ : ι) :
+    pullHom' hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ (by simp) (by simp) = hom i₁ i₂ := by
+  rw [pullHom'_eq_pullHom hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ (by simp) (by simp)
+    (𝟙 _) (by simp)  (by simp)]
+  simp [pullHom, mapComp'_comp_id_hom_app, mapComp'_comp_id_inv_app]
+
+lemma pullHom'_self' (hom_self : ∀ i, pullHom' hom (f i) (𝟙 (X i)) (𝟙 (X i)) = 𝟙 _)
+    ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (hg : g ≫ f i = q) :
+    pullHom' hom q g g hg hg = 𝟙 _ := by
+  simp [← pullHom_pullHom' hom g (f i) q hg (𝟙 (X i)) (𝟙 (X i)) (by simp) (by simp) g g
+    (by simp) (by simp), hom_self, pullHom]
+
+variable {sq₃} in
+@[reassoc]
+lemma comp_pullHom'' (hom_comp : ∀ (i₁ i₂ i₃ : ι),
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ≫
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ =
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃)
+    ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁)
+    (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃) (hf₁ : f₁ ≫ f i₁ = q)
+    (hf₂ : f₂ ≫ f i₂ = q) (hf₃ : f₃ ≫ f i₃ = q) :
+    pullHom' hom q f₁ f₂ ≫ pullHom' hom q f₂ f₃ = pullHom' hom q f₁ f₃ := by
+  obtain ⟨φ, _, _, _⟩ := (sq₃ i₁ i₂ i₃).exists_lift f₁ f₂ f₃ q hf₁ hf₂ hf₃
+  rw [← pullHom_pullHom'_assoc hom φ (sq₃ i₁ i₂ i₃).p _ _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂,
+    pullHom, Category.assoc, Category.assoc,
+    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ _ (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃,
+    ← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ _ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃,
+    pullHom, pullHom]
+  · dsimp
+    simp [← Functor.map_comp_assoc, hom_comp]
+  all_goals cat_disch
+
+end
+
+end DescentData'
+
+open DescentData' in
+/-- Given a pseudofunctor `F` from `LocallyDiscrete Cᵒᵖ` to `Cat`, a family of
+morphisms `f i : X i ⟶ S`, chosen pullbacks `sq i j` of `f i` and `f j` for all `i` and `j`,
+and chosen threefold wide pullbacks `sq₃`, this structure contains a description
+of objects over the `X i` equipped with a descent data relative to the morphisms `f i`,
+where the (iso)morphisms are compatibilities are considered over the chosen pullbacks. -/
+structure DescentData' where
+  /-- The objects over `X i` for all `i` -/
+  obj (i : ι) : F.obj (.mk (op (X i)))
+  /-- The compatibility morphisms after pulling back to the chosen pullback. It follows
+  from the conditions `pullHom'_hom_self` and `pullHom'_hom_comp` that these morphisms
+  are isomorphisms. -/
+  hom : ∀ (i j : ι), (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶
+    (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
+  pullHom'_hom_self : ∀ i, pullHom' hom (f i) (𝟙 (X i)) (𝟙 (X i)) = 𝟙 _
+  pullHom'_hom_comp (i₁ i₂ i₃ : ι) :
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ≫
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ =
+    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃
+
+namespace DescentData'
+
+variable {F sq sq₃}
+
+@[simp]
+lemma pullHom'_self (D : F.DescentData' sq sq₃)
+    ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i) (hg : g ≫ f i = q) :
+    pullHom' D.hom q g g hg hg = 𝟙 _ :=
+  pullHom'_self' _ D.pullHom'_hom_self _ _ _
+
+@[reassoc (attr := simp)]
+lemma comp_pullHom' (D : F.DescentData' sq sq₃)
+    ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁)
+    (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃) (hf₁ : f₁ ≫ f i₁ = q)
+    (hf₂ : f₂ ≫ f i₂ = q) (hf₃ : f₃ ≫ f i₃ = q) :
+    pullHom' D.hom q f₁ f₂ hf₁ hf₂ ≫ pullHom' D.hom q f₂ f₃ hf₂ hf₃ =
+      pullHom' D.hom q f₁ f₃ hf₁ hf₃ :=
+  comp_pullHom'' _ D.pullHom'_hom_comp _ _ _ _ hf₁ hf₂ hf₃
+
+instance (D : F.DescentData' sq sq₃)
+    {Y : C} (q : Y ⟶ S) (i₁ i₂ : ι) (f₁ : Y ⟶ X i₁)
+    (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q)
+    (hf₂ : f₂ ≫ f i₂ = q) :
+    IsIso (pullHom' D.hom q f₁ f₂ hf₁ hf₂) :=
+  ⟨pullHom' D.hom q f₂ f₁ hf₂ hf₁, by simp, by simp⟩
+
+lemma pullHom'_eq_hom (D : F.DescentData' sq sq₃) (i₁ i₂ : ι) :
+    pullHom' D.hom _ _ _ (by simp) = D.hom i₁ i₂ := by
+  simp
+
+instance (D : F.DescentData' sq sq₃) (i₁ i₂ : ι) :
+    IsIso (D.hom i₁ i₂) := by
+  simpa using inferInstanceAs (IsIso (pullHom' D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂))
+
+/-- The type of morphisms in the category `F.DescentData' sq sq₃`. -/
+@[ext]
+structure Hom (D₁ D₂ : F.DescentData' sq sq₃) where
+  /-- The morphisms between the `obj` fields of descent data. -/
+  hom (i : ι) : D₁.obj i ⟶ D₂.obj i
+  comm (i₁ i₂ : ι) :
+    (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom i₁) ≫ D₂.hom i₁ i₂  =
+    D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom i₂) := by cat_disch
+
+attribute [reassoc (attr := simp)] Hom.comm
+
+instance : Category (F.DescentData' sq sq₃) where
+  Hom := Hom
+  id _ := { hom _ := 𝟙 _ }
+  comp f g := { hom i := f.hom i ≫ g.hom i }
+
+@[ext]
+lemma hom_ext {D₁ D₂ : F.DescentData' sq sq₃} {f g : D₁ ⟶ D₂}
+    (h : ∀ i, f.hom i = g.hom i) : f = g :=
+  Hom.ext (funext h)
+
+@[simp]
+lemma id_hom (D : F.DescentData' sq sq₃) (i : ι) :
+    Hom.hom (𝟙 D) i = 𝟙 _ :=
+  rfl
+
+@[reassoc, simp]
+lemma comp_hom {D₁ D₂ D₃ : F.DescentData' sq sq₃} (f : D₁ ⟶ D₂) (g : D₂ ⟶ D₃) (i : ι) :
+    (f ≫ g).hom i = f.hom i ≫ g.hom i :=
+  rfl
+
+@[reassoc]
+lemma comm {D₁ D₂ : F.DescentData' sq sq₃} (φ : D₁ ⟶ D₂)
+    ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁)
+    (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q) :
+    (F.map f₁.op.toLoc).toFunctor.map (φ.hom i₁) ≫ pullHom' D₂.hom q f₁ f₂ hf₁ hf₂ =
+      pullHom' D₁.hom q f₁ f₂ hf₁ hf₂ ≫ (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂) := by
+  obtain ⟨p, _, _⟩  := (sq i₁ i₂).isPullback.exists_lift f₁ f₂ (by cat_disch)
+  rw [← pullHom_pullHom' D₂.hom p (sq i₁ i₂).p q (by cat_disch) (sq i₁ i₂).p₁ (sq i₁ i₂).p₂
+    (by simp) (by simp) f₁ f₂ (by cat_disch) (by cat_disch),
+    ← pullHom_pullHom' D₁.hom p (sq i₁ i₂).p q (by cat_disch) (sq i₁ i₂).p₁ (sq i₁ i₂).p₂
+      (by simp) (by simp) f₁ f₂ (by cat_disch) (by cat_disch), pullHom'_p₁_p₂, pullHom'_p₁_p₂]
+  dsimp only [pullHom]
+  rw [NatTrans.naturality_assoc]
+  dsimp
+  rw [← Functor.map_comp_assoc, φ.comm, Functor.map_comp_assoc, mapComp'_inv_naturality]
+  simp only [Category.assoc]
+
+/-- Constructor for isomorphisms in the category `F.DescentData' sq sq₃`. -/
+@[simps]
+def isoMk {D₁ D₂ : F.DescentData' sq sq₃} (e : ∀ (i : ι), D₁.obj i ≅ D₂.obj i)
+    (comm : ∀ (i₁ i₂ : ι), (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom i₁ i₂ =
+    D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom := by cat_disch) :
+    D₁ ≅ D₂ where
+  hom :=
+    { hom i := (e i).hom
+      comm := comm }
+  inv :=
+    { hom i := (e i).inv
+      comm i₁ i₂ := by
+        rw [← cancel_mono ((F.map _).toFunctor.map (e i₂).hom), Category.assoc,
+          Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
+          ← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),
+          Iso.map_hom_inv_id_assoc, comm i₁ i₂] }
+
+end DescentData'
+
+end Pseudofunctor
+
+end CategoryTheory