diff --git a/Mathlib.lean b/Mathlib.lean
index fa28f69d477e9..dcf15edc173f4 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -218,6 +218,7 @@ import Mathlib.Algebra.Support
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.CategoryTheory.Adjunction.Basic
 import Mathlib.CategoryTheory.Arrow
 import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Basic
@@ -226,6 +227,7 @@ import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Category.RelCat
+import Mathlib.CategoryTheory.CommSq
 import Mathlib.CategoryTheory.Comma
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
 import Mathlib.CategoryTheory.DiscreteCategory
@@ -240,13 +242,18 @@ import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Functor.Const
 import Mathlib.CategoryTheory.Functor.Currying
 import Mathlib.CategoryTheory.Functor.Default
+import Mathlib.CategoryTheory.Functor.EpiMono
 import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.InvIsos
+import Mathlib.CategoryTheory.Functor.ReflectsIso
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.Limits.Cones
+import Mathlib.CategoryTheory.LiftingProperties.Adjunction
+import Mathlib.CategoryTheory.LiftingProperties.Basic
+import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Opposites
diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean
new file mode 100644
index 0000000000000..a5b65f05aaa50
--- /dev/null
+++ b/Mathlib/CategoryTheory/Adjunction/Basic.lean
@@ -0,0 +1,677 @@
+/-
+Copyright (c) 2019 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton, Johan Commelin, Bhavik Mehta
+
+! This file was ported from Lean 3 source module category_theory.adjunction.basic
+! leanprover-community/mathlib commit d101e93197bb5f6ea89bd7ba386b7f7dff1f3903
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Equivalence
+
+/-!
+# Adjunctions between functors
+
+`F ⊣ G` represents the data of an adjunction between two functors
+`F : C ⥤ D` and `G : D ⥤ C`. `F` is the left adjoint and `G` is the right adjoint.
+
+We provide various useful constructors:
+* `mkOfHomEquiv`
+* `mkOfUnitCounit`
+* `leftAdjointOfEquiv` / `rightAdjointOfEquiv`
+  construct a left/right adjoint of a given functor given the action on objects and
+  the relevant equivalence of morphism spaces.
+* `adjunctionOfEquivLeft` / `adjunctionOfEquivRight` witness that these constructions
+  give adjunctions.
+
+There are also typeclasses `IsLeftAdjoint` / `IsRightAdjoint`, carrying data witnessing
+that a given functor is a left or right adjoint.
+Given `[IsLeftAdjoint F]`, a right adjoint of `F` can be constructed as `rightAdjoint F`.
+
+`Adjunction.comp` composes adjunctions.
+
+`toEquivalence` upgrades an adjunction to an equivalence,
+given witnesses that the unit and counit are pointwise isomorphisms.
+Conversely `Equivalence.toAdjunction` recovers the underlying adjunction from an equivalence.
+-/
+
+
+namespace CategoryTheory
+
+open Category
+
+-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+-- Porting Note: `elab_without_expected_type` cannot be a local attribute
+-- attribute [local elab_without_expected_type] whiskerLeft whiskerRight
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+/-- `F ⊣ G` represents the data of an adjunction between two functors
+`F : C ⥤ D` and `G : D ⥤ C`. `F` is the left adjoint and `G` is the right adjoint.
+
+To construct an `adjunction` between two functors, it's often easier to instead use the
+constructors `mkOfHomEquiv` or `mkOfUnitCounit`. To construct a left adjoint,
+there are also constructors `leftAdjointOfEquiv` and `adjunctionOfEquivLeft` (as
+well as their duals) which can be simpler in practice.
+
+Uniqueness of adjoints is shown in `CategoryTheory.Adjunction.Opposites`.
+
+See <https://stacks.math.columbia.edu/tag/0037>.
+-/
+structure Adjunction (F : C ⥤ D) (G : D ⥤ C) where
+  /-- The equivalence between `Hom (F X) Y` and `Hom X (G Y)` coming from an adjunction -/
+  homEquiv : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
+  /-- The unit of an adjunction -/
+  unit : 𝟭 C ⟶ F.comp G
+  /-- The counit of an adjunction -/
+  counit : G.comp F ⟶ 𝟭 D
+  -- Porting note: It's strange that this `Prop` is being flagged by the `docBlame` linter
+  /-- Naturality of the unit of an adjunction -/
+  homEquiv_unit : ∀ {X Y f}, (homEquiv X Y) f = (unit : _ ⟶ _).app X ≫ G.map f := by aesop_cat
+  -- Porting note: It's strange that this `Prop` is being flagged by the `docBlame` linter
+  /-- Naturality of the counit of an adjunction -/
+  homEquiv_counit : ∀ {X Y g}, (homEquiv X Y).symm g = F.map g ≫ counit.app Y := by aesop_cat
+#align category_theory.adjunction CategoryTheory.Adjunction
+#align category_theory.adjunction.hom_equiv CategoryTheory.Adjunction.homEquiv
+#align category_theory.adjunction.hom_equiv_unit CategoryTheory.Adjunction.homEquiv_unit
+#align category_theory.adjunction.hom_equiv_unit' CategoryTheory.Adjunction.homEquiv_unit
+#align category_theory.adjunction.hom_equiv_counit CategoryTheory.Adjunction.homEquiv_counit
+#align category_theory.adjunction.hom_equiv_counit' CategoryTheory.Adjunction.homEquiv_counit
+
+-- mathport name: «expr ⊣ »
+/-- The notation `F ⊣ G` stands for `Adjunction F G` representing that `F` is left adjoint to `G` -/
+infixl:15 " ⊣ " => Adjunction
+
+/-- A class giving a chosen right adjoint to the functor `left`. -/
+class IsLeftAdjoint (left : C ⥤ D) where
+  /-- The right adjoint to `left` -/
+  right : D ⥤ C
+  /-- The adjunction between `left` and `right` -/
+  adj : left ⊣ right
+#align category_theory.is_left_adjoint CategoryTheory.IsLeftAdjoint
+
+/-- A class giving a chosen left adjoint to the functor `right`. -/
+class IsRightAdjoint (right : D ⥤ C) where
+  /-- The left adjoint to `right` -/
+  left : C ⥤ D
+  /-- The adjunction between `left` and `right` -/
+  adj : left ⊣ right
+#align category_theory.is_right_adjoint CategoryTheory.IsRightAdjoint
+
+/-- Extract the left adjoint from the instance giving the chosen adjoint. -/
+def leftAdjoint (R : D ⥤ C) [IsRightAdjoint R] : C ⥤ D :=
+  IsRightAdjoint.left R
+#align category_theory.left_adjoint CategoryTheory.leftAdjoint
+
+/-- Extract the right adjoint from the instance giving the chosen adjoint. -/
+def rightAdjoint (L : C ⥤ D) [IsLeftAdjoint L] : D ⥤ C :=
+  IsLeftAdjoint.right L
+#align category_theory.right_adjoint CategoryTheory.rightAdjoint
+
+/-- The adjunction associated to a functor known to be a left adjoint. -/
+def Adjunction.ofLeftAdjoint (left : C ⥤ D) [IsLeftAdjoint left] :
+    Adjunction left (rightAdjoint left) :=
+  IsLeftAdjoint.adj
+#align category_theory.adjunction.of_left_adjoint CategoryTheory.Adjunction.ofLeftAdjoint
+
+/-- The adjunction associated to a functor known to be a right adjoint. -/
+def Adjunction.ofRightAdjoint (right : C ⥤ D) [IsRightAdjoint right] :
+    Adjunction (leftAdjoint right) right :=
+  IsRightAdjoint.adj
+#align category_theory.adjunction.of_right_adjoint CategoryTheory.Adjunction.ofRightAdjoint
+
+namespace Adjunction
+
+-- porting note: Workaround not needed in Lean 4
+-- restate_axiom homEquiv_unit'
+
+-- restate_axiom homEquiv_counit'
+
+attribute [simp] homEquiv_unit homEquiv_counit
+
+section
+
+variable {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) {X' X : C} {Y Y' : D}
+
+theorem homEquiv_id (X : C) : adj.homEquiv X _ (𝟙 _) = adj.unit.app X := by simp
+#align category_theory.adjunction.hom_equiv_id CategoryTheory.Adjunction.homEquiv_id
+
+theorem homEquiv_symm_id (X : D) : (adj.homEquiv _ X).symm (𝟙 _) = adj.counit.app X := by simp
+#align category_theory.adjunction.hom_equiv_symm_id CategoryTheory.Adjunction.homEquiv_symm_id
+
+/-
+Porting note: `nolint simpNF` as the linter was complaining that this was provable using `simp`
+but it is in fact not. Also the `docBlame` linter expects a docstring even though this is `Prop`
+valued
+-/
+@[simp, nolint simpNF]
+theorem homEquiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
+    (adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g := by
+  rw [homEquiv_counit, F.map_comp, assoc, adj.homEquiv_counit.symm]
+#align category_theory.adjunction.hom_equiv_naturality_left_symm CategoryTheory.Adjunction.homEquiv_naturality_left_symm
+
+-- Porting note: Same as above
+@[simp, nolint simpNF]
+theorem homEquiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
+    (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g := by
+  rw [← Equiv.eq_symm_apply]
+  simp only [Equiv.symm_apply_apply,eq_self_iff_true,homEquiv_naturality_left_symm]
+#align category_theory.adjunction.hom_equiv_naturality_left CategoryTheory.Adjunction.homEquiv_naturality_left
+
+-- Porting note: Same as above
+@[simp, nolint simpNF]
+theorem homEquiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') :
+    (adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g := by
+  rw [homEquiv_unit, G.map_comp, ← assoc, ← homEquiv_unit]
+#align category_theory.adjunction.hom_equiv_naturality_right CategoryTheory.Adjunction.homEquiv_naturality_right
+
+-- Porting note: Same as above
+@[simp, nolint simpNF]
+theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
+    (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g := by
+  rw [Equiv.symm_apply_eq]
+  simp only [homEquiv_naturality_right,eq_self_iff_true,Equiv.apply_symm_apply]
+#align category_theory.adjunction.hom_equiv_naturality_right_symm CategoryTheory.Adjunction.homEquiv_naturality_right_symm
+
+@[simp]
+theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = NatTrans.id _ := by
+  ext; dsimp
+  erw [← adj.homEquiv_counit, Equiv.symm_apply_eq, adj.homEquiv_unit]
+  simp
+#align category_theory.adjunction.left_triangle CategoryTheory.Adjunction.left_triangle
+
+@[simp]
+theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = NatTrans.id _ := by
+  ext; dsimp
+  erw [← adj.homEquiv_unit, ← Equiv.eq_symm_apply, adj.homEquiv_counit]
+  simp
+#align category_theory.adjunction.right_triangle CategoryTheory.Adjunction.right_triangle
+
+@[reassoc (attr := simp)]
+theorem left_triangle_components :
+    F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X) :=
+  congr_arg (fun t : NatTrans _ (𝟭 C ⋙ F) => t.app X) adj.left_triangle
+#align category_theory.adjunction.left_triangle_components CategoryTheory.Adjunction.left_triangle_components
+
+@[reassoc (attr := simp)]
+theorem right_triangle_components {Y : D} :
+    adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y) :=
+  congr_arg (fun t : NatTrans _ (G ⋙ 𝟭 C) => t.app Y) adj.right_triangle
+#align category_theory.adjunction.right_triangle_components CategoryTheory.Adjunction.right_triangle_components
+
+@[reassoc (attr := simp)]
+theorem counit_naturality {X Y : D} (f : X ⟶ Y) :
+    F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f :=
+  adj.counit.naturality f
+#align category_theory.adjunction.counit_naturality CategoryTheory.Adjunction.counit_naturality
+
+@[reassoc (attr := simp)]
+theorem unit_naturality {X Y : C} (f : X ⟶ Y) :
+    adj.unit.app X ≫ G.map (F.map f) = f ≫ adj.unit.app Y :=
+  (adj.unit.naturality f).symm
+#align category_theory.adjunction.unit_naturality CategoryTheory.Adjunction.unit_naturality
+
+theorem homEquiv_apply_eq {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
+    adj.homEquiv A B f = g ↔ f = (adj.homEquiv A B).symm g :=
+  ⟨fun h => by
+    cases h
+    simp, fun h => by
+    cases h
+    simp⟩
+#align category_theory.adjunction.hom_equiv_apply_eq CategoryTheory.Adjunction.homEquiv_apply_eq
+
+theorem eq_homEquiv_apply {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
+    g = adj.homEquiv A B f ↔ (adj.homEquiv A B).symm g = f :=
+  ⟨fun h => by
+    cases h
+    simp, fun h => by
+    cases h
+    simp⟩
+#align category_theory.adjunction.eq_hom_equiv_apply CategoryTheory.Adjunction.eq_homEquiv_apply
+
+end
+
+end Adjunction
+
+namespace Adjunction
+
+/-- This is an auxiliary data structure useful for constructing adjunctions.
+See `Adjunction.mkOfHomEquiv`.
+This structure won't typically be used anywhere else.
+-/
+-- Porting comment: `has_nonempty_instance` linter doesn't exist (yet?)
+-- @[nolint has_nonempty_instance]
+structure CoreHomEquiv (F : C ⥤ D) (G : D ⥤ C) where
+  /-- The equivalence between `Hom (F X) Y` and `Hom X (G Y)` -/
+  homEquiv : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
+  /-- The property that describes how `homEquiv.symm` transforms compositions `X' ⟶ X ⟶ G Y` -/
+  homEquiv_naturality_left_symm :
+    ∀ {X' X Y} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
+      (homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (homEquiv X Y).symm g := by
+    aesop_cat
+  /-- The property that describes how `homEquiv` transforms compositions `F X ⟶ Y ⟶ Y'` -/
+  homEquiv_naturality_right :
+    ∀ {X Y Y'} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
+      (homEquiv X Y') (f ≫ g) = (homEquiv X Y) f ≫ G.map g := by
+    aesop_cat
+#align category_theory.adjunction.core_hom_equiv CategoryTheory.Adjunction.CoreHomEquiv
+#align category_theory.adjunction.core_hom_equiv.hom_equiv CategoryTheory.Adjunction.CoreHomEquiv.homEquiv
+#align category_theory.adjunction.core_hom_equiv.hom_equiv' CategoryTheory.Adjunction.CoreHomEquiv.homEquiv
+#align category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right
+#align category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right' CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right
+#align category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left_symm CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm
+#align category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left_symm' CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm
+
+namespace CoreHomEquiv
+
+-- Porting note: Workaround not needed in Lean 4.
+-- restate_axiom homEquiv_naturality_left_symm'
+
+-- restate_axiom homEquiv_naturality_right'
+
+attribute [simp] homEquiv_naturality_left_symm homEquiv_naturality_right
+
+variable {F : C ⥤ D} {G : D ⥤ C} (adj : CoreHomEquiv F G) {X' X : C} {Y Y' : D}
+
+@[simp]
+theorem homEquiv_naturality_left_aux (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
+    (adj.homEquiv X' (F.obj X)) (F.map f) ≫ G.map g = f ≫ (adj.homEquiv X Y) g := by
+  rw [← homEquiv_naturality_right, ← Equiv.eq_symm_apply] ; simp
+
+-- @[simp] -- Porting note: LHS simplifies, added aux lemma above
+theorem homEquiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
+    (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g := by
+  rw [← Equiv.eq_symm_apply] ; simp
+#align category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left
+
+@[simp]
+theorem homEquiv_naturality_right_symm_aux (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
+    F.map f ≫ (adj.homEquiv (G.obj Y) Y').symm (G.map g) = (adj.homEquiv X Y).symm f ≫ g := by
+  rw [← homEquiv_naturality_left_symm, Equiv.symm_apply_eq] ; simp
+
+-- @[simp] -- Porting note: LHS simplifies, added aux lemma above
+theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
+    (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g := by
+  rw [Equiv.symm_apply_eq] ; simp
+#align category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right_symm CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm
+
+end CoreHomEquiv
+
+/-- This is an auxiliary data structure useful for constructing adjunctions.
+See `Adjunction.mkOfUnitCounit`.
+This structure won't typically be used anywhere else.
+-/
+-- Porting comment: `has_nonempty_instance` linter doesn't exist (yet?)
+-- @[nolint has_nonempty_instance]
+structure CoreUnitCounit (F : C ⥤ D) (G : D ⥤ C) where
+  /-- The unit of an adjunction between `F` and `G` -/
+  unit : 𝟭 C ⟶ F.comp G
+  /-- The counit of an adjunction between `F` and `G`s -/
+  counit : G.comp F ⟶ 𝟭 D
+  /-- Equality of the composition of the unit, associator, and counit with the identity
+  `F ⟶ (F G) F ⟶ F (G F) ⟶ F = NatTrans.id F` -/
+  left_triangle :
+    whiskerRight unit F ≫ (Functor.associator F G F).hom ≫ whiskerLeft F counit =
+      NatTrans.id (𝟭 C ⋙ F) := by
+    aesop_cat
+  /-- Equality of the composition of the unit, associator, and counit with the identity
+  `G ⟶ G (F G) ⟶ (F G) F ⟶ G = NatTrans.id G` -/
+  right_triangle :
+    whiskerLeft G unit ≫ (Functor.associator G F G).inv ≫ whiskerRight counit G =
+      NatTrans.id (G ⋙ 𝟭 C) := by
+    aesop_cat
+#align category_theory.adjunction.core_unit_counit CategoryTheory.Adjunction.CoreUnitCounit
+#align category_theory.adjunction.core_unit_counit.left_triangle' CategoryTheory.Adjunction.CoreUnitCounit.left_triangle
+#align category_theory.adjunction.core_unit_counit.left_triangle CategoryTheory.Adjunction.CoreUnitCounit.left_triangle
+#align category_theory.adjunction.core_unit_counit.right_triangle' CategoryTheory.Adjunction.CoreUnitCounit.right_triangle
+#align category_theory.adjunction.core_unit_counit.right_triangle CategoryTheory.Adjunction.CoreUnitCounit.right_triangle
+
+namespace CoreUnitCounit
+
+attribute [simp] left_triangle right_triangle
+
+end CoreUnitCounit
+
+variable {F : C ⥤ D} {G : D ⥤ C}
+
+/-- Construct an adjunction between `F` and `G` out of a natural bijection between each
+`F.obj X ⟶ Y` and `X ⟶ G.obj Y`. -/
+@[simps]
+def mkOfHomEquiv (adj : CoreHomEquiv F G) : F ⊣ G :=
+  -- See note [dsimp, simp].
+  { adj with
+    unit :=
+      { app := fun X => (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X))
+        naturality := by
+          intros
+          erw [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right]
+          dsimp; simp }
+    counit :=
+      { app := fun Y => (adj.homEquiv _ _).invFun (𝟙 (G.obj Y))
+        naturality := by
+          intros
+          erw [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm]
+          dsimp; simp }
+    homEquiv_unit := @fun X Y f => by erw [← adj.homEquiv_naturality_right]; simp
+    homEquiv_counit := @fun X Y f => by erw [← adj.homEquiv_naturality_left_symm]; simp
+  }
+#align category_theory.adjunction.mk_of_hom_equiv CategoryTheory.Adjunction.mkOfHomEquiv
+
+/-- Construct an adjunction between functors `F` and `G` given a unit and counit for the adjunction
+satisfying the triangle identities. -/
+
+@[simps!]
+def mkOfUnitCounit (adj : CoreUnitCounit F G) : F ⊣ G :=
+  { adj with
+    homEquiv := fun X Y =>
+      { toFun := fun f => adj.unit.app X ≫ G.map f
+        invFun := fun g => F.map g ≫ adj.counit.app Y
+        left_inv := fun f => by
+          change F.map (_ ≫ _) ≫ _ = _
+          rw [F.map_comp, assoc, ← Functor.comp_map, adj.counit.naturality, ← assoc]
+          convert id_comp f
+          have t := congrArg (fun (s : NatTrans (𝟭 C ⋙ F) (F ⋙ 𝟭 D)) => s.app X) adj.left_triangle
+          dsimp at t
+          simp only [id_comp] at t
+          exact t
+        right_inv := fun g => by
+          change _ ≫ G.map (_ ≫ _) = _
+          rw [G.map_comp, ← assoc, ← Functor.comp_map, ← adj.unit.naturality, assoc]
+          convert comp_id g
+          have t := congrArg (fun t : NatTrans (G ⋙ 𝟭 C) (𝟭 D ⋙ G) => t.app Y) adj.right_triangle
+          dsimp at t
+          simp only [id_comp] at t
+          exact t } }
+#align category_theory.adjunction.mk_of_unit_counit CategoryTheory.Adjunction.mkOfUnitCounit
+
+/- Porting note: simpNF linter claims these are solved by simp but that 
+is not true -/
+attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply 
+attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply 
+
+/-- The adjunction between the identity functor on a category and itself. -/
+def id : 𝟭 C ⊣ 𝟭 C where
+  homEquiv X Y := Equiv.refl _
+  unit := 𝟙 _
+  counit := 𝟙 _
+#align category_theory.adjunction.id CategoryTheory.Adjunction.id
+
+-- Satisfy the inhabited linter.
+instance : Inhabited (Adjunction (𝟭 C) (𝟭 C)) :=
+  ⟨id⟩
+
+/-- If F and G are naturally isomorphic functors, establish an equivalence of hom-sets. -/
+@[simps]
+def equivHomsetLeftOfNatIso {F F' : C ⥤ D} (iso : F ≅ F') {X : C} {Y : D} :
+    (F.obj X ⟶ Y) ≃ (F'.obj X ⟶ Y)
+    where
+  toFun f := iso.inv.app _ ≫ f
+  invFun g := iso.hom.app _ ≫ g
+  left_inv f := by simp
+  right_inv g := by simp
+#align category_theory.adjunction.equiv_homset_left_of_nat_iso CategoryTheory.Adjunction.equivHomsetLeftOfNatIso
+
+/-- If G and H are naturally isomorphic functors, establish an equivalence of hom-sets. -/
+@[simps]
+def equivHomsetRightOfNatIso {G G' : D ⥤ C} (iso : G ≅ G') {X : C} {Y : D} :
+    (X ⟶ G.obj Y) ≃ (X ⟶ G'.obj Y)
+    where
+  toFun f := f ≫ iso.hom.app _
+  invFun g := g ≫ iso.inv.app _
+  left_inv f := by simp
+  right_inv g := by simp
+#align category_theory.adjunction.equiv_homset_right_of_nat_iso CategoryTheory.Adjunction.equivHomsetRightOfNatIso
+
+/-- Transport an adjunction along an natural isomorphism on the left. -/
+def ofNatIsoLeft {F G : C ⥤ D} {H : D ⥤ C} (adj : F ⊣ H) (iso : F ≅ G) : G ⊣ H :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv := fun X Y => (equivHomsetLeftOfNatIso iso.symm).trans (adj.homEquiv X Y) }
+#align category_theory.adjunction.of_nat_iso_left CategoryTheory.Adjunction.ofNatIsoLeft
+
+/-- Transport an adjunction along an natural isomorphism on the right. -/
+def ofNatIsoRight {F : C ⥤ D} {G H : D ⥤ C} (adj : F ⊣ G) (iso : G ≅ H) : F ⊣ H :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv := fun X Y => (adj.homEquiv X Y).trans (equivHomsetRightOfNatIso iso) }
+#align category_theory.adjunction.of_nat_iso_right CategoryTheory.Adjunction.ofNatIsoRight
+
+/-- Transport being a right adjoint along a natural isomorphism. -/
+def rightAdjointOfNatIso {F G : C ⥤ D} (h : F ≅ G) [r : IsRightAdjoint F] : IsRightAdjoint G
+    where
+  left := r.left
+  adj := ofNatIsoRight r.adj h
+#align category_theory.adjunction.right_adjoint_of_nat_iso CategoryTheory.Adjunction.rightAdjointOfNatIso
+
+/-- Transport being a left adjoint along a natural isomorphism. -/
+def leftAdjointOfNatIso {F G : C ⥤ D} (h : F ≅ G) [r : IsLeftAdjoint F] : IsLeftAdjoint G
+    where
+  right := r.right
+  adj := ofNatIsoLeft r.adj h
+#align category_theory.adjunction.left_adjoint_of_nat_iso CategoryTheory.Adjunction.leftAdjointOfNatIso
+
+section
+
+variable {E : Type u₃} [ℰ : Category.{v₃} E] {H : D ⥤ E} {I : E ⥤ D}
+
+/-- Composition of adjunctions.
+
+See <https://stacks.math.columbia.edu/tag/0DV0>.
+-/
+def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G
+    where
+  homEquiv X Z := Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)
+  unit := adj₁.unit ≫ (whiskerLeft F <| whiskerRight adj₂.unit G) ≫ (Functor.associator _ _ _).inv
+  counit :=
+    (Functor.associator _ _ _).hom ≫ (whiskerLeft I <| whiskerRight adj₁.counit H) ≫ adj₂.counit
+#align category_theory.adjunction.comp CategoryTheory.Adjunction.comp
+
+/-- If `F` and `G` are left adjoints then `F ⋙ G` is a left adjoint too. -/
+instance leftAdjointOfComp {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E)
+    [Fl : IsLeftAdjoint F] [Gl : IsLeftAdjoint G] : IsLeftAdjoint (F ⋙ G)
+    where
+  right := Gl.right ⋙ Fl.right
+  adj := Fl.adj.comp Gl.adj
+#align category_theory.adjunction.left_adjoint_of_comp CategoryTheory.Adjunction.leftAdjointOfComp
+
+/-- If `F` and `G` are right adjoints then `F ⋙ G` is a right adjoint too. -/
+instance rightAdjointOfComp {E : Type u₃} [Category.{v₃} E] {F : C ⥤ D} {G : D ⥤ E}
+    [Fr : IsRightAdjoint F] [Gr : IsRightAdjoint G] : IsRightAdjoint (F ⋙ G)
+    where
+  left := Gr.left ⋙ Fr.left
+  adj := Gr.adj.comp Fr.adj
+#align category_theory.adjunction.right_adjoint_of_comp CategoryTheory.Adjunction.rightAdjointOfComp
+
+end
+
+section ConstructLeft
+
+-- Construction of a left adjoint. In order to construct a left
+-- adjoint to a functor G : D → C, it suffices to give the object part
+-- of a functor F : C → D together with isomorphisms Hom(FX, Y) ≃
+-- Hom(X, GY) natural in Y. The action of F on morphisms can be
+-- constructed from this data.
+variable {F_obj : C → D}
+
+variable (e : ∀ X Y, (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
+
+variable (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g)
+
+private theorem he' {X Y Y'} (f g) : (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g := by
+  intros ; rw [Equiv.symm_apply_eq, he] ; simp
+-- #align category_theory.adjunction.he' category_theory.adjunction.he'
+
+/-- Construct a left adjoint functor to `G`, given the functor's value on objects `F_obj` and
+a bijection `e` between `F_obj X ⟶ Y` and `X ⟶ G.obj Y` satisfying a naturality law
+`he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g`.
+Dual to `rightAdjointOfEquiv`. -/
+@[simps!]
+def leftAdjointOfEquiv : C ⥤ D where
+  obj := F_obj
+  map {X} {X'} f := (e X (F_obj X')).symm (f ≫ e X' (F_obj X') (𝟙 _))
+  map_comp := fun f f' =>
+    by
+    rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]
+    conv =>
+      rhs
+      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
+    simp
+#align category_theory.adjunction.left_adjoint_of_equiv CategoryTheory.Adjunction.leftAdjointOfEquiv
+
+/-- Show that the functor given by `leftAdjointOfEquiv` is indeed left adjoint to `G`. Dual
+to `adjunctionOfRightEquiv`. -/
+@[simps!]
+def adjunctionOfEquivLeft : leftAdjointOfEquiv e he ⊣ G :=
+  mkOfHomEquiv
+    { homEquiv := e
+      homEquiv_naturality_left_symm := fun {X'} {X} {Y} f g => by
+        have := @he' C _ D _ G F_obj e he
+        erw [← this, ← Equiv.apply_eq_iff_eq (e X' Y)]
+        simp [(he X' (F_obj X) Y (e X Y |>.symm g) (leftAdjointOfEquiv e he |>.map f)).symm]
+        congr
+        rw [← he]
+        simp
+    }
+#align category_theory.adjunction.adjunction_of_equiv_left CategoryTheory.Adjunction.adjunctionOfEquivLeft
+
+end ConstructLeft
+
+section ConstructRight
+
+-- Construction of a right adjoint, analogous to the above.
+variable {G_obj : D → C}
+
+variable (e : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
+
+variable (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g)
+
+private theorem he'' {X' X Y} (f g) : F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g) := by
+  intros ; rw [Equiv.eq_symm_apply, he] ; simp
+-- #align category_theory.adjunction.he' category_theory.adjunction.he'
+
+/-- Construct a right adjoint functor to `F`, given the functor's value on objects `G_obj` and
+a bijection `e` between `F.obj X ⟶ Y` and `X ⟶ G_obj Y` satisfying a naturality law
+`he : ∀ X Y Y' g h, e X' Y (F.map f ≫ g) = f ≫ e X Y g`.
+Dual to `leftAdjointOfEquiv`. -/
+@[simps!]
+def rightAdjointOfEquiv : D ⥤ C where
+  obj := G_obj
+  map {Y} {Y'} g := (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 _) ≫ g)
+  map_comp := fun {Y} {Y'} {Y''} g g' => by
+    rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_apply]
+    conv =>
+      rhs
+      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
+    simp
+#align category_theory.adjunction.right_adjoint_of_equiv CategoryTheory.Adjunction.rightAdjointOfEquiv
+
+/-- Show that the functor given by `rightAdjointOfEquiv` is indeed right adjoint to `F`. Dual
+to `adjunctionOfEquivRight`. -/
+@[simps!]
+def adjunctionOfEquivRight : F ⊣ (rightAdjointOfEquiv e he) :=
+  mkOfHomEquiv
+    { homEquiv := e
+      homEquiv_naturality_left_symm := by
+        intro X X' Y f g; rw [Equiv.symm_apply_eq]; dsimp; rw [he]; simp
+      homEquiv_naturality_right := by
+        intro X Y Y' g h
+        erw [← he, Equiv.apply_eq_iff_eq, ← assoc, he'' e he, comp_id, Equiv.symm_apply_apply] }
+#align category_theory.adjunction.adjunction_of_equiv_right CategoryTheory.Adjunction.adjunctionOfEquivRight
+
+end ConstructRight
+
+/--
+If the unit and counit of a given adjunction are (pointwise) isomorphisms, then we can upgrade the
+adjunction to an equivalence.
+-/
+@[simps!]
+noncomputable def toEquivalence (adj : F ⊣ G) [∀ X, IsIso (adj.unit.app X)]
+    [∀ Y, IsIso (adj.counit.app Y)] : C ≌ D
+    where
+  functor := F
+  inverse := G
+  unitIso := NatIso.ofComponents (fun X => asIso (adj.unit.app X)) (by simp)
+  counitIso := NatIso.ofComponents (fun Y => asIso (adj.counit.app Y)) (by simp)
+#align category_theory.adjunction.to_equivalence CategoryTheory.Adjunction.toEquivalence
+
+/--
+If the unit and counit for the adjunction corresponding to a right adjoint functor are (pointwise)
+isomorphisms, then the functor is an equivalence of categories.
+-/
+@[simps!]
+noncomputable def isRightAdjointToIsEquivalence [IsRightAdjoint G]
+    [∀ X, IsIso ((Adjunction.ofRightAdjoint G).unit.app X)]
+    [∀ Y, IsIso ((Adjunction.ofRightAdjoint G).counit.app Y)] : IsEquivalence G :=
+  IsEquivalence.ofEquivalenceInverse (Adjunction.ofRightAdjoint G).toEquivalence
+#align category_theory.adjunction.is_right_adjoint_to_is_equivalence CategoryTheory.Adjunction.isRightAdjointToIsEquivalence
+
+end Adjunction
+
+open Adjunction
+
+namespace Equivalence
+
+/-- The adjunction given by an equivalence of categories. (To obtain the opposite adjunction,
+simply use `e.symm.toAdjunction`. -/
+def toAdjunction (e : C ≌ D) : e.functor ⊣ e.inverse :=
+  mkOfUnitCounit
+    ⟨e.unit, e.counit, by
+      ext
+      dsimp
+      simp only [id_comp]
+      exact e.functor_unit_comp _, by
+      ext
+      dsimp
+      simp only [id_comp]
+      exact e.unit_inverse_comp _⟩
+#align category_theory.equivalence.to_adjunction CategoryTheory.Equivalence.toAdjunction
+
+@[simp]
+theorem asEquivalence_toAdjunction_unit {e : C ≌ D} :
+    e.functor.asEquivalence.toAdjunction.unit = e.unit :=
+  rfl
+#align category_theory.equivalence.as_equivalence_to_adjunction_unit CategoryTheory.Equivalence.asEquivalence_toAdjunction_unit
+
+@[simp]
+theorem asEquivalence_toAdjunction_counit {e : C ≌ D} :
+    e.functor.asEquivalence.toAdjunction.counit = e.counit :=
+  rfl
+#align category_theory.equivalence.as_equivalence_to_adjunction_counit CategoryTheory.Equivalence.asEquivalence_toAdjunction_counit
+
+end Equivalence
+
+namespace Functor
+
+/-- An equivalence `E` is left adjoint to its inverse. -/
+def adjunction (E : C ⥤ D) [IsEquivalence E] : E ⊣ E.inv :=
+  E.asEquivalence.toAdjunction
+#align category_theory.functor.adjunction CategoryTheory.Functor.adjunction
+
+/-- If `F` is an equivalence, it's a left adjoint. -/
+instance (priority := 10) leftAdjointOfEquivalence {F : C ⥤ D} [IsEquivalence F] : IsLeftAdjoint F
+    where
+  right := _
+  adj := Functor.adjunction F
+#align category_theory.functor.left_adjoint_of_equivalence CategoryTheory.Functor.leftAdjointOfEquivalence
+
+@[simp]
+theorem rightAdjoint_of_isEquivalence {F : C ⥤ D} [IsEquivalence F] : rightAdjoint F = inv F :=
+  rfl
+#align category_theory.functor.right_adjoint_of_is_equivalence CategoryTheory.Functor.rightAdjoint_of_isEquivalence
+
+/-- If `F` is an equivalence, it's a right adjoint. -/
+instance (priority := 10) rightAdjointOfEquivalence {F : C ⥤ D} [IsEquivalence F] : IsRightAdjoint F
+    where
+  left := _
+  adj := Functor.adjunction F.inv
+#align category_theory.functor.right_adjoint_of_equivalence CategoryTheory.Functor.rightAdjointOfEquivalence
+
+@[simp]
+theorem leftAdjoint_of_isEquivalence {F : C ⥤ D} [IsEquivalence F] : leftAdjoint F = inv F :=
+  rfl
+#align category_theory.functor.left_adjoint_of_is_equivalence CategoryTheory.Functor.leftAdjoint_of_isEquivalence
+
+end Functor
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Arrow.lean b/Mathlib/CategoryTheory/Arrow.lean
index 475368b88c326..41f7ee32c56d9 100644
--- a/Mathlib/CategoryTheory/Arrow.lean
+++ b/Mathlib/CategoryTheory/Arrow.lean
@@ -334,4 +334,3 @@ def Arrow.isoOfNatIso {C D : Type _} [Category C] [Category D] {F G : C ⥤ D} (
 #align category_theory.arrow.iso_of_nat_iso CategoryTheory.Arrow.isoOfNatIso
  
 end CategoryTheory
-#lint
diff --git a/Mathlib/CategoryTheory/CommSq.lean b/Mathlib/CategoryTheory/CommSq.lean
new file mode 100644
index 0000000000000..12ffba8bc2641
--- /dev/null
+++ b/Mathlib/CategoryTheory/CommSq.lean
@@ -0,0 +1,241 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Joël Riou
+
+! This file was ported from Lean 3 source module category_theory.comm_sq
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Arrow
+
+/-!
+# Commutative squares
+
+This file provide an API for commutative squares in categories.
+If `top`, `left`, `right` and `bottom` are four morphisms which are the edges
+of a square, `CommSq top left right bottom` is the predicate that this
+square is commutative.
+
+The structure `CommSq` is extended in `CategoryTheory/Shapes/Limits/CommSq.lean`
+as `IsPullback` and `IsPushout` in order to define pullback and pushout squares.
+
+## Future work
+
+Refactor `LiftStruct` from `Arrow.lean` and lifting properties using `CommSq.lean`.
+
+-/
+
+
+namespace CategoryTheory
+
+variable {C : Type _} [Category C]
+
+/-- The proposition that a square
+```
+  W ---f---> X
+  |          |
+  g          h
+  |          |
+  v          v
+  Y ---i---> Z
+
+```
+is a commuting square.
+-/
+structure CommSq {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) : Prop where
+  /-- The square commutes. -/
+  w : f ≫ h = g ≫ i
+#align category_theory.comm_sq CategoryTheory.CommSq
+
+attribute [reassoc] CommSq.w
+
+namespace CommSq
+
+variable {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
+
+theorem flip (p : CommSq f g h i) : CommSq g f i h :=
+  ⟨p.w.symm⟩
+#align category_theory.comm_sq.flip CategoryTheory.CommSq.flip
+
+theorem of_arrow {f g : Arrow C} (h : f ⟶ g) : CommSq f.hom h.left h.right g.hom :=
+  ⟨h.w.symm⟩
+#align category_theory.comm_sq.of_arrow CategoryTheory.CommSq.of_arrow
+
+/-- The commutative square in the opposite category associated to a commutative square. -/
+theorem op (p : CommSq f g h i) : CommSq i.op h.op g.op f.op :=
+  ⟨by simp only [← op_comp, p.w]⟩
+#align category_theory.comm_sq.op CategoryTheory.CommSq.op
+
+/-- The commutative square associated to a commutative square in the opposite category. -/
+theorem unop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CommSq f g h i) :
+    CommSq i.unop h.unop g.unop f.unop :=
+  ⟨by simp only [← unop_comp, p.w]⟩
+#align category_theory.comm_sq.unop CategoryTheory.CommSq.unop
+
+end CommSq
+
+namespace Functor
+
+variable {D : Type _} [Category D]
+
+variable (F : C ⥤ D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
+
+theorem map_commSq (s : CommSq f g h i) : CommSq (F.map f) (F.map g) (F.map h) (F.map i) :=
+  ⟨by simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w⟩
+#align category_theory.functor.map_comm_sq CategoryTheory.Functor.map_commSq
+
+end Functor
+
+alias Functor.map_commSq ← CommSq.map
+#align category_theory.comm_sq.map CategoryTheory.CommSq.map
+
+namespace CommSq
+
+
+variable {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
+
+/-- Now we consider a square:
+```
+  A ---f---> X
+  |          |
+  i          p
+  |          |
+  v          v
+  B ---g---> Y
+```
+
+The datum of a lift in a commutative square, i.e. a up-right-diagonal
+morphism which makes both triangles commute. -/
+-- Porting note: removed @[nolint has_nonempty_instance]
+@[ext]
+structure LiftStruct (sq : CommSq f i p g) where
+  /-- The lift. -/
+  l : B ⟶ X
+  /-- The upper left triangle commutes. -/
+  fac_left : i ≫ l = f
+  /-- The lower right triangle commutes. -/
+  fac_right: l ≫ p = g
+#align category_theory.comm_sq.lift_struct CategoryTheory.CommSq.LiftStruct
+
+namespace LiftStruct
+
+/-- A `lift_struct` for a commutative square gives a `lift_struct` for the
+corresponding square in the opposite category. -/
+@[simps]
+def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op
+    where
+  l := l.l.op
+  fac_left := by rw [← op_comp, l.fac_right]
+  fac_right := by rw [← op_comp, l.fac_left]
+#align category_theory.comm_sq.lift_struct.op CategoryTheory.CommSq.LiftStruct.op
+
+/-- A `lift_struct` for a commutative square in the opposite category
+gives a `lift_struct` for the corresponding square in the original category. -/
+@[simps]
+def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CommSq f i p g}
+    (l : LiftStruct sq) : LiftStruct sq.unop
+    where
+  l := l.l.unop
+  fac_left := by rw [← unop_comp, l.fac_right]
+  fac_right := by rw [← unop_comp, l.fac_left]
+#align category_theory.comm_sq.lift_struct.unop CategoryTheory.CommSq.LiftStruct.unop
+
+/-- Equivalences of `lift_struct` for a square and the corresponding square
+in the opposite category. -/
+@[simps]
+def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
+    where
+  toFun := op
+  invFun := unop
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
+#align category_theory.comm_sq.lift_struct.op_equiv CategoryTheory.CommSq.LiftStruct.opEquiv
+
+/-- Equivalences of `lift_struct` for a square in the oppositive category and
+the corresponding square in the original category. -/
+def unopEquiv {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
+    (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.unop
+    where
+  toFun := unop
+  invFun := op
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
+#align category_theory.comm_sq.lift_struct.unop_equiv CategoryTheory.CommSq.LiftStruct.unopEquiv
+
+end LiftStruct
+
+instance subsingleton_liftStruct_of_epi (sq : CommSq f i p g) [Epi i] :
+    Subsingleton (LiftStruct sq) :=
+  ⟨fun l₁ l₂ => by
+    ext
+    rw [← cancel_epi i]
+    simp only [LiftStruct.fac_left]
+    ⟩
+#align category_theory.comm_sq.subsingleton_lift_struct_of_epi CategoryTheory.CommSq.subsingleton_liftStruct_of_epi
+
+instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
+    Subsingleton (LiftStruct sq) :=
+  ⟨fun l₁ l₂ => by
+    ext
+    rw [← cancel_mono p]
+    simp only [LiftStruct.fac_right]⟩
+#align category_theory.comm_sq.subsingleton_lift_struct_of_mono CategoryTheory.CommSq.subsingleton_liftStruct_of_mono
+
+variable (sq : CommSq f i p g)
+
+
+/-- The assertion that a square has a `lift_struct`. -/
+class HasLift : Prop where
+  /-- Square has a `lift_struct`. -/
+  exists_lift : Nonempty sq.LiftStruct
+#align category_theory.comm_sq.has_lift CategoryTheory.CommSq.HasLift
+
+namespace HasLift
+
+variable {sq}
+
+theorem mk' (l : sq.LiftStruct) : HasLift sq :=
+  ⟨Nonempty.intro l⟩
+#align category_theory.comm_sq.has_lift.mk' CategoryTheory.CommSq.HasLift.mk'
+
+variable (sq)
+
+theorem iff : HasLift sq ↔ Nonempty sq.LiftStruct := by
+  constructor
+  exacts[fun h => h.exists_lift, fun h => mk h]
+#align category_theory.comm_sq.has_lift.iff CategoryTheory.CommSq.HasLift.iff
+
+theorem iff_op : HasLift sq ↔ HasLift sq.op := by
+  rw [iff, iff]
+  exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun
+#align category_theory.comm_sq.has_lift.iff_op CategoryTheory.CommSq.HasLift.iff_op
+
+theorem iff_unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
+    (sq : CommSq f i p g) : HasLift sq ↔ HasLift sq.unop := by
+  rw [iff, iff]
+  exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun
+#align category_theory.comm_sq.has_lift.iff_unop CategoryTheory.CommSq.HasLift.iff_unop
+
+end HasLift
+
+/-- A choice of a diagonal morphism that is part of a `lift_struct` when
+the square has a lift. -/
+noncomputable def lift [hsq : HasLift sq] : B ⟶ X :=
+  hsq.exists_lift.some.l
+#align category_theory.comm_sq.lift CategoryTheory.CommSq.lift
+
+@[reassoc (attr := simp)]
+theorem fac_left [hsq : HasLift sq] : i ≫ sq.lift = f :=
+  hsq.exists_lift.some.fac_left
+#align category_theory.comm_sq.fac_left CategoryTheory.CommSq.fac_left
+
+@[reassoc (attr := simp)]
+theorem fac_right [hsq : HasLift sq] : sq.lift ≫ p = g :=
+  hsq.exists_lift.some.fac_right
+#align category_theory.comm_sq.fac_right CategoryTheory.CommSq.fac_right
+
+end CommSq
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Functor/EpiMono.lean b/Mathlib/CategoryTheory/Functor/EpiMono.lean
new file mode 100644
index 0000000000000..3c0d2c474c510
--- /dev/null
+++ b/Mathlib/CategoryTheory/Functor/EpiMono.lean
@@ -0,0 +1,356 @@
+/-
+Copyright (c) 2022 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+
+! This file was ported from Lean 3 source module category_theory.functor.epi_mono
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.EpiMono
+import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
+import Mathlib.CategoryTheory.LiftingProperties.Adjunction
+
+/-!
+# Preservation and reflection of monomorphisms and epimorphisms
+
+We provide typeclasses that state that a functor preserves or reflects monomorphisms or
+epimorphisms.
+-/
+
+
+open CategoryTheory
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+namespace CategoryTheory.Functor
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] {E : Type u₃}
+  [Category.{v₃} E]
+
+/-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms. -/
+class PreservesMonomorphisms (F : C ⥤ D) : Prop where
+  /-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms. -/
+  preserves : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], Mono (F.map f)
+#align category_theory.functor.preserves_monomorphisms CategoryTheory.Functor.PreservesMonomorphisms
+
+instance map_mono (F : C ⥤ D) [PreservesMonomorphisms F] {X Y : C} (f : X ⟶ Y) [Mono f] :
+    Mono (F.map f) :=
+  PreservesMonomorphisms.preserves f
+#align category_theory.functor.map_mono CategoryTheory.Functor.map_mono
+
+/-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms. -/
+class PreservesEpimorphisms (F : C ⥤ D) : Prop where
+  /-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms. -/
+  preserves : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], Epi (F.map f)
+#align category_theory.functor.preserves_epimorphisms CategoryTheory.Functor.PreservesEpimorphisms
+
+instance map_epi (F : C ⥤ D) [PreservesEpimorphisms F] {X Y : C} (f : X ⟶ Y) [Epi f] :
+    Epi (F.map f) :=
+  PreservesEpimorphisms.preserves f
+#align category_theory.functor.map_epi CategoryTheory.Functor.map_epi
+
+/-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves
+    monomorphisms. -/
+class ReflectsMonomorphisms (F : C ⥤ D) : Prop where
+   /-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves
+    monomorphisms. -/ 
+  reflects : ∀ {X Y : C} (f : X ⟶ Y), Mono (F.map f) → Mono f
+#align category_theory.functor.reflects_monomorphisms CategoryTheory.Functor.ReflectsMonomorphisms
+
+theorem mono_of_mono_map (F : C ⥤ D) [ReflectsMonomorphisms F] {X Y : C} {f : X ⟶ Y}
+    (h : Mono (F.map f)) : Mono f :=
+  ReflectsMonomorphisms.reflects f h
+#align category_theory.functor.mono_of_mono_map CategoryTheory.Functor.mono_of_mono_map
+
+/-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves
+    epimorphisms. -/
+class ReflectsEpimorphisms (F : C ⥤ D) : Prop where
+  /-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves
+      epimorphisms. -/
+  reflects : ∀ {X Y : C} (f : X ⟶ Y), Epi (F.map f) → Epi f
+#align category_theory.functor.reflects_epimorphisms CategoryTheory.Functor.ReflectsEpimorphisms
+
+theorem epi_of_epi_map (F : C ⥤ D) [ReflectsEpimorphisms F] {X Y : C} {f : X ⟶ Y}
+    (h : Epi (F.map f)) : Epi f :=
+  ReflectsEpimorphisms.reflects f h
+#align category_theory.functor.epi_of_epi_map CategoryTheory.Functor.epi_of_epi_map
+
+instance preservesMonomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [PreservesMonomorphisms F]
+    [PreservesMonomorphisms G] : PreservesMonomorphisms (F ⋙ G) where 
+  preserves f h := by
+    rw [comp_map]
+    exact inferInstance
+#align category_theory.functor.preserves_monomorphisms_comp CategoryTheory.Functor.preservesMonomorphisms_comp
+
+instance preservesEpimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [PreservesEpimorphisms F]
+    [PreservesEpimorphisms G] : PreservesEpimorphisms (F ⋙ G) where 
+  preserves f h := by
+    rw [comp_map]
+    exact inferInstance
+#align category_theory.functor.preserves_epimorphisms_comp CategoryTheory.Functor.preservesEpimorphisms_comp
+
+instance reflectsMonomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [ReflectsMonomorphisms F]
+    [ReflectsMonomorphisms G] : ReflectsMonomorphisms (F ⋙ G) where 
+  reflects _ h := F.mono_of_mono_map (G.mono_of_mono_map h)
+#align category_theory.functor.reflects_monomorphisms_comp CategoryTheory.Functor.reflectsMonomorphisms_comp
+
+instance reflectsEpimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [ReflectsEpimorphisms F]
+    [ReflectsEpimorphisms G] : ReflectsEpimorphisms (F ⋙ G) where 
+  reflects _ h := F.epi_of_epi_map (G.epi_of_epi_map h)
+#align category_theory.functor.reflects_epimorphisms_comp CategoryTheory.Functor.reflectsEpimorphisms_comp
+
+theorem preservesEpimorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+    [PreservesEpimorphisms (F ⋙ G)] [ReflectsEpimorphisms G] : PreservesEpimorphisms F :=
+  ⟨fun f _ => G.epi_of_epi_map <| show Epi ((F ⋙ G).map f) from inferInstance⟩
+#align category_theory.functor.preserves_epimorphisms_of_preserves_of_reflects CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects
+
+theorem preservesMonomorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+    [PreservesMonomorphisms (F ⋙ G)] [ReflectsMonomorphisms G] : PreservesMonomorphisms F :=
+  ⟨fun f _ => G.mono_of_mono_map <| show Mono ((F ⋙ G).map f) from inferInstance⟩
+#align category_theory.functor.preserves_monomorphisms_of_preserves_of_reflects CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects
+
+theorem reflectsEpimorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+    [PreservesEpimorphisms G] [ReflectsEpimorphisms (F ⋙ G)] : ReflectsEpimorphisms F :=
+  ⟨fun f _ => (F ⋙ G).epi_of_epi_map <| show Epi (G.map (F.map f)) from inferInstance⟩
+#align category_theory.functor.reflects_epimorphisms_of_preserves_of_reflects CategoryTheory.Functor.reflectsEpimorphisms_of_preserves_of_reflects
+
+theorem reflectsMonomorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+    [PreservesMonomorphisms G] [ReflectsMonomorphisms (F ⋙ G)] : ReflectsMonomorphisms F :=
+  ⟨fun f _ => (F ⋙ G).mono_of_mono_map <| show Mono (G.map (F.map f)) from inferInstance⟩
+#align category_theory.functor.reflects_monomorphisms_of_preserves_of_reflects CategoryTheory.Functor.reflectsMonomorphisms_of_preserves_of_reflects
+
+theorem preservesMonomorphisms.of_iso {F G : C ⥤ D} [PreservesMonomorphisms F] (α : F ≅ G) :
+    PreservesMonomorphisms G :=
+  {
+    preserves := fun {X} {Y} f h =>
+      by
+      haveI : Mono (F.map f ≫ (α.app Y).hom) := mono_comp _ _
+      convert (mono_comp _ _ : Mono ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom))
+      rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }
+#align category_theory.functor.preserves_monomorphisms.of_iso CategoryTheory.Functor.preservesMonomorphisms.of_iso
+
+theorem preservesMonomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
+    PreservesMonomorphisms F ↔ PreservesMonomorphisms G :=
+  ⟨fun _ => preservesMonomorphisms.of_iso α, fun _ => preservesMonomorphisms.of_iso α.symm⟩
+#align category_theory.functor.preserves_monomorphisms.iso_iff CategoryTheory.Functor.preservesMonomorphisms.iso_iff
+
+theorem preservesEpimorphisms.of_iso {F G : C ⥤ D} [PreservesEpimorphisms F] (α : F ≅ G) :
+    PreservesEpimorphisms G :=
+  {
+    preserves := fun {X} {Y} f h =>
+      by
+      haveI : Epi (F.map f ≫ (α.app Y).hom) := epi_comp _ _
+      convert (epi_comp _ _ : Epi ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom))
+      rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }
+#align category_theory.functor.preserves_epimorphisms.of_iso CategoryTheory.Functor.preservesEpimorphisms.of_iso
+
+theorem preservesEpimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
+    PreservesEpimorphisms F ↔ PreservesEpimorphisms G :=
+  ⟨fun _ => preservesEpimorphisms.of_iso α, fun _ => preservesEpimorphisms.of_iso α.symm⟩
+#align category_theory.functor.preserves_epimorphisms.iso_iff CategoryTheory.Functor.preservesEpimorphisms.iso_iff
+
+theorem reflectsMonomorphisms.of_iso {F G : C ⥤ D} [ReflectsMonomorphisms F] (α : F ≅ G) :
+    ReflectsMonomorphisms G :=
+  {
+    reflects := fun {X} {Y} f h => by
+      apply F.mono_of_mono_map
+      haveI : Mono (G.map f ≫ (α.app Y).inv) := mono_comp _ _
+      convert (mono_comp _ _ : Mono ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv))
+      rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }
+#align category_theory.functor.reflects_monomorphisms.of_iso CategoryTheory.Functor.reflectsMonomorphisms.of_iso
+
+theorem reflectsMonomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
+    ReflectsMonomorphisms F ↔ ReflectsMonomorphisms G :=
+  ⟨fun _ => reflectsMonomorphisms.of_iso α, fun _ => reflectsMonomorphisms.of_iso α.symm⟩
+#align category_theory.functor.reflects_monomorphisms.iso_iff CategoryTheory.Functor.reflectsMonomorphisms.iso_iff
+
+theorem reflectsEpimorphisms.of_iso {F G : C ⥤ D} [ReflectsEpimorphisms F] (α : F ≅ G) :
+    ReflectsEpimorphisms G :=
+  {
+    reflects := fun {X} {Y} f h => by
+      apply F.epi_of_epi_map
+      haveI : Epi (G.map f ≫ (α.app Y).inv) := epi_comp _ _
+      convert (epi_comp _ _ : Epi ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv))
+      rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }
+#align category_theory.functor.reflects_epimorphisms.of_iso CategoryTheory.Functor.reflectsEpimorphisms.of_iso
+
+theorem reflectsEpimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
+    ReflectsEpimorphisms F ↔ ReflectsEpimorphisms G :=
+  ⟨fun _ => reflectsEpimorphisms.of_iso α, fun _ => reflectsEpimorphisms.of_iso α.symm⟩
+#align category_theory.functor.reflects_epimorphisms.iso_iff CategoryTheory.Functor.reflectsEpimorphisms.iso_iff
+
+theorem preservesEpimorphsisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
+    PreservesEpimorphisms F :=
+  {
+    preserves := fun {X} {Y} f hf =>
+      ⟨by
+        intro Z g h H
+        replace H := congr_arg (adj.homEquiv X Z) H
+        rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
+          Equiv.apply_eq_iff_eq] at H⟩ }
+#align category_theory.functor.preserves_epimorphsisms_of_adjunction CategoryTheory.Functor.preservesEpimorphsisms_of_adjunction
+
+instance (priority := 100) preservesEpimorphisms_of_isLeftAdjoint (F : C ⥤ D) [IsLeftAdjoint F] :
+    PreservesEpimorphisms F :=
+  preservesEpimorphsisms_of_adjunction (Adjunction.ofLeftAdjoint F)
+#align category_theory.functor.preserves_epimorphisms_of_is_left_adjoint CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint
+
+theorem preservesMonomorphisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
+    PreservesMonomorphisms G :=
+  {
+    preserves := fun {X} {Y} f hf =>
+      ⟨by
+        intro Z g h H
+        replace H := congr_arg (adj.homEquiv Z Y).symm H
+        rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
+          Equiv.apply_eq_iff_eq] at H⟩ }
+#align category_theory.functor.preserves_monomorphisms_of_adjunction CategoryTheory.Functor.preservesMonomorphisms_of_adjunction
+
+instance (priority := 100) preservesMonomorphisms_of_isRightAdjoint (F : C ⥤ D) [IsRightAdjoint F] :
+    PreservesMonomorphisms F :=
+  preservesMonomorphisms_of_adjunction (Adjunction.ofRightAdjoint F)
+#align category_theory.functor.preserves_monomorphisms_of_is_right_adjoint CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint
+
+instance (priority := 100) reflectsMonomorphisms_of_faithful (F : C ⥤ D) [Faithful F] :
+    ReflectsMonomorphisms F
+    where reflects {X} {Y} f hf :=
+    ⟨fun {Z} g h hgh =>
+      F.map_injective ((cancel_mono (F.map f)).1 (by rw [← F.map_comp, hgh, F.map_comp]))⟩
+#align category_theory.functor.reflects_monomorphisms_of_faithful CategoryTheory.Functor.reflectsMonomorphisms_of_faithful
+
+instance (priority := 100) reflectsEpimorphisms_of_faithful (F : C ⥤ D) [Faithful F] :
+    ReflectsEpimorphisms F
+    where reflects {X} {Y} f hf :=
+    ⟨fun {Z} g h hgh =>
+      F.map_injective ((cancel_epi (F.map f)).1 (by rw [← F.map_comp, hgh, F.map_comp]))⟩
+#align category_theory.functor.reflects_epimorphisms_of_faithful CategoryTheory.Functor.reflectsEpimorphisms_of_faithful
+
+section
+
+variable (F : C ⥤ D) {X Y : C} (f : X ⟶ Y)
+
+/-- If `F` is a fully faithful functor, split epimorphisms are preserved and reflected by `F`. -/
+def splitEpiEquiv [Full F] [Faithful F] : SplitEpi f ≃ SplitEpi (F.map f)
+    where
+  toFun f := f.map F
+  invFun s := by
+    refine' ⟨F.preimage s.section_, _⟩
+    apply F.map_injective
+    simp only [map_comp, image_preimage, map_id]
+    apply SplitEpi.id
+  left_inv := by aesop_cat
+  right_inv := by 
+      simp only [Function.RightInverse,Function.LeftInverse]
+      intro x 
+      simp only [SplitEpi.map, preimage]
+      aesop_cat 
+#align category_theory.functor.split_epi_equiv CategoryTheory.Functor.splitEpiEquiv
+
+@[simp]
+theorem isSplitEpi_iff [Full F] [Faithful F] : IsSplitEpi (F.map f) ↔ IsSplitEpi f := by
+  constructor
+  · intro h
+    exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)
+  · intro h
+    exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)
+#align category_theory.functor.is_split_epi_iff CategoryTheory.Functor.isSplitEpi_iff
+
+/-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`. -/
+def splitMonoEquiv [Full F] [Faithful F] : SplitMono f ≃ SplitMono (F.map f)
+    where
+  toFun f := f.map F
+  invFun s := by
+    refine' ⟨F.preimage s.retraction, _⟩
+    apply F.map_injective
+    simp only [map_comp, image_preimage, map_id]
+    apply SplitMono.id
+  left_inv := by aesop_cat
+  right_inv := by 
+    simp only [Function.RightInverse, Function.LeftInverse]
+    intro x
+    simp only [SplitMono.map,preimage]
+    aesop_cat
+
+#align category_theory.functor.split_mono_equiv CategoryTheory.Functor.splitMonoEquiv
+
+@[simp]
+theorem isSplitMono_iff [Full F] [Faithful F] : IsSplitMono (F.map f) ↔ IsSplitMono f := by
+  constructor
+  · intro h
+    exact IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.some)
+  · intro h
+    exact IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)
+#align category_theory.functor.is_split_mono_iff CategoryTheory.Functor.isSplitMono_iff
+
+@[simp]
+theorem epi_map_iff_epi [hF₁ : PreservesEpimorphisms F] [hF₂ : ReflectsEpimorphisms F] :
+    Epi (F.map f) ↔ Epi f := by
+  constructor
+  · exact F.epi_of_epi_map
+  · intro h
+    exact F.map_epi f
+#align category_theory.functor.epi_map_iff_epi CategoryTheory.Functor.epi_map_iff_epi
+
+@[simp]
+theorem mono_map_iff_mono [hF₁ : PreservesMonomorphisms F] [hF₂ : ReflectsMonomorphisms F] :
+    Mono (F.map f) ↔ Mono f := by
+  constructor
+  · exact F.mono_of_mono_map
+  · intro h
+    exact F.map_mono f
+#align category_theory.functor.mono_map_iff_mono CategoryTheory.Functor.mono_map_iff_mono
+
+/-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `split_epi_category`,
+then `D` also is. -/
+def splitEpiCategoryImpOfIsEquivalence [IsEquivalence F] [SplitEpiCategory C] :
+    SplitEpiCategory D :=
+  ⟨fun {X} {Y} f => by
+    intro
+    rw [← F.inv.isSplitEpi_iff f]
+    apply isSplitEpi_of_epi⟩
+#align category_theory.functor.split_epi_category_imp_of_is_equivalence CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence
+
+end
+
+end CategoryTheory.Functor
+
+namespace CategoryTheory.Adjunction
+
+variable {C D : Type _} [Category C] [Category D] {F : C ⥤ D} {F' : D ⥤ C} {A B : C}
+
+theorem strongEpi_map_of_strongEpi (adj : F ⊣ F') (f : A ⟶ B) [h₁ : F'.PreservesMonomorphisms]
+    [h₂ : F.PreservesEpimorphisms] [StrongEpi f] : StrongEpi (F.map f) :=
+  ⟨inferInstance, fun X Y Z => by
+    intro
+    rw [adj.hasLiftingProperty_iff]
+    infer_instance⟩
+#align category_theory.adjunction.strong_epi_map_of_strong_epi CategoryTheory.Adjunction.strongEpi_map_of_strongEpi
+
+instance strongEpi_map_of_isEquivalence [IsEquivalence F] (f : A ⟶ B) [_h : StrongEpi f] :
+    StrongEpi (F.map f) :=
+  F.asEquivalence.toAdjunction.strongEpi_map_of_strongEpi f
+#align category_theory.adjunction.strong_epi_map_of_is_equivalence CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence
+
+end CategoryTheory.Adjunction
+
+namespace CategoryTheory.Functor
+
+variable {C D : Type _} [Category C] [Category D] {F : C ⥤ D} {A B : C} (f : A ⟶ B)
+
+@[simp]
+theorem strongEpi_map_iff_strongEpi_of_isEquivalence [IsEquivalence F] :
+    StrongEpi (F.map f) ↔ StrongEpi f := by
+  constructor
+  · intro
+    have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
+      Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
+    rw [StrongEpi.iff_of_arrow_iso e]
+    infer_instance
+  · intro
+    infer_instance
+#align category_theory.functor.strong_epi_map_iff_strong_epi_of_is_equivalence CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence
+
+end CategoryTheory.Functor
+
diff --git a/Mathlib/CategoryTheory/Functor/ReflectsIso.lean b/Mathlib/CategoryTheory/Functor/ReflectsIso.lean
new file mode 100644
index 0000000000000..34192a02d8c1d
--- /dev/null
+++ b/Mathlib/CategoryTheory/Functor/ReflectsIso.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2020 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+
+! This file was ported from Lean 3 source module category_theory.functor.reflects_isomorphisms
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Balanced
+import Mathlib.CategoryTheory.Functor.EpiMono
+import Mathlib.CategoryTheory.Functor.FullyFaithful
+
+/-!
+# Functors which reflect isomorphisms
+
+A functor `F` reflects isomorphisms if whenever `F.map f` is an isomorphism, `f` was too.
+
+It is formalized as a `Prop` valued typeclass `ReflectsIsomorphisms F`.
+
+Any fully faithful functor reflects isomorphisms.
+-/
+
+
+open CategoryTheory CategoryTheory.Functor
+
+namespace CategoryTheory
+
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+section ReflectsIso
+
+variable {D : Type u₂} [Category.{v₂} D]
+
+variable {E : Type u₃} [Category.{v₃} E]
+
+/-- Define what it means for a functor `F : C ⥤ D` to reflect isomorphisms: for any
+morphism `f : A ⟶ B`, if `F.map f` is an isomorphism then `f` is as well.
+Note that we do not assume or require that `F` is faithful.
+-/
+class ReflectsIsomorphisms (F : C ⥤ D) : Prop where
+  /-- For any `f`, if `F.map f` is an iso, then so was `f`-/
+  reflects : ∀ {A B : C} (f : A ⟶ B) [IsIso (F.map f)], IsIso f
+#align category_theory.reflects_isomorphisms CategoryTheory.ReflectsIsomorphisms
+
+/-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso. -/
+theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.map f)]
+    [ReflectsIsomorphisms F] : IsIso f :=
+  ReflectsIsomorphisms.reflects F f
+#align category_theory.is_iso_of_reflects_iso CategoryTheory.isIso_of_reflects_iso
+
+instance (priority := 100) of_full_and_faithful (F : C ⥤ D) [Full F] [Faithful F] :
+    ReflectsIsomorphisms F
+    where reflects f i :=
+    ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩
+#align category_theory.of_full_and_faithful CategoryTheory.of_full_and_faithful
+
+instance (F : C ⥤ D) (G : D ⥤ E) [ReflectsIsomorphisms F] [ReflectsIsomorphisms G] :
+    ReflectsIsomorphisms (F ⋙ G) :=
+  ⟨fun f (hf : IsIso (G.map _)) => by
+    skip
+    haveI := isIso_of_reflects_iso (F.map f) G
+    exact isIso_of_reflects_iso f F⟩
+
+instance (priority := 100) reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
+    [Balanced C] (F : C ⥤ D) [ReflectsMonomorphisms F] [ReflectsEpimorphisms F] :
+    ReflectsIsomorphisms F where 
+  reflects f hf := by
+    skip
+    haveI : Epi f := epi_of_epi_map F inferInstance
+    haveI : Mono f := mono_of_mono_map F inferInstance
+    exact isIso_of_mono_of_epi f
+#align category_theory.reflects_isomorphisms_of_reflects_monomorphisms_of_reflects_epimorphisms CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
+
+end ReflectsIso
+
+end CategoryTheory
+
diff --git a/Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean b/Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
new file mode 100644
index 0000000000000..39edcc3687f81
--- /dev/null
+++ b/Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean
@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2022 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+
+! This file was ported from Lean 3 source module category_theory.lifting_properties.adjunction
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.LiftingProperties.Basic
+import Mathlib.CategoryTheory.Adjunction.Basic
+
+/-!
+
+# Lifting properties and adjunction
+
+In this file, we obtain `Adjunction.HasLiftingProperty_iff`, which states
+that when we have an adjunction `adj : G ⊣ F` between two functors `G : C ⥤ D`
+and `F : D ⥤ C`, then a morphism of the form `G.map i` has the left lifting
+property in `D` with respect to a morphism `p` if and only the morphism `i`
+has the left lifting property in `C` with respect to `F.map p`.
+
+-/
+
+
+namespace CategoryTheory
+
+open Category
+
+variable {C D : Type _} [Category C] [Category D] {G : C ⥤ D} {F : D ⥤ C}
+
+namespace CommSq
+
+section
+
+variable {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y}
+  (sq : CommSq u (G.map i) p v) (adj : G ⊣ F)
+
+/-- When we have an adjunction `G ⊣ F`, any commutative square where the left
+map is of the form `G.map i` and the right map is `p` has an "adjoint" commutative
+square whose left map is `i` and whose right map is `F.map p`. -/
+theorem right_adjoint : CommSq (adj.homEquiv _ _ u) i (F.map p) (adj.homEquiv _ _ v) :=
+  ⟨by
+    simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
+    rw [F.map_comp, Adjunction.unit_naturality_assoc]⟩
+#align category_theory.comm_sq.right_adjoint CategoryTheory.CommSq.right_adjoint
+
+/-- The liftings of a commutative are in bijection with the liftings of its (right)
+adjoint square. -/
+def rightAdjointLiftStructEquiv : sq.LiftStruct ≃ (sq.right_adjoint adj).LiftStruct
+    where
+  toFun l :=
+    { l := adj.homEquiv _ _ l.l
+      fac_left := by rw [← adj.homEquiv_naturality_left, l.fac_left]
+      fac_right := by rw [← Adjunction.homEquiv_naturality_right, l.fac_right] }
+  invFun l :=
+    { l := (adj.homEquiv _ _).symm l.l
+      fac_left := by
+        rw [← Adjunction.homEquiv_naturality_left_symm, l.fac_left]
+        apply (adj.homEquiv _ _).left_inv
+      fac_right := by
+        rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]
+        apply (adj.homEquiv _ _).left_inv }
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
+#align category_theory.comm_sq.right_adjoint_lift_struct_equiv CategoryTheory.CommSq.rightAdjointLiftStructEquiv
+
+/-- A square has a lifting if and only if its (right) adjoint square has a lifting. -/
+theorem right_adjoint_hasLift_iff : HasLift (sq.right_adjoint adj) ↔ HasLift sq := by
+  simp only [HasLift.iff]
+  exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm
+#align category_theory.comm_sq.right_adjoint_has_lift_iff CategoryTheory.CommSq.right_adjoint_hasLift_iff
+
+instance [HasLift sq] : HasLift (sq.right_adjoint adj) := by
+  rw [right_adjoint_hasLift_iff]
+  infer_instance
+
+end
+
+section
+
+variable {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y}
+  (sq : CommSq u i (F.map p) v) (adj : G ⊣ F)
+
+/-- When we have an adjunction `G ⊣ F`, any commutative square where the left
+map is of the form `i` and the right map is `F.map p` has an "adjoint" commutative
+square whose left map is `G.map i` and whose right map is `p`. -/
+theorem left_adjoint : CommSq ((adj.homEquiv _ _).symm u) (G.map i) p ((adj.homEquiv _ _).symm v) :=
+  ⟨by
+    simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
+    rw [G.map_comp, assoc, Adjunction.counit_naturality]⟩
+#align category_theory.comm_sq.left_adjoint CategoryTheory.CommSq.left_adjoint
+
+/-- The liftings of a commutative are in bijection with the liftings of its (left)
+adjoint square. -/
+def leftAdjointLiftStructEquiv : sq.LiftStruct ≃ (sq.left_adjoint adj).LiftStruct
+    where
+  toFun l :=
+    { l := (adj.homEquiv _ _).symm l.l
+      fac_left := by rw [← adj.homEquiv_naturality_left_symm, l.fac_left]
+      fac_right := by rw [← adj.homEquiv_naturality_right_symm, l.fac_right] }
+  invFun l :=
+    { l := (adj.homEquiv _ _) l.l
+      fac_left := by
+        rw [← adj.homEquiv_naturality_left, l.fac_left]
+        apply (adj.homEquiv _ _).right_inv
+      fac_right := by
+        rw [← adj.homEquiv_naturality_right, l.fac_right]
+        apply (adj.homEquiv _ _).right_inv }
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
+#align category_theory.comm_sq.left_adjoint_lift_struct_equiv CategoryTheory.CommSq.leftAdjointLiftStructEquiv
+
+/-- A (left) adjoint square has a lifting if and only if the original square has a lifting. -/
+theorem left_adjoint_hasLift_iff : HasLift (sq.left_adjoint adj) ↔ HasLift sq := by
+  simp only [HasLift.iff]
+  exact Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm
+#align category_theory.comm_sq.left_adjoint_has_lift_iff CategoryTheory.CommSq.left_adjoint_hasLift_iff
+
+instance [HasLift sq] : HasLift (sq.left_adjoint adj) := by
+  rw [left_adjoint_hasLift_iff]
+  infer_instance
+
+end
+
+end CommSq
+
+namespace Adjunction
+
+theorem hasLiftingProperty_iff (adj : G ⊣ F) {A B : C} {X Y : D} (i : A ⟶ B) (p : X ⟶ Y) :
+    HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p) := by
+  constructor <;> intro <;> constructor <;> intro f g sq
+  · rw [← sq.left_adjoint_hasLift_iff adj]
+    infer_instance
+  · rw [← sq.right_adjoint_hasLift_iff adj]
+    infer_instance
+#align category_theory.adjunction.has_lifting_property_iff CategoryTheory.Adjunction.hasLiftingProperty_iff
+
+end Adjunction
+
+end CategoryTheory
+
diff --git a/Mathlib/CategoryTheory/LiftingProperties/Basic.lean b/Mathlib/CategoryTheory/LiftingProperties/Basic.lean
new file mode 100644
index 0000000000000..7fc094780277e
--- /dev/null
+++ b/Mathlib/CategoryTheory/LiftingProperties/Basic.lean
@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2021 Jakob Scholbach. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jakob Scholbach, Joël Riou
+
+! This file was ported from Lean 3 source module category_theory.lifting_properties.basic
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.CommSq
+
+/-!
+# Lifting properties
+
+This file defines the lifting property of two morphisms in a category and
+shows basic properties of this notion.
+
+## Main results
+- `HasLiftingProperty`: the definition of the lifting property
+
+## Tags
+lifting property
+
+@TODO :
+1) define llp/rlp with respect to a `morphism_property`
+2) retracts, direct/inverse images, (co)products, adjunctions
+
+-/
+
+
+universe v
+
+namespace CategoryTheory
+
+open Category
+
+variable {C : Type _} [Category C] {A B B' X Y Y' : C} (i : A ⟶ B) (i' : B ⟶ B') (p : X ⟶ Y)
+  (p' : Y ⟶ Y')
+
+/-- `HasLiftingProperty i p` means that `i` has the left lifting
+property with respect to `p`, or equivalently that `p` has
+the right lifting property with respect to `i`. -/
+class HasLiftingProperty : Prop where
+  /-- Unique field expressing the any commutative square built from `f` and `g` has a lift -/
+  sq_hasLift : ∀ {f : A ⟶ X} {g : B ⟶ Y} (sq : CommSq f i p g), sq.HasLift
+#align category_theory.has_lifting_property CategoryTheory.HasLiftingProperty
+#align category_theory.has_lifting_property.sq_has_lift CategoryTheory.HasLiftingProperty.sq_hasLift
+
+instance (priority := 100) sq_hasLift_of_hasLiftingProperty {f : A ⟶ X} {g : B ⟶ Y}
+    (sq : CommSq f i p g) [hip : HasLiftingProperty i p] : sq.HasLift := by apply hip.sq_hasLift
+#align category_theory.sq_has_lift_of_has_lifting_property CategoryTheory.sq_hasLift_of_hasLiftingProperty
+
+namespace HasLiftingProperty
+
+variable {i p}
+
+theorem op (h : HasLiftingProperty i p) : HasLiftingProperty p.op i.op :=
+  ⟨fun {f} {g} sq => by
+    simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
+    infer_instance⟩
+#align category_theory.has_lifting_property.op CategoryTheory.HasLiftingProperty.op
+
+theorem unop {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) :
+    HasLiftingProperty p.unop i.unop :=
+  ⟨fun {f} {g} sq => by
+    rw [CommSq.HasLift.iff_op]
+    simp only [Quiver.Hom.op_unop]
+    infer_instance⟩
+#align category_theory.has_lifting_property.unop CategoryTheory.HasLiftingProperty.unop
+
+theorem iff_op : HasLiftingProperty i p ↔ HasLiftingProperty p.op i.op :=
+  ⟨op, unop⟩
+#align category_theory.has_lifting_property.iff_op CategoryTheory.HasLiftingProperty.iff_op
+
+theorem iff_unop {A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y) :
+    HasLiftingProperty i p ↔ HasLiftingProperty p.unop i.unop :=
+  ⟨unop, op⟩
+#align category_theory.has_lifting_property.iff_unop CategoryTheory.HasLiftingProperty.iff_unop
+
+variable (i p)
+
+instance (priority := 100) of_left_iso [IsIso i] : HasLiftingProperty i p :=
+  ⟨fun {f} {g} sq =>
+    CommSq.HasLift.mk'
+      { l := inv i ≫ f
+        fac_left := by simp only [IsIso.hom_inv_id_assoc]
+        fac_right := by simp only [sq.w, assoc, IsIso.inv_hom_id_assoc] }⟩
+#align category_theory.has_lifting_property.of_left_iso CategoryTheory.HasLiftingProperty.of_left_iso
+
+instance (priority := 100) of_right_iso [IsIso p] : HasLiftingProperty i p :=
+  ⟨fun {f} {g} sq =>
+    CommSq.HasLift.mk'
+      { l := g ≫ inv p
+        fac_left := by simp only [← sq.w_assoc, IsIso.hom_inv_id, comp_id]
+        fac_right := by simp only [assoc, IsIso.inv_hom_id, comp_id] }⟩
+#align category_theory.has_lifting_property.of_right_iso CategoryTheory.HasLiftingProperty.of_right_iso
+
+instance of_comp_left [HasLiftingProperty i p] [HasLiftingProperty i' p] :
+    HasLiftingProperty (i ≫ i') p :=
+  ⟨fun {f} {g} sq => by
+    have fac := sq.w
+    rw [assoc] at fac
+    exact
+      CommSq.HasLift.mk'
+        { l := (CommSq.mk (CommSq.mk fac).fac_right).lift
+          fac_left := by simp only [assoc, CommSq.fac_left]
+          fac_right := by simp only [CommSq.fac_right] }⟩
+#align category_theory.has_lifting_property.of_comp_left CategoryTheory.HasLiftingProperty.of_comp_left
+
+instance of_comp_right [HasLiftingProperty i p] [HasLiftingProperty i p'] :
+    HasLiftingProperty i (p ≫ p') :=
+  ⟨fun {f} {g} sq => by
+    have fac := sq.w
+    rw [← assoc] at fac
+    let _ := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
+    exact
+      CommSq.HasLift.mk'
+        { l := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
+          fac_left := by simp only [CommSq.fac_left]
+          fac_right := by simp only [CommSq.fac_right_assoc, CommSq.fac_right] }⟩
+#align category_theory.has_lifting_property.of_comp_right CategoryTheory.HasLiftingProperty.of_comp_right
+
+theorem of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
+    (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) [hip : HasLiftingProperty i p] :
+    HasLiftingProperty i' p := by
+  rw [Arrow.iso_w' e]
+  infer_instance
+#align category_theory.has_lifting_property.of_arrow_iso_left CategoryTheory.HasLiftingProperty.of_arrow_iso_left
+
+theorem of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
+    (e : Arrow.mk p ≅ Arrow.mk p') [hip : HasLiftingProperty i p] : HasLiftingProperty i p' := by
+  rw [Arrow.iso_w' e]
+  infer_instance
+#align category_theory.has_lifting_property.of_arrow_iso_right CategoryTheory.HasLiftingProperty.of_arrow_iso_right
+
+theorem iff_of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
+    (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) : HasLiftingProperty i p ↔ HasLiftingProperty i' p :=
+  by
+  constructor <;> intro
+  exacts[of_arrow_iso_left e p, of_arrow_iso_left e.symm p]
+#align category_theory.has_lifting_property.iff_of_arrow_iso_left CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left
+
+theorem iff_of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
+    (e : Arrow.mk p ≅ Arrow.mk p') : HasLiftingProperty i p ↔ HasLiftingProperty i p' := by
+  constructor <;> intro
+  exacts[of_arrow_iso_right i e, of_arrow_iso_right i e.symm]
+#align category_theory.has_lifting_property.iff_of_arrow_iso_right CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right
+
+end HasLiftingProperty
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
new file mode 100644
index 0000000000000..a71d94949664b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
@@ -0,0 +1,249 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+
+! This file was ported from Lean 3 source module category_theory.limits.shapes.strong_epi
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Balanced
+import Mathlib.CategoryTheory.LiftingProperties.Basic
+
+/-!
+# Strong epimorphisms
+
+In this file, we define strong epimorphisms. A strong epimorphism is an epimorphism `f`
+which has the (unique) left lifting property with respect to monomorphisms. Similarly,
+a strong monomorphisms in a monomorphism which has the (unique) right lifting property
+with respect to epimorphisms.
+
+## Main results
+
+Besides the definition, we show that
+* the composition of two strong epimorphisms is a strong epimorphism,
+* if `f ≫ g` is a strong epimorphism, then so is `g`,
+* if `f` is both a strong epimorphism and a monomorphism, then it is an isomorphism
+
+We also define classes `strong_mono_category` and `strong_epi_category` for categories in which
+every monomorphism or epimorphism is strong, and deduce that these categories are balanced.
+
+## TODO
+
+Show that the dual of a strong epimorphism is a strong monomorphism, and vice versa.
+
+## References
+
+* [F. Borceux, *Handbook of Categorical Algebra 1*][borceux-vol1]
+-/
+
+
+universe v u
+
+namespace CategoryTheory
+
+variable {C : Type u} [Category.{v} C]
+
+variable {P Q : C}
+
+/-- A strong epimorphism `f` is an epimorphism which has the left lifting property
+with respect to monomorphisms. -/
+class StrongEpi (f : P ⟶ Q) : Prop where
+  /-- The epimorphism condition on `f` -/
+  epi : Epi f
+  /-- The left lifting property with respect to all monomorphism -/
+  llp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Mono z], HasLiftingProperty f z
+#align category_theory.strong_epi CategoryTheory.StrongEpi
+#align category_theory.strong_epi.epi CategoryTheory.StrongEpi.epi
+
+
+theorem StrongEpi.mk' {f : P ⟶ Q} [Epi f]
+    (hf : ∀ (X Y : C) (z : X ⟶ Y) 
+      (_ : Mono z) (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v), sq.HasLift) :
+    StrongEpi f :=
+  { epi := inferInstance
+    llp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩ }
+#align category_theory.strong_epi.mk' CategoryTheory.StrongEpi.mk'
+
+/-- A strong monomorphism `f` is a monomorphism which has the right lifting property
+with respect to epimorphisms. -/
+class StrongMono (f : P ⟶ Q) : Prop where
+  /-- The monomorphism condition on `f` -/
+  mono : Mono f
+  /-- The right lifting property with respect to all epimorphisms -/
+  rlp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Epi z], HasLiftingProperty z f
+#align category_theory.strong_mono CategoryTheory.StrongMono
+
+theorem StrongMono.mk' {f : P ⟶ Q} [Mono f]
+    (hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Epi z) (u : X ⟶ P) 
+    (v : Y ⟶ Q) (sq : CommSq u z f v), sq.HasLift) : StrongMono f where
+  mono := inferInstance
+  rlp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩
+#align category_theory.strong_mono.mk' CategoryTheory.StrongMono.mk'
+
+attribute [instance] StrongEpi.llp
+
+attribute [instance] StrongMono.rlp
+
+instance (priority := 100) epi_of_strongEpi (f : P ⟶ Q) [StrongEpi f] : Epi f :=
+  StrongEpi.epi
+#align category_theory.epi_of_strong_epi CategoryTheory.epi_of_strongEpi
+
+instance (priority := 100) mono_of_strongMono (f : P ⟶ Q) [StrongMono f] : Mono f :=
+  StrongMono.mono
+#align category_theory.mono_of_strong_mono CategoryTheory.mono_of_strongMono
+
+section
+
+variable {R : C} (f : P ⟶ Q) (g : Q ⟶ R)
+
+/-- The composition of two strong epimorphisms is a strong epimorphism. -/
+theorem strongEpi_comp [StrongEpi f] [StrongEpi g] : StrongEpi (f ≫ g) :=
+  { epi := epi_comp _ _
+    llp := by
+      intros
+      infer_instance }
+#align category_theory.strong_epi_comp CategoryTheory.strongEpi_comp
+
+/-- The composition of two strong monomorphisms is a strong monomorphism. -/
+theorem strongMono_comp [StrongMono f] [StrongMono g] : StrongMono (f ≫ g) :=
+  { mono := mono_comp _ _
+    rlp := by
+      intros
+      infer_instance }
+#align category_theory.strong_mono_comp CategoryTheory.strongMono_comp
+
+/-- If `f ≫ g` is a strong epimorphism, then so is `g`. -/
+theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
+  { epi := epi_of_epi f g
+    llp := fun {X} {Y} z _ => by
+      constructor
+      intro u v sq
+      have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
+      exact
+        CommSq.HasLift.mk'
+          ⟨(CommSq.mk h₀).lift, by
+            simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩ }
+#align category_theory.strong_epi_of_strong_epi CategoryTheory.strongEpi_of_strongEpi
+
+/-- If `f ≫ g` is a strong monomorphism, then so is `f`. -/
+theorem strongMono_of_strongMono [StrongMono (f ≫ g)] : StrongMono f :=
+  { mono := mono_of_mono f g
+    rlp := fun {X} {Y} z => by
+      intros
+      constructor
+      intro u v sq
+      have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by 
+        rw [←Category.assoc, eq_whisker sq.w, Category.assoc]
+      exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩ }
+#align category_theory.strong_mono_of_strong_mono CategoryTheory.strongMono_of_strongMono
+
+/-- An isomorphism is in particular a strong epimorphism. -/
+instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f
+    where
+  epi := by infer_instance
+  llp {X} {Y} z := HasLiftingProperty.of_left_iso _ _
+#align category_theory.strong_epi_of_is_iso CategoryTheory.strongEpi_of_isIso
+
+/-- An isomorphism is in particular a strong monomorphism. -/
+instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f
+    where
+  mono := by infer_instance
+  rlp {X} {Y} z := HasLiftingProperty.of_right_iso _ _
+#align category_theory.strong_mono_of_is_iso CategoryTheory.strongMono_of_isIso
+
+theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+    (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongEpi f] : StrongEpi g :=
+  { epi := by
+      rw [Arrow.iso_w' e]
+      haveI := epi_comp f e.hom.right
+      apply epi_comp
+    llp := fun {X} {Y} z => by
+      intro
+      apply HasLiftingProperty.of_arrow_iso_left e z }
+#align category_theory.strong_epi.of_arrow_iso CategoryTheory.StrongEpi.of_arrow_iso
+
+theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+    (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongMono f] : StrongMono g :=
+  { mono := by
+      rw [Arrow.iso_w' e]
+      haveI := mono_comp f e.hom.right
+      apply mono_comp
+    rlp := fun {X} {Y} z => by
+      intro
+      apply HasLiftingProperty.of_arrow_iso_right z e }
+#align category_theory.strong_mono.of_arrow_iso CategoryTheory.StrongMono.of_arrow_iso
+
+theorem StrongEpi.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+    (e : Arrow.mk f ≅ Arrow.mk g) : StrongEpi f ↔ StrongEpi g := by
+  constructor <;> intro
+  exacts[StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]
+#align category_theory.strong_epi.iff_of_arrow_iso CategoryTheory.StrongEpi.iff_of_arrow_iso
+
+theorem StrongMono.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+    (e : Arrow.mk f ≅ Arrow.mk g) : StrongMono f ↔ StrongMono g := by
+  constructor <;> intro
+  exacts[StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]
+#align category_theory.strong_mono.iff_of_arrow_iso CategoryTheory.StrongMono.iff_of_arrow_iso
+
+end
+
+/-- A strong epimorphism that is a monomorphism is an isomorphism. -/
+theorem isIso_of_mono_of_strongEpi (f : P ⟶ Q) [Mono f] [StrongEpi f] : IsIso f :=
+  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by aesop_cat⟩⟩
+#align category_theory.is_iso_of_mono_of_strong_epi CategoryTheory.isIso_of_mono_of_strongEpi
+
+/-- A strong monomorphism that is an epimorphism is an isomorphism. -/
+theorem isIso_of_epi_of_strongMono (f : P ⟶ Q) [Epi f] [StrongMono f] : IsIso f :=
+  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by aesop_cat⟩⟩
+#align category_theory.is_iso_of_epi_of_strong_mono CategoryTheory.isIso_of_epi_of_strongMono
+
+section
+
+variable (C)
+
+/-- A strong epi category is a category in which every epimorphism is strong. -/
+class StrongEpiCategory : Prop where
+  /-- A strong epi category is a category in which every epimorphism is strong. -/
+  strongEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], StrongEpi f
+#align category_theory.strong_epi_category CategoryTheory.StrongEpiCategory
+
+/-- A strong mono category is a category in which every monomorphism is strong. -/
+class StrongMonoCategory : Prop where
+  /-- A strong mono category is a category in which every monomorphism is strong. -/
+  strongMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], StrongMono f
+#align category_theory.strong_mono_category CategoryTheory.StrongMonoCategory
+
+end
+
+theorem strongEpi_of_epi [StrongEpiCategory C] (f : P ⟶ Q) [Epi f] : StrongEpi f :=
+  StrongEpiCategory.strongEpi_of_epi _
+#align category_theory.strong_epi_of_epi CategoryTheory.strongEpi_of_epi
+
+theorem strongMono_of_mono [StrongMonoCategory C] (f : P ⟶ Q) [Mono f] : StrongMono f :=
+  StrongMonoCategory.strongMono_of_mono _
+#align category_theory.strong_mono_of_mono CategoryTheory.strongMono_of_mono
+
+section
+
+attribute [local instance] strongEpi_of_epi
+
+instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C
+    where isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _
+#align category_theory.balanced_of_strong_epi_category CategoryTheory.balanced_of_strongEpiCategory
+
+end
+
+section
+
+attribute [local instance] strongMono_of_mono
+
+instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C
+    where isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _
+#align category_theory.balanced_of_strong_mono_category CategoryTheory.balanced_of_strongMonoCategory
+
+end
+
+end CategoryTheory
+#lint
diff --git a/scripts/start_port-macos.sh b/scripts/start_port-macos.sh
new file mode 100755
index 0000000000000..da56887ff18fb
--- /dev/null
+++ b/scripts/start_port-macos.sh
@@ -0,0 +1,86 @@
+#!/usr/bin/env bash
+
+set -e
+
+if [ ! -d Mathlib ] ; then
+    echo "No Mathlib/ directory; are you at the root of the mathlib4 repo?"
+    exit 1
+fi
+
+if [ ! $1 ] ; then
+    echo "usage: ./scripts/start_port.sh Mathlib/Foo/Bar/Baz.lean"
+    exit 1
+fi
+
+case $1 in
+    Mathlib/*) true ;;
+    *) echo "argument must begin with Mathlib/"
+       exit 1 ;;
+esac
+
+if [ -f $1 ] ; then
+    echo "file already exists"
+    exit 1
+fi
+
+set -x
+set -o pipefail
+
+MATHLIB3PORT_BASE_URL=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master
+PORT_STATUS_YAML=https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+TMP_FILE=start_port_tmp.lean
+
+mathlib4_path=$1
+mathlib4_mod=$(basename $(echo "$mathlib4_path" | tr / .) .lean)
+
+mathlib3port_url=$MATHLIB3PORT_BASE_URL/Mathbin/${1#Mathlib/}
+
+curl --silent --show-error --fail -o "$TMP_FILE" "$mathlib3port_url"
+
+mathlib3_module=$(grep '^! .*source module ' <"$TMP_FILE" | gsed 's/.*source module \(.*\)$/\1/')
+
+if curl --silent --show-error --fail "$PORT_STATUS_YAML" | grep -F "$mathlib3_module: " | grep "mathlib4#" ; then
+    set +x
+    echo "WARNING: The file is already in the process of being ported."
+    echo "(See line above for PR number.)"
+    rm "$TMP_FILE"
+    exit 1
+fi
+
+mkdir -p $(dirname "$mathlib4_path")
+mv "$TMP_FILE" "$mathlib4_path"
+
+git fetch
+mathlib4_mod_tail=${mathlib4_mod#Mathlib.}
+branch_name=port/${mathlib4_mod_tail}
+git checkout --no-track -b "$branch_name" origin/master
+
+# Empty commit with nice title. Ugsed by gh and hub to suggest PR title.
+git commit -m "feat: port $mathlib4_mod_tail" --allow-empty
+
+git add "$mathlib4_path"
+git commit -m 'Initial file copy from mathport'
+
+gsed -i 's/Mathbin\./Mathlib\./g' "$mathlib4_path"
+gsed -i '/^import/{s/[.]Gcd/.GCD/g; s/[.]Modeq/.ModEq/g; s/[.]Nary/.NAry/g; s/[.]Peq/.PEq/g; s/[.]Pfun/.PFun/g; s/[.]Pnat/.PNat/g; s/[.]Smul/.SMul/g; s/[.]Zmod/.ZMod/g}' "$mathlib4_path"
+
+# gawk script taken from https://github.com/leanprover-community/mathlib4/pull/1523
+gawk '{do {{if (match($0, "^  by$") && length(p) < 98 && (!(match(p, "^[ \t]*--.*$")))) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}' "$mathlib4_path" > "$mathlib4_path.tmp"
+mv "$mathlib4_path.tmp" "$mathlib4_path"
+
+(echo "import $mathlib4_mod" ; cat Mathlib.lean) | LC_ALL=C sort | uniq > Mathlib.lean.tmp
+mv -f Mathlib.lean.tmp Mathlib.lean
+
+git add Mathlib.lean "$mathlib4_path"
+git commit \
+	-m 'automated fixes' \
+	-m '' \
+	-m 'Mathbin -> Mathlib' \
+	-m 'fix certain import statements' \
+	-m 'move "by" to end of line' \
+	-m 'add import to Mathlib.lean'
+
+set +x
+
+echo "After pushing, you can open a PR at:"
+echo "https://github.com/leanprover-community/mathlib4/compare/$branch_name?expand=1&title=feat:+port+$mathlib4_mod_tail&labels=mathlib-port"