feat(CategoryTheory/Sites): functoriality of descent data (leanprover-community#30190)

Given a pseudofunctor `F` from `LocallyDiscrete Cᵒᵖ` to `Cat`, we show that up to an equivalence, the category `F.DescentData f` is unchanged when we replace `S` by an isomorphic object, or the family `f i : X i ⟶ S` by another family which generates the same sieve (see `Pseudofunctor.DescentData.pullFunctorEquivalence`).

Co-authored-by: Christian Merten [christian@merten.dev](mailto:christian@merten.dev)

Author: joelriou

Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

@@ -5,6 +5,7 @@ Authors: Yuma Mizuno, Calle Sönne
 -/
 module
 
+public import Mathlib.CategoryTheory.CommSq
 public import Mathlib.CategoryTheory.Discrete.Basic
 public import Mathlib.CategoryTheory.Bicategory.Strict.Basic
 
@@ -156,4 +157,10 @@ lemma CategoryTheory.LocallyDiscrete.eqToHom_toLoc {C : Type u} [Category.{v} C]
     (h : a = b) : (eqToHom h).toLoc = eqToHom (congrArg LocallyDiscrete.mk h) := by
   subst h; rfl
 
+lemma CategoryTheory.CommSq.toLoc {C : Type*} [Category C] {X₁ X₂ X₃ X₄ : C}
+    {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄}
+    (h : CommSq t l r b) :
+    CommSq t.toLoc l.toLoc r.toLoc b.toLoc :=
+  ⟨by simp only [← Quiver.Hom.comp_toLoc, h.w]⟩
+
 end

Mathlib/CategoryTheory/Category/Cat.lean

@@ -180,6 +180,34 @@ lemma isoMk_toNatIso {X Y : Cat.{v, u}} {F G : X ⟶ Y} (e : F ≅ G) :
 lemma toNatIso_isoMk {C D : Type u} [Category.{v} C] [Category.{v} D] {F G : C ⥤ D} (e : F ≅ G) :
     Hom.toNatIso (isoMk e) = e := rfl
 
+instance {X Y : Cat.{v, u}} {F G : X ⟶ Y} (e : F ≅ G) :
+    IsIso e.hom.toNatTrans :=
+  (toNatIso e).isIso_hom
+
+instance {X Y : Cat.{v, u}} {F G : X ⟶ Y} (e : F ≅ G) :
+    IsIso e.inv.toNatTrans :=
+  (toNatIso e).isIso_inv
+
+@[reassoc (attr := simp)]
+lemma hom_inv_id_toNatTrans {X Y : Cat.{v, u}} {F G : X ⟶ Y} (e : F ≅ G) :
+    e.hom.toNatTrans ≫ e.inv.toNatTrans = 𝟙 _ :=
+  (toNatIso e).hom_inv_id
+
+@[reassoc (attr := simp)]
+lemma inv_hom_id_toNatTrans {X Y : Cat.{v, u}} {F G : X ⟶ Y} (e : F ≅ G) :
+    e.inv.toNatTrans ≫ e.hom.toNatTrans = 𝟙 _ :=
+  (toNatIso e).inv_hom_id
+
+@[reassoc (attr := simp)]
+lemma hom_inv_id_toNatTrans_app {X Y : Cat.{v, u}} {F G : X ⟶ Y} (e : F ≅ G) (A : X) :
+    e.hom.toNatTrans.app A ≫ e.inv.toNatTrans.app A = 𝟙 _ :=
+  (toNatIso e).hom_inv_id_app A
+
+@[reassoc (attr := simp)]
+lemma inv_hom_id_toNatTrans_app {X Y : Cat.{v, u}} {F G : X ⟶ Y} (e : F ≅ G) (A : X) :
+    e.inv.toNatTrans.app A ≫ e.hom.toNatTrans.app A = 𝟙 _ :=
+  (toNatIso e).inv_hom_id_app A
+
 end Hom
 
 end

Mathlib/CategoryTheory/Sites/Descent/DescentData.lean

@@ -15,6 +15,11 @@ and a family of maps `f i : X i ⟶ S` in the category `C`,
 we define the category `F.DescentData f` of objects over the `X i`
 equipped with a descent data relative to the morphisms `f i : X i ⟶ S`.
 
+We show that up to an equivalence, the category `F.DescentData f` is unchanged
+when we replace `S` by an isomorphic object, or the family `f i : X i ⟶ S`
+by another family which generates the same sieve
+(see `Pseudofunctor.DescentData.pullFunctorEquivalence`).
+
 ## TODO (@joelriou, @chrisflav)
 * Relate the prestack condition to the fully faithfullness of `Pseudofunctor.toDescentData`.
 * Define stacks.
@@ -25,7 +30,7 @@ when `F` also has a covariant functoriality, etc.).
 
 @[expose] public section
 
