feat: port Order.Category.HeytAlgCat (#5021)

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Mathlib.lean

@@ -2277,6 +2277,7 @@ import Mathlib.Order.Category.CompleteLatCat
 import Mathlib.Order.Category.DistLatCat
 import Mathlib.Order.Category.FinPartOrd
 import Mathlib.Order.Category.FrmCat
+import Mathlib.Order.Category.HeytAlgCat
 import Mathlib.Order.Category.LatCat
 import Mathlib.Order.Category.LinOrdCat
 import Mathlib.Order.Category.NonemptyFinLinOrdCat

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -60,6 +60,7 @@ deriving instance LargeCategory for SemiRingCat
 
 --Porting note: deriving fails for ConcreteCategory, adding instance manually.
 --deriving instance LargeCategory, ConcreteCategory for SemiRingCat
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
 
 instance : ConcreteCategory SemiRingCat := by
   dsimp [SemiRingCat]
@@ -168,6 +169,7 @@ instance : BundledHom.ParentProjection @Ring.toSemiring :=
 
 -- Porting note: Another place where mathlib had derived a concrete category
 -- but this does not work here, so we add the instance manually.
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
 deriving instance LargeCategory for RingCat
 
 instance : ConcreteCategory RingCat := by
@@ -260,6 +262,7 @@ instance : BundledHom.ParentProjection @CommSemiring.toSemiring :=
   ⟨⟩
 
 -- Porting note: again, deriving fails for concrete category instances.
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
 deriving instance LargeCategory for CommSemiRingCat
 
 instance : ConcreteCategory CommSemiRingCat := by
@@ -369,6 +372,7 @@ instance : BundledHom.ParentProjection @CommRing.toRing :=
   ⟨⟩
 
 -- Porting note: deriving fails for concrete category.
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
 deriving instance LargeCategory for CommRingCat
 
 instance : ConcreteCategory CommRingCat := by

Mathlib/MeasureTheory/Category/MeasCat.lean

@@ -72,6 +72,7 @@ instance unbundledHom : UnbundledHom @Measurable :=
 deriving instance LargeCategory for MeasCat
 
 -- Porting note: `deriving instance ConcreteCategory for MeasCat` didn't work. Define it manually.
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
 instance : ConcreteCategory MeasCat := by
   unfold MeasCat
   infer_instance

Mathlib/Order/Category/DistLatCat.lean

@@ -58,6 +58,7 @@ instance : BundledHom.ParentProjection @DistribLattice.toLattice :=
 
 deriving instance LargeCategory for DistLatCat
 
+-- Porting note: probably see https://github.com/leanprover-community/mathlib4/issues/5020
 instance : ConcreteCategory DistLatCat :=
   BundledHom.concreteCategory _
 

Mathlib/Order/Category/FrmCat.lean

@@ -69,6 +69,7 @@ instance bundledHom : BundledHom Hom where
 #align Frm.bundled_hom FrmCat.bundledHom
 
 -- Porting note: Originally `deriving instance LargeCategory, ConcreteCategory for FrmCat`
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
 deriving instance LargeCategory, Category for FrmCat
 
 instance : ConcreteCategory FrmCat := by

Mathlib/Order/Category/HeytAlgCat.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+
+! This file was ported from Lean 3 source module order.category.HeytAlg
+! leanprover-community/mathlib commit e8ac6315bcfcbaf2d19a046719c3b553206dac75
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Order.Category.BddDistLatCat
+import Mathlib.Order.Heyting.Hom
+
+/-!
+# The category of Heyting algebras
+
+This file defines `HeytAlg`, the category of Heyting algebras.
+-/
+
+set_option linter.uppercaseLean3 false
+
+universe u
+
+open CategoryTheory Opposite Order
+
+/-- The category of Heyting algebras. -/
+def HeytAlgCat :=
+  Bundled HeytingAlgebra
+#align HeytAlg HeytAlgCat
+
+namespace HeytAlgCat
+
+instance : CoeSort HeytAlgCat (Type _) :=
+  Bundled.coeSort
+
+instance (X : HeytAlgCat) : HeytingAlgebra X :=
+  X.str
+
+/-- Construct a bundled `HeytAlgCat` from a `HeytingAlgebra`. -/
+def of (α : Type _) [HeytingAlgebra α] : HeytAlgCat :=
+  Bundled.of α
+#align HeytAlg.of HeytAlgCat.of
+
+@[simp]
+theorem coe_of (α : Type _) [HeytingAlgebra α] : ↥(of α) = α :=
+  rfl
+#align HeytAlg.coe_of HeytAlgCat.coe_of
+
+instance : Inhabited HeytAlgCat :=
+  ⟨of PUnit⟩
+
+instance bundledHom : BundledHom HeytingHom where
+  toFun α β [HeytingAlgebra α] [HeytingAlgebra β] := (FunLike.coe : HeytingHom α β → α → β)
+  id := @HeytingHom.id
+  comp := @HeytingHom.comp
+  hom_ext α β [HeytingAlgebra α] [HeytingAlgebra β] := FunLike.coe_injective
+#align HeytAlg.bundled_hom HeytAlgCat.bundledHom
+
+deriving instance LargeCategory for HeytAlgCat
+
+-- Porting note: deriving failed.
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
+instance : ConcreteCategory HeytAlgCat := by
+  dsimp [HeytAlgCat]
+  infer_instance
+
+-- Porting note: No idea why it does not find this instance...
+instance {X Y : HeytAlgCat.{u}} : HeytingHomClass (X ⟶ Y) ↑X ↑Y :=
+  HeytingHom.instHeytingHomClass
+
+@[simps]
+instance hasForgetToLat : HasForget₂ HeytAlgCat BddDistLatCat where
+  forget₂ :=
+    { obj := fun X => BddDistLatCat.of X
+      map := fun {X Y} f => (f : BoundedLatticeHom X Y) }
+#align HeytAlg.has_forget_to_Lat HeytAlgCat.hasForgetToLat
+
+/-- Constructs an isomorphism of Heyting algebras from an order isomorphism between them. -/
+@[simps]
+def Iso.mk {α β : HeytAlgCat.{u}} (e : α ≃o β) : α ≅ β where
+  hom := (e : HeytingHom _ _)
+  inv := (e.symm : HeytingHom _ _)
+  hom_inv_id := by ext; exact e.symm_apply_apply _
+  inv_hom_id := by ext; exact e.apply_symm_apply _
+#align HeytAlg.iso.mk HeytAlgCat.Iso.mk
+
+end HeytAlgCat

Mathlib/Order/Category/LinOrdCat.lean

@@ -34,6 +34,7 @@ instance : BundledHom.ParentProjection @LinearOrder.toPartialOrder :=
 
 deriving instance LargeCategory for LinOrdCat
 
+-- Porting note: Probably see https://github.com/leanprover-community/mathlib4/issues/5020
 instance : ConcreteCategory LinOrdCat :=
   BundledHom.concreteCategory _
 

Mathlib/Order/Category/NonemptyFinLinOrdCat.lean

@@ -69,6 +69,7 @@ instance : BundledHom.ParentProjection @NonemptyFinLinOrd.toLinearOrder :=
 
 deriving instance LargeCategory for NonemptyFinLinOrdCat
 
+-- Porting note: probably see https://github.com/leanprover-community/mathlib4/issues/5020
 instance : ConcreteCategory NonemptyFinLinOrdCat :=
   BundledHom.concreteCategory _
 

Mathlib/Order/Category/PartOrdCat.lean

@@ -35,6 +35,7 @@ instance : BundledHom.ParentProjection @PartialOrder.toPreorder :=
 
 deriving instance LargeCategory for PartOrdCat
 
+-- Porting note: probably see https://github.com/leanprover-community/mathlib4/issues/5020
 instance : ConcreteCategory PartOrdCat :=
   BundledHom.concreteCategory _
 

Mathlib/Order/Category/PreordCat.lean

@@ -40,6 +40,7 @@ instance : BundledHom @OrderHom where
 
 deriving instance LargeCategory for PreordCat
 
+-- Porting note: probably see https://github.com/leanprover-community/mathlib4/issues/5020
 instance : ConcreteCategory PreordCat :=
   BundledHom.concreteCategory _
 

Mathlib/Order/Heyting/Hom.lean

@@ -244,7 +244,7 @@ namespace HeytingHom
 
 variable [HeytingAlgebra α] [HeytingAlgebra β] [HeytingAlgebra γ] [HeytingAlgebra δ]
 
-instance : HeytingHomClass (HeytingHom α β) α β where
+instance instHeytingHomClass : HeytingHomClass (HeytingHom α β) α β where
   coe f := f.toFun
   coe_injective' f g h := by obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f; obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g; congr
   map_sup f := f.map_sup'

Mathlib/Topology/Category/TopCat/Basic.lean

@@ -46,6 +46,7 @@ set_option linter.uppercaseLean3 false in
 deriving instance LargeCategory for TopCat
 
 -- Porting note: currently no derive handler for ConcreteCategory
+-- see https://github.com/leanprover-community/mathlib4/issues/5020
 instance concreteCategory : ConcreteCategory TopCat := by
   dsimp [TopCat]
   infer_instance