feat: port CategoryTheory.Sites.SheafOfTypes (#3223)

Co-authored-by: Scott Morrison <scott@tqft.net>

Author: joelriou

Mathlib.lean

@@ -489,6 +489,7 @@ import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.SingleObj
 import Mathlib.CategoryTheory.Sites.Grothendieck
 import Mathlib.CategoryTheory.Sites.Pretopology
+import Mathlib.CategoryTheory.Sites.SheafOfTypes
 import Mathlib.CategoryTheory.Sites.Sieves
 import Mathlib.CategoryTheory.Sites.Spaces
 import Mathlib.CategoryTheory.Skeletal

Mathlib/CategoryTheory/Adjunction/Evaluation.lean

@@ -67,7 +67,7 @@ def evaluationAdjunctionRight (c : C) : evaluationLeftAdjoint D c ⊣ (evaluatio
             ext x
             dsimp
             ext ⟨g⟩
-            simp only [colimit.ι_desc, Cofan.mk_ι, Category.assoc, ←f.naturality,
+            simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ←f.naturality,
               evaluationLeftAdjoint_obj_map, colimit.ι_desc_assoc,
               Discrete.functor_obj, Cofan.mk_pt, Discrete.natTrans_app, Category.id_comp]
           right_inv := fun f => by
@@ -131,7 +131,7 @@ def evaluationAdjunctionLeft (c : C) : (evaluation _ _).obj c ⊣ evaluationRigh
             ext ⟨g⟩
             simp only [Discrete.functor_obj, NatTrans.naturality_assoc,
               evaluationRightAdjoint_obj_obj, evaluationRightAdjoint_obj_map, limit.lift_π,
-              Fan.mk_pt, Fan.mk_π, Discrete.natTrans_app, Category.comp_id] } }
+              Fan.mk_pt, Fan.mk_π_app, Discrete.natTrans_app, Category.comp_id] } }
 #align category_theory.evaluation_adjunction_left CategoryTheory.evaluationAdjunctionLeft
 
 instance evaluationIsLeftAdjoint (c : C) : IsLeftAdjoint ((evaluation _ D).obj c) :=

Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

@@ -153,7 +153,7 @@ noncomputable def preservesFinOfPreservesBinaryAndTerminal :
     refine' Fin.inductionOn j ?_ ?_
     · apply (Category.id_comp _).symm
     · rintro i _
-      dsimp [extendFan_π_app, Iso.refl_hom, Fan.mk_π]
+      dsimp [extendFan_π_app, Iso.refl_hom, Fan.mk_π_app]
       rw [Fin.cases_succ, Fin.cases_succ]
       change F.map _ ≫ _ = 𝟙 _ ≫ _
       simp only [id_comp, ← F.map_comp]
@@ -298,7 +298,7 @@ noncomputable def preservesFinOfPreservesBinaryAndInitial :
     refine' Fin.inductionOn j ?_ ?_
     · apply Category.comp_id
     · rintro i _
-      dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι]
+      dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι_app]
       rw [Fin.cases_succ, Fin.cases_succ, comp_id, ← F.map_comp]
 #align category_theory.preserves_fin_of_preserves_binary_and_initial CategoryTheory.preservesFinOfPreservesBinaryAndInitialₓ  -- Porting note: order of universes changed
 

Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

@@ -746,9 +746,7 @@ noncomputable def multicoforkEquivSigmaCofork :
             apply Limits.colimit.hom_ext
             rintro ⟨j⟩
             dsimp
-            -- porting note: the last element was `cofan.mk_ι_app` in mathlib3 but at the
-            -- time of writing this was not being generated by `@[simps]` on `Cofan.mk` in lean4
-            simp only [Category.comp_id, colimit.ι_desc, Cofan.mk_ι]
+            simp only [Category.comp_id, colimit.ι_desc, Cofan.mk_ι_app]
             rfl))
       fun {K₁ K₂} f => by
         -- porting note: in mathlib3 the next line was just `ext`

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -64,15 +64,15 @@ abbrev Cofan (f : β → C) :=
 #align category_theory.limits.cofan CategoryTheory.Limits.Cofan
 
 /-- A fan over `f : β → C` consists of a collection of maps from an object `P` to every `f b`. -/
-@[simps]
+@[simps! pt π_app]
 def Fan.mk {f : β → C} (P : C) (p : ∀ b, P ⟶ f b) : Fan f
     where
   pt := P
   π := Discrete.natTrans (fun X => p X.as)
 #align category_theory.limits.fan.mk CategoryTheory.Limits.Fan.mk
 
 /-- A cofan over `f : β → C` consists of a collection of maps from every `f b` to an object `P`. -/
-@[simps]
+@[simps! pt ι_app]
 def Cofan.mk {f : β → C} (P : C) (p : ∀ b, f b ⟶ P) : Cofan f
     where
   pt := P
@@ -243,7 +243,7 @@ theorem map_lift_piComparison [HasProduct f] [HasProduct fun b => G.obj (f b)] (
     (g : ∀ j, P ⟶ f j) : G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j) := by
   ext ⟨j⟩
   simp only [Discrete.functor_obj, Category.assoc, piComparison_comp_π, ← G.map_comp,
-    limit.lift_π, Fan.mk_pt, Fan.mk_π, Discrete.natTrans_app]
+    limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
 #align category_theory.limits.map_lift_pi_comparison CategoryTheory.Limits.map_lift_piComparison
 
 /-- The comparison morphism for the coproduct of `f`. This is an iso iff `G` preserves the coproduct
@@ -265,7 +265,7 @@ theorem sigmaComparison_map_desc [HasCoproduct f] [HasCoproduct fun b => G.obj (
     sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j) := by
   ext ⟨j⟩
   simp only [Discrete.functor_obj, ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc,
-    Cofan.mk_pt, Cofan.mk_ι, Discrete.natTrans_app]
+    Cofan.mk_pt, Cofan.mk_ι_app]
 #align category_theory.limits.sigma_comparison_map_desc CategoryTheory.Limits.sigmaComparison_map_desc
 
 end Comparison