-universe t v' v u' u
+universe t t' t'' v' v u' u
 
 namespace CategoryTheory
 
@@ -129,11 +134,6 @@ def ofObj (M : F.obj (.mk (op S))) : F.DescentData f where
         gf₁.op.toLoc q'.op.toLoc (by grind) (by grind) (by grind),
       F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app (f i₂).op.toLoc f₂.op.toLoc g.op.toLoc
       q.op.toLoc gf₂.op.toLoc q'.op.toLoc (by grind) (by grind) (by grind)]
-  hom_self Y q i g h := by
-    simp [← Cat.Hom₂.comp_app]
-  hom_comp Y q i₁ i₂ i₃ f₁ f₂ f₃ hf₁ hf₂ hf₃ := by
-    simp only [← Cat.Hom₂.comp_app]
-    simp
 
 /-- Constructor for isomorphisms in `Pseudofunctor.DescentData`. -/
 @[simps]
@@ -143,8 +143,7 @@ def isoMk {D₁ D₂ : F.DescentData f} (e : ∀ (i : ι), D₁.obj i ≅ D₂.o
     (F.map f₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom q f₁ f₂ =
       D₁.hom q f₁ f₂ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom := by cat_disch) : D₁ ≅ D₂ where
   hom :=
-    { hom i := (e i).hom
-      comm := comm }
+    { hom i := (e i).hom }
   inv :=
     { hom i := (e i).inv
       comm Y q i₁ i₂ f₁ f₂ hf₁ hf₂ := by
@@ -156,10 +155,232 @@ def isoMk {D₁ D₂ : F.DescentData f} (e : ∀ (i : ι), D₁.obj i ≅ D₂.o
 end DescentData
 
 /-- The functor `F.obj (.mk (op S)) ⥤ F.DescentData f`. -/
+@[simps]
 def toDescentData : F.obj (.mk (op S)) ⥤ F.DescentData f where
   obj M := .ofObj M
   map {M M'} φ := { hom i := (F.map (f i).op.toLoc).toFunctor.map φ }
 
+namespace DescentData
+
+section
+
+variable {F f} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : ∀ j, X' j ⟶ S'}
+  {α : ι' → ι} {p' : ∀ j, X' j ⟶ X (α j)} (w : ∀ j, p' j ≫ f (α j) = f' j ≫ p)
+
+/-- Auxiliary definition for `pullFunctor`. -/
+def pullFunctorObjHom (D : F.DescentData f)
+    ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂)
+    (hf₁ : f₁ ≫ f' j₁ = q := by cat_disch) (hf₂ : f₂ ≫ f' j₂ = q := by cat_disch) :
+    (F.map f₁.op.toLoc).toFunctor.obj ((F.map (p' j₁).op.toLoc).toFunctor.obj (D.obj (α j₁))) ⟶
+      (F.map f₂.op.toLoc).toFunctor.obj ((F.map (p' j₂).op.toLoc).toFunctor.obj (D.obj (α j₂))) :=
+  (F.mapComp (p' j₁).op.toLoc f₁.op.toLoc).inv.toNatTrans.app _ ≫
+    D.hom (q ≫ p) (f₁ ≫ p' _) (f₂ ≫ p' _) (by simp [w, reassoc_of% hf₁])
+      (by simp [w, reassoc_of% hf₂]) ≫
+    (F.mapComp (p' j₂).op.toLoc f₂.op.toLoc).hom.toNatTrans.app _
+
+@[reassoc]
+lemma pullFunctorObjHom_eq (D : F.DescentData f)
+    ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂)
+    (q' : Y ⟶ S) (f₁' : Y ⟶ X (α j₁)) (f₂' : Y ⟶ X (α j₂))
+    (hf₁ : f₁ ≫ f' j₁ = q := by cat_disch) (hf₂ : f₂ ≫ f' j₂ = q := by cat_disch)
+    (hq' : q ≫ p = q' := by cat_disch)
+    (hf₁' : f₁ ≫ p' j₁ = f₁' := by cat_disch)
+    (hf₂' : f₂ ≫ p' j₂ = f₂' := by cat_disch) :
+  pullFunctorObjHom w D q f₁ f₂ =
+    (F.mapComp' _ _ _).inv.toNatTrans.app _ ≫ D.hom q' f₁' f₂'
+      (by rw [← hq', ← hf₁', Category.assoc, w, reassoc_of% hf₁])
+      (by rw [← hq', ← hf₂', Category.assoc, w, reassoc_of% hf₂]) ≫
+      (F.mapComp' _ _ _).hom.toNatTrans.app _ := by
+  subst hq' hf₁' hf₂'
+  simp [mapComp'_eq_mapComp, pullFunctorObjHom]
+
+/-- Auxiliary definition for `pullFunctor`. -/
+@[simps]
+def pullFunctorObj (D : F.DescentData f) :
+    F.DescentData f' where
+  obj j := (F.map (p' _).op.toLoc).toFunctor.obj (D.obj (α j))
+  hom Y q j₁ j₂ f₁ f₂ hf₁ hf₂ := pullFunctorObjHom w _ _ _ _
+  pullHom_hom Y' Y g q q' hq j₁ j₂ f₁ f₂ hf₁ hf₂ gf₁ gf₂ hgf₁ hgf₂ := by
+    rw [pullFunctorObjHom_eq _ _ _ _ _ (q' ≫ p) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂),
+      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)]
+    rw [← D.pullHom_hom g (q ≫ p) (q' ≫ p) (by rw [reassoc_of% hq])
+      (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) (by rw [Category.assoc, w, reassoc_of% hf₁])
+      (by rw [Category.assoc, w, reassoc_of% hf₂]) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂)
+      (by cat_disch) (by cat_disch)]
+    dsimp [pullHom]
+    simp only [Functor.map_comp, Category.assoc]
+    rw [F.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc _ _ _ _ _ _ _ _ (by cat_disch),
+      mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app _ _ _ _ _ _ _ _ _ (by cat_disch)]
+  hom_self Y q j g hg := by
+    rw [pullFunctorObjHom_eq _ _ _ _ _ _ _ _ rfl rfl rfl rfl rfl,
+      D.hom_self _ _ (by cat_disch)]
+    simp
+  hom_comp Y q j₁ j₂ j₃ f₁ f₂ f₃ hf₁ hf₂ hf₃ := by
+    rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂),
+      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₂ ≫ p' j₂) (f₃ ≫ p' j₃),
+      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₃ ≫ p' j₃)]
+    simp
+
+variable (F)
+
+/-- Given family of morphisms `f : X i ⟶ S` and `f' : X' j ⟶ S'`, and suitable
+commutative diagrams `p' j ≫ f (α j) = f' j ≫ p`, this is the
+induced functor `F.DescentData f ⥤ F.DescentData f'`. (Up to a (unique) isomorphism,
+this functor only depends on `f` and `f'`, see `pullFunctorIso`.) -/
+@[simps]
+def pullFunctor : F.DescentData f ⥤ F.DescentData f' where
+  obj D := pullFunctorObj w D
+  map {D₁ D₂} φ :=
+    { hom j := (F.map (p' j).op.toLoc).toFunctor.map (φ.hom (α j))
+      comm Y q j₁ j₂ f₁ f₂ hf₁ hf₂ := by
+        have := φ.comm (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)
+          (by rw [Category.assoc, w, reassoc_of% hf₁])
+          (by rw [Category.assoc, w, reassoc_of% hf₂])
+        dsimp at this ⊢
+        rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂),
+          pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)]
+        dsimp
+        rw [mapComp'_inv_naturality_assoc, ← mapComp'_hom_naturality,
+          reassoc_of% this] }
+
+/-- Given families of morphisms `f : X i ⟶ S` and `f' : X' j ⟶ S'`, suitable
+commutative diagrams `w j : p' j ≫ f (α j) = f' j ≫ p`, this is the natural
+isomorphism between the descent data relative to `f'` that are obtained either:
+* by considering the obvious descent data relative to `f` given by an object `M : F.obj (op S)`,
+followed by the application of `pullFunctor F w : F.DescentData f ⥤ F.DescentData f'`;
+* by considering the obvious descent data relative to `f'` given by pulling
+back the object `M` to `S'`. -/
+def toDescentDataCompPullFunctorIso :
+    F.toDescentData f ⋙ pullFunctor F w ≅ (F.map p.op.toLoc).toFunctor ⋙ F.toDescentData f' :=
+  NatIso.ofComponents
+    (fun M ↦ isoMk (fun i ↦ (Cat.Hom.toNatIso
+        (F.isoMapOfCommSq (CommSq.mk (w i)).op.toLoc)).symm.app M)
+      (fun Y q i₁ i₂ f₁ f₂ hf₁ hf₂ ↦ by
+        dsimp
+        rw [F.isoMapOfCommSq_eq _ _  rfl, F.isoMapOfCommSq_eq _ _  rfl]
+        dsimp
+        simp only [Functor.map_comp, Category.assoc]
+        rw [← F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc p.op.toLoc
+            (f' i₁).op.toLoc f₁.op.toLoc _ q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) rfl
+            (by grind) (by grind) M,
+          pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' i₁) (f₂ ≫ p' i₂),
+          ← cancel_mono ((F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc
+            (by grind)).inv.toNatTrans.app _)]
+        dsimp
+        simp only [Category.assoc,
+          ← F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app p.op.toLoc
+            (f' i₂).op.toLoc f₂.op.toLoc _ q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) rfl
+            (by grind) (by grind) M,
+          ← F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc (f (α i₁)).op.toLoc
+            (p' i₁).op.toLoc f₁.op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) _
+            (p.op.toLoc ≫ q.op.toLoc) (by grind) rfl (by grind) M,
+          F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc (f (α i₂)).op.toLoc
+            (p' i₂).op.toLoc f₂.op.toLoc (p.op.toLoc ≫ (f' i₂).op.toLoc) _
+            (p.op.toLoc ≫ q.op.toLoc) (by grind) rfl (by grind) M]
+        simp))
+    (fun f ↦ by
+      ext i
+      exact (F.isoMapOfCommSq (CommSq.mk (w i)).op.toLoc).inv.toNatTrans.naturality f)
+
+/-- Up to a (unique) isomorphism, the functor
+`pullFunctor : F.DescentData f ⥤ F.DescentData f'` does not depend
+on the auxiliary data. -/
+@[simps!]
+def pullFunctorIso {β : ι' → ι} {p'' : ∀ j, X' j ⟶ X (β j)}
+    (w' : ∀ j, p'' j ≫ f (β j) = f' j ≫ p) :
+    pullFunctor F w ≅ pullFunctor F w' :=
+  NatIso.ofComponents (fun D ↦ isoMk (fun j ↦ D.iso _ _ _) (by
+    intro Y q j₁ j₂ f₁ f₂ hf₁ hf₂
+    dsimp
+    rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
+      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
+      map_eq_pullHom_assoc _ _ (f₁ ≫ p' j₁) (f₁ ≫ p'' j₁) (by cat_disch) (by cat_disch),
+      map_eq_pullHom _ _ (f₂ ≫ p' j₂) (f₂ ≫ p'' j₂) (by cat_disch) (by cat_disch)]
+    simp only [Cat.Hom.hom_inv_id_toNatTrans_app_assoc, Category.assoc]
+    rw [pullHom_hom _ _ _ (q ≫ p) (by rw [w, reassoc_of% hf₁]) _ _
+        rfl (by cat_disch) _ _ rfl rfl, hom_comp_assoc,
+      pullHom_hom _ _ _ (q ≫ p) (by rw [w, reassoc_of% hf₂]) _ _
+        rfl (by cat_disch) _ _ rfl rfl, hom_comp_assoc]))
+    (fun φ ↦ by
+      ext j
+      exact φ.comm _ _ _ rfl (by cat_disch))
+
+variable (S) in
+/-- The functor `F.DescentData f ⥤ F.DescentData f` corresponding to `pullFunctor`
+applied to identity morphisms is isomorphic to the identity functor. -/
+@[simps!]
+def pullFunctorIdIso :
+    pullFunctor F (p := 𝟙 S) (p' := fun _ ↦ 𝟙 _) (w := by simp) ≅ 𝟭 (F.DescentData f) :=
+  NatIso.ofComponents (fun D ↦ isoMk (fun i ↦ (Cat.Hom.toNatIso (F.mapId _)).app _) (by
+    intro Y q i₁ i₂ f₁ f₂ hf₁ hf₂
+    dsimp
+    rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ q f₁ f₂ rfl]
+    simp [mapComp'_id_comp_inv_app_assoc, mapComp'_id_comp_hom_app, ← Functor.map_comp]))
+
+/-- The composition of two functors `pullFunctor` is isomorphic to `pullFunctor` applied
+to the compositions. -/
+@[simps!]
+def pullFunctorCompIso
+    {S'' : C} {q : S'' ⟶ S'} {ι'' : Type t''} {X'' : ι'' → C} {f'' : ∀ k, X'' k ⟶ S''}
+    {β : ι'' → ι'} {q' : ∀ k, X'' k ⟶ X' (β k)} (w' : ∀ k, q' k ≫ f' (β k) = f'' k ≫ q)
+    (r : S'' ⟶ S) {r' : ∀ k, X'' k ⟶ X (α (β k))}
+    (hr : q ≫ p = r := by cat_disch) (hr' : ∀ k, q' k ≫ p' (β k) = r' k := by cat_disch) :
+    pullFunctor F w ⋙ pullFunctor F w' ≅
+      pullFunctor F (p := r) (α := α ∘ β) (p' := r') (fun k ↦ by
+        dsimp
+        rw [← hr', Category.assoc, w, reassoc_of% w', hr]) :=
+  NatIso.ofComponents
+    (fun D ↦ isoMk (fun _ ↦ (Cat.Hom.toNatIso (F.mapComp' _ _ _ (by grind))).symm.app _) (by
+      intro Y s k₁ k₂ f₁ f₂ hf₁ hf₂
+      dsimp
+      rw [pullFunctorObjHom_eq _ _ _ _ _  (s ≫ r) _ _ rfl,
+        pullFunctorObjHom_eq _ _ _ _ _ (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂)]
+      dsimp
+      rw [pullFunctorObjHom_eq _ _ _ _ _ (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂)
+        rfl (by simp [w', reassoc_of% hf₁, reassoc_of% hf₂]) (by
+          simp [reassoc_of% w', reassoc_of% hf₁, hr])]
+      dsimp
+      simp only [Category.assoc]
+      rw [mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc _ _ _ _ _ _ _
+        (by grind) rfl rfl, mapComp'₀₂₃_hom_app _ _ _ _ _ _ _ _ rfl rfl]))
+
+end
+
+variable {f} in
+/-- Up to an equivalence, the category `DescentData` for a pseudofunctor `F` and
+a family of morphisms `f : X i ⟶ S` is unchanged when we replace `S` by an isomorphic object,
+or when we replace `f` by another family which generate the same sieve. -/
+@[simps]
+def pullFunctorEquivalence {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : ∀ j, X' j ⟶ S'}
+    (e : S' ≅ S) {α : ι' → ι} {p' : ∀ j, X' j ⟶ X (α j)}
+    (w : ∀ j, p' j ≫ f (α j) = f' j ≫ e.hom)
+    {β : ι → ι'} {q' : ∀ i, X i ⟶ X' (β i)} (w' : ∀ i, q' i ≫ f' (β i) = f i ≫ e.inv) :
+    F.DescentData f ≌ F.DescentData f' where
+  functor := pullFunctor F w
+  inverse := pullFunctor F w'
+  unitIso :=
+    (pullFunctorIdIso F S).symm ≪≫ pullFunctorIso _ _ _ ≪≫
+      (pullFunctorCompIso _ _ _ _ e.inv_hom_id (fun _ ↦ rfl)).symm
+  counitIso :=
+    pullFunctorCompIso _ _ _ _ e.hom_inv_id (fun _ ↦ rfl) ≪≫
+      pullFunctorIso _ _ _ ≪≫ pullFunctorIdIso F S'
+  functor_unitIso_comp D := by
+    ext j
+    dsimp
+    simp only [Category.id_comp, Functor.map_comp, Category.assoc]
+    rw [pullFunctorObjHom_eq_assoc _ _ _ _ _  (p' _ ≫ f _) (p' _ ≫ q' _ ≫ p' _) (p' _) (by simp)
+        (by simp [w', reassoc_of% w]),
+      map_eq_pullHom_assoc _ (p' j) (p' j) (p' _ ≫ q' _ ≫ p' _) (by simp) (by simp),
+      D.pullHom_hom _ _ (p' j ≫ f _) (by simp) _ _ (by simp)
+        (by simp [w, reassoc_of% w']) _ _ (by simp) rfl]
+    dsimp
+    rw [← F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc _ _ _ _ _ _ rfl rfl (by simp),
+      mapComp'_comp_id_hom_app, mapComp'_id_comp_inv_app_assoc, ← Functor.map_comp_assoc,
+      Cat.Hom.inv_hom_id_toNatTrans_app]
+    simp [D.hom_self _ _ rfl]
+
+end DescentData
+
 end Pseudofunctor
 
 end CategoryTheory