diff --git a/Mathlib.lean b/Mathlib.lean
index 58cfceb753602..356a0330c621e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -225,6 +225,7 @@ import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.RelCat
 import Mathlib.CategoryTheory.Comma
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
+import Mathlib.CategoryTheory.EpiMono
 import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Equivalence
 import Mathlib.CategoryTheory.EssentialImage
@@ -236,7 +237,9 @@ import Mathlib.CategoryTheory.Functor.Currying
 import Mathlib.CategoryTheory.Functor.Default
 import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
+import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.InvIsos
+import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
@@ -247,6 +250,7 @@ import Mathlib.CategoryTheory.Products.Basic
 import Mathlib.CategoryTheory.Products.Bifunctor
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Thin
+import Mathlib.CategoryTheory.Types
 import Mathlib.CategoryTheory.Whiskering
 import Mathlib.CategoryTheory.Yoneda
 import Mathlib.Combinatorics.Additive.Energy
diff --git a/Mathlib/CategoryTheory/EpiMono.lean b/Mathlib/CategoryTheory/EpiMono.lean
new file mode 100644
index 0000000000000..565bbbeb662d2
--- /dev/null
+++ b/Mathlib/CategoryTheory/EpiMono.lean
@@ -0,0 +1,275 @@
+/-
+Copyright (c) 2019 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton, Scott Morrison
+
+! This file was ported from Lean 3 source module category_theory.epi_mono
+! leanprover-community/mathlib commit 48085f140e684306f9e7da907cd5932056d1aded
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Opposites
+import Mathlib.CategoryTheory.Groupoid
+
+/-!
+# Facts about epimorphisms and monomorphisms.
+
+The definitions of `Epi` and `Mono` are in `CategoryTheory.Category`,
+since they are used by some lemmas for `Iso`, which is used everywhere.
+-/
+
+
+universe v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+instance unop_mono_of_epi {A B : Cᵒᵖ} (f : A ⟶ B) [Epi f] : Mono f.unop :=
+  ⟨fun _ _ eq => Quiver.Hom.op_inj ((cancel_epi f).1 (Quiver.Hom.unop_inj eq))⟩
+#align category_theory.unop_mono_of_epi CategoryTheory.unop_mono_of_epi
+
+instance unop_epi_of_mono {A B : Cᵒᵖ} (f : A ⟶ B) [Mono f] : Epi f.unop :=
+  ⟨fun _ _ eq => Quiver.Hom.op_inj ((cancel_mono f).1 (Quiver.Hom.unop_inj eq))⟩
+#align category_theory.unop_epi_of_mono CategoryTheory.unop_epi_of_mono
+
+instance op_mono_of_epi {A B : C} (f : A ⟶ B) [Epi f] : Mono f.op :=
+  ⟨fun _ _ eq => Quiver.Hom.unop_inj ((cancel_epi f).1 (Quiver.Hom.op_inj eq))⟩
+#align category_theory.op_mono_of_epi CategoryTheory.op_mono_of_epi
+
+instance op_epi_of_mono {A B : C} (f : A ⟶ B) [Mono f] : Epi f.op :=
+  ⟨fun _ _ eq => Quiver.Hom.unop_inj ((cancel_mono f).1 (Quiver.Hom.op_inj eq))⟩
+#align category_theory.op_epi_of_mono CategoryTheory.op_epi_of_mono
+
+/-- A split monomorphism is a morphism `f : X ⟶ Y` with a given retraction `retraction f : Y ⟶ X`
+such that `f ≫ retraction f = 𝟙 X`.
+
+Every split monomorphism is a monomorphism.
+-/
+/- Porting note: @[nolint has_nonempty_instance] -/
+/- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule -/
+@[aesop apply safe (rule_sets [CategoryTheory])]
+structure SplitMono {X Y : C} (f : X ⟶ Y) where
+  /-- The map splitting `f` -/
+  retraction : Y ⟶ X
+  /-- `f` composed with `retraction` is the identity -/
+  id : f ≫ retraction = 𝟙 X := by aesop_cat
+#align category_theory.split_mono CategoryTheory.SplitMono
+
+attribute [reassoc (attr := simp)] SplitMono.id
+
+/-- `IsSplitMono f` is the assertion that `f` admits a retraction -/
+class IsSplitMono {X Y : C} (f : X ⟶ Y) : Prop where
+  /-- There is a splitting -/ 
+  exists_splitMono : Nonempty (SplitMono f)
+#align category_theory.is_split_mono CategoryTheory.IsSplitMono
+
+/-- A constructor for `IsSplitMono f` taking a `SplitMono f` as an argument -/
+theorem IsSplitMono.mk' {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : IsSplitMono f :=
+  ⟨Nonempty.intro sm⟩
+#align category_theory.is_split_mono.mk' CategoryTheory.IsSplitMono.mk'
+
+/-- A split epimorphism is a morphism `f : X ⟶ Y` with a given section `section_ f : Y ⟶ X`
+such that `section_ f ≫ f = 𝟙 Y`.
+(Note that `section` is a reserved keyword, so we append an underscore.)
+
+Every split epimorphism is an epimorphism.
+-/
+/- Porting note: @[nolint has_nonempty_instance] -/
+/- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule -/
+@[aesop apply safe (rule_sets [CategoryTheory])]
+structure SplitEpi {X Y : C} (f : X ⟶ Y) where
+  /-- The map splitting `f` -/
+  section_ : Y ⟶ X
+  /--  `section_` composed with `f` is the identity -/
+  id : section_ ≫ f = 𝟙 Y := by aesop_cat
+#align category_theory.split_epi CategoryTheory.SplitEpi
+
+attribute [reassoc (attr := simp)] SplitEpi.id
+
+/-- `IsSplitEpi f` is the assertion that `f` admits a section -/
+class IsSplitEpi {X Y : C} (f : X ⟶ Y) : Prop where
+  /-- There is a splitting -/
+  exists_splitEpi : Nonempty (SplitEpi f)
+#align category_theory.is_split_epi CategoryTheory.IsSplitEpi
+
+/-- A constructor for `IsSplitEpi f` taking a `SplitEpi f` as an argument -/
+theorem IsSplitEpi.mk' {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : IsSplitEpi f :=
+  ⟨Nonempty.intro se⟩
+#align category_theory.is_split_epi.mk' CategoryTheory.IsSplitEpi.mk'
+
+/-- The chosen retraction of a split monomorphism. -/
+noncomputable def retraction {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Y ⟶ X :=
+  hf.exists_splitMono.some.retraction
+#align category_theory.retraction CategoryTheory.retraction
+
+@[reassoc (attr := simp)]
+theorem IsSplitMono.id {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : f ≫ retraction f = 𝟙 X :=
+  hf.exists_splitMono.some.id
+#align category_theory.is_split_mono.id CategoryTheory.IsSplitMono.id
+
+/-- The retraction of a split monomorphism has an obvious section. -/
+def SplitMono.splitEpi {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : SplitEpi sm.retraction 
+    where section_ := f
+#align category_theory.split_mono.split_epi CategoryTheory.SplitMono.splitEpi
+
+/-- The retraction of a split monomorphism is itself a split epimorphism. -/
+instance retraction_isSplitEpi {X Y : C} (f : X ⟶ Y) [IsSplitMono f] :
+    IsSplitEpi (retraction f) :=
+  IsSplitEpi.mk' (SplitMono.splitEpi _)
+#align category_theory.retraction_is_split_epi CategoryTheory.retraction_isSplitEpi
+
+/-- A split mono which is epi is an iso. -/
+theorem isIso_of_epi_of_isSplitMono {X Y : C} (f : X ⟶ Y) [IsSplitMono f] [Epi f] : IsIso f :=
+  ⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩
+#align category_theory.is_iso_of_epi_of_is_split_mono CategoryTheory.isIso_of_epi_of_isSplitMono
+
+/-- The chosen section of a split epimorphism.
+(Note that `section` is a reserved keyword, so we append an underscore.)
+-/
+noncomputable def section_ {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Y ⟶ X :=
+  hf.exists_splitEpi.some.section_
+#align category_theory.section_ CategoryTheory.section_
+
+@[reassoc (attr := simp)]
+theorem IsSplitEpi.id {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : section_ f ≫ f = 𝟙 Y :=
+  hf.exists_splitEpi.some.id
+#align category_theory.is_split_epi.id CategoryTheory.IsSplitEpi.id
+
+/-- The section of a split epimorphism has an obvious retraction. -/
+def SplitEpi.splitMono {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : SplitMono se.section_
+    where retraction := f
+#align category_theory.split_epi.split_mono CategoryTheory.SplitEpi.splitMono
+
+/-- The section of a split epimorphism is itself a split monomorphism. -/
+instance section_isSplitMono {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsSplitMono (section_ f) :=
+  IsSplitMono.mk' (SplitEpi.splitMono _)
+#align category_theory.section_is_split_mono CategoryTheory.section_isSplitMono
+
+/-- A split epi which is mono is an iso. -/
+theorem isIso_of_mono_of_isSplitEpi {X Y : C} (f : X ⟶ Y) [Mono f] [IsSplitEpi f] : IsIso f :=
+  ⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩
+#align category_theory.is_iso_of_mono_of_is_split_epi CategoryTheory.isIso_of_mono_of_isSplitEpi
+
+/-- Every iso is a split mono. -/
+instance (priority := 100) IsSplitMono.of_iso {X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitMono f :=
+  IsSplitMono.mk' { retraction := inv f }
+#align category_theory.is_split_mono.of_iso CategoryTheory.IsSplitMono.of_iso
+
+/-- Every iso is a split epi. -/
+instance (priority := 100) IsSplitEpi.of_iso {X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitEpi f :=
+  IsSplitEpi.mk' { section_ := inv f }
+#align category_theory.is_split_epi.of_iso CategoryTheory.IsSplitEpi.of_iso
+
+theorem SplitMono.mono {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : Mono f :=
+  { right_cancellation := fun g h w => by replace w := w =≫ sm.retraction; simpa using w }
+#align category_theory.split_mono.mono CategoryTheory.SplitMono.mono
+
+/-- Every split mono is a mono. -/
+instance (priority := 100) IsSplitMono.mono {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Mono f :=
+  hf.exists_splitMono.some.mono
+#align category_theory.is_split_mono.mono CategoryTheory.IsSplitMono.mono
+
+theorem SplitEpi.epi {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : Epi f :=
+  { left_cancellation := fun g h w => by replace w := se.section_ ≫= w; simpa using w }
+#align category_theory.split_epi.epi CategoryTheory.SplitEpi.epi
+
+/-- Every split epi is an epi. -/
+instance (priority := 100) IsSplitEpi.epi {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] : Epi f :=
+  hf.exists_splitEpi.some.epi
+#align category_theory.is_split_epi.epi CategoryTheory.IsSplitEpi.epi
+
+/-- Every split mono whose retraction is mono is an iso. -/
+theorem IsIso.of_mono_retraction' {X Y : C} {f : X ⟶ Y} (hf : SplitMono f) [Mono <| hf.retraction] :
+    IsIso f :=
+  ⟨⟨hf.retraction, ⟨by simp, (cancel_mono_id <| hf.retraction).mp (by simp)⟩⟩⟩
+#align category_theory.is_iso.of_mono_retraction' CategoryTheory.IsIso.of_mono_retraction'
+
+/-- Every split mono whose retraction is mono is an iso. -/
+theorem IsIso.of_mono_retraction {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f]
+    [hf' : Mono <| retraction f] : IsIso f :=
+  @IsIso.of_mono_retraction' _ _ _ _ _ hf.exists_splitMono.some hf'
+#align category_theory.is_iso.of_mono_retraction CategoryTheory.IsIso.of_mono_retraction
+
+/-- Every split epi whose section is epi is an iso. -/
+theorem IsIso.of_epi_section' {X Y : C} {f : X ⟶ Y} (hf : SplitEpi f) [Epi <| hf.section_] :
+    IsIso f :=
+  ⟨⟨hf.section_, ⟨(cancel_epi_id <| hf.section_).mp (by simp), by simp⟩⟩⟩
+#align category_theory.is_iso.of_epi_section' CategoryTheory.IsIso.of_epi_section'
+
+/-- Every split epi whose section is epi is an iso. -/
+theorem IsIso.of_epi_section {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] [hf' : Epi <| section_ f] :
+    IsIso f :=
+  @IsIso.of_epi_section' _ _ _ _ _ hf.exists_splitEpi.some hf'
+#align category_theory.is_iso.of_epi_section CategoryTheory.IsIso.of_epi_section
+
+-- FIXME this has unnecessarily become noncomputable!
+/-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
+noncomputable def Groupoid.ofTruncSplitMono
+    (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)) : Groupoid.{v₁} C := by
+  apply Groupoid.ofIsIso
+  intro X Y f
+  have ⟨a,_⟩:= Trunc.exists_rep <| all_split_mono f
+  have ⟨b,_⟩:= Trunc.exists_rep <| all_split_mono <| retraction f
+  apply IsIso.of_mono_retraction
+#align category_theory.groupoid.of_trunc_split_mono CategoryTheory.Groupoid.ofTruncSplitMono
+
+section
+
+variable (C)
+
+/-- A split mono category is a category in which every monomorphism is split. -/
+class SplitMonoCategory where
+  /-- All monos are split -/
+  isSplitMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], IsSplitMono f
+#align category_theory.split_mono_category CategoryTheory.SplitMonoCategory
+
+/-- A split epi category is a category in which every epimorphism is split. -/
+class SplitEpiCategory where
+  /-- All epis are split -/
+  isSplitEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], IsSplitEpi f
+#align category_theory.split_epi_category CategoryTheory.SplitEpiCategory
+
+end
+
+/-- In a category in which every monomorphism is split, every monomorphism splits. This is not an
+    instance because it would create an instance loop. -/
+theorem isSplitMono_of_mono [SplitMonoCategory C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f :=
+  SplitMonoCategory.isSplitMono_of_mono _
+#align category_theory.is_split_mono_of_mono CategoryTheory.isSplitMono_of_mono
+
+/-- In a category in which every epimorphism is split, every epimorphism splits. This is not an
+    instance because it would create an instance loop. -/
+theorem isSplitEpi_of_epi [SplitEpiCategory C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f :=
+  SplitEpiCategory.isSplitEpi_of_epi _
+#align category_theory.is_split_epi_of_epi CategoryTheory.isSplitEpi_of_epi
+
+section
+
+variable {D : Type u₂} [Category.{v₂} D]
+
+/-- Split monomorphisms are also absolute monomorphisms. -/
+@[simps]
+def SplitMono.map {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) (F : C ⥤ D) : SplitMono (F.map f)
+    where
+  retraction := F.map sm.retraction
+  id := by rw [← Functor.map_comp, SplitMono.id, Functor.map_id]
+#align category_theory.split_mono.map CategoryTheory.SplitMono.map
+
+/-- Split epimorphisms are also absolute epimorphisms. -/
+@[simps]
+def SplitEpi.map {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) (F : C ⥤ D) : SplitEpi (F.map f)
+    where
+  section_ := F.map se.section_
+  id := by rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]
+#align category_theory.split_epi.map CategoryTheory.SplitEpi.map
+
+instance {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] (F : C ⥤ D) : IsSplitMono (F.map f) :=
+  IsSplitMono.mk' (hf.exists_splitMono.some.map F)
+
+instance {X Y : C} (f : X ⟶ Y) [hf : IsSplitEpi f] (F : C ⥤ D) : IsSplitEpi (F.map f) :=
+  IsSplitEpi.mk' (hf.exists_splitEpi.some.map F)
+
+end
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Functor/Hom.lean b/Mathlib/CategoryTheory/Functor/Hom.lean
new file mode 100644
index 0000000000000..1db6fb49476f3
--- /dev/null
+++ b/Mathlib/CategoryTheory/Functor/Hom.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2018 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton, Scott Morrison
+
+! This file was ported from Lean 3 source module category_theory.functor.hom
+! leanprover-community/mathlib commit 369525b73f229ccd76a6ec0e0e0bf2be57599768
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Products.Basic
+import Mathlib.CategoryTheory.Types
+
+/-!
+The hom functor, sending `(X, Y)` to the type `X ⟶ Y`.
+-/
+
+
+universe v u
+
+open Opposite
+
+open CategoryTheory
+
+namespace CategoryTheory.Functor
+
+variable (C : Type u) [Category.{v} C]
+
+/-- `Functor.hom` is the hom-pairing, sending `(X, Y)` to `X ⟶ Y`, contravariant in `X` and
+covariant in `Y`. -/
+@[simps]
+def hom : Cᵒᵖ × C ⥤ Type v where
+  obj p := unop p.1 ⟶ p.2
+  map f h := f.1.unop ≫ h ≫ f.2
+  map_id := by aesop_cat 
+  map_comp := fun {X} {Y} {Z} f g => by funext b; simp
+#align category_theory.functor.hom CategoryTheory.Functor.hom
+
+end CategoryTheory.Functor
diff --git a/Mathlib/CategoryTheory/Groupoid.lean b/Mathlib/CategoryTheory/Groupoid.lean
new file mode 100644
index 0000000000000..8ebf75d278f76
--- /dev/null
+++ b/Mathlib/CategoryTheory/Groupoid.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2018 Reid Barton All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton, Scott Morrison, David Wärn
+
+! This file was ported from Lean 3 source module category_theory.groupoid
+! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.FullSubcategory
+import Mathlib.CategoryTheory.Products.Basic
+import Mathlib.CategoryTheory.Pi.Basic
+import Mathlib.CategoryTheory.Category.Basic
+import Mathlib.Combinatorics.Quiver.ConnectedComponent
+
+/-!
+# Groupoids
+
+We define `groupoid` as a typeclass extending `category`,
+asserting that all morphisms have inverses.
+
+The instance `IsIso.ofGroupoid (f : X ⟶ Y) : IsIso f` means that you can then write
+`inv f` to access the inverse of any morphism `f`.
+
+`Groupoid.isoEquivHom : (X ≅ Y) ≃ (X ⟶ Y)` provides the equivalence between
+isomorphisms and morphisms in a groupoid.
+
+We provide a (non-instance) constructor `Groupoid.ofIsIso` from an existing category
+with `IsIso f` for every `f`.
+
+## See also
+
+See also `CategoryTheory.Core` for the groupoid of isomorphisms in a category.
+-/
+
+
+namespace CategoryTheory
+
+universe v v₂ u u₂
+
+-- morphism levels before object levels. See note [CategoryTheory universes].
+/-- A `groupoid` is a category such that all morphisms are isomorphisms. -/
+class Groupoid (obj : Type u) extends Category.{v} obj : Type max u (v + 1) where
+  /-- The inverse morphism -/ 
+  inv : ∀ {X Y : obj}, (X ⟶ Y) → (Y ⟶ X)
+  /-- `inv f` composed `f` is the identity -/
+  inv_comp : ∀ {X Y : obj} (f : X ⟶ Y), comp (inv f) f = id Y := by aesop_cat
+  /-- `f` composed with `inv f` is the identity -/
+  comp_inv : ∀ {X Y : obj} (f : X ⟶ Y), comp f (inv f) = id X := by aesop_cat
+#align category_theory.groupoid CategoryTheory.Groupoid
+
+/-- A `LargeGroupoid` is a groupoid
+where the objects live in `Type (u+1)` while the morphisms live in `Type u`.
+-/
+abbrev LargeGroupoid (C : Type (u + 1)) : Type (u + 1) :=
+  Groupoid.{u} C
+#align category_theory.large_groupoid CategoryTheory.LargeGroupoid
+
+/-- A `SmallGroupoid` is a groupoid
+where the objects and morphisms live in the same universe.
+-/
+abbrev SmallGroupoid (C : Type u) : Type (u + 1) :=
+  Groupoid.{u} C
+#align category_theory.small_groupoid CategoryTheory.SmallGroupoid
+
+section
+
+variable {C : Type u} [Groupoid.{v} C] {X Y : C}
+
+-- see Note [lower instance priority]
+instance (priority := 100) IsIso.of_groupoid (f : X ⟶ Y) : IsIso f :=
+  ⟨⟨Groupoid.inv f, Groupoid.comp_inv f, Groupoid.inv_comp f⟩⟩
+#align category_theory.is_iso.of_groupoid CategoryTheory.IsIso.of_groupoid
+
+@[simp]
+theorem Groupoid.inv_eq_inv (f : X ⟶ Y) : Groupoid.inv f = CategoryTheory.inv f :=
+  IsIso.eq_inv_of_hom_inv_id <| Groupoid.comp_inv f
+#align category_theory.groupoid.inv_eq_inv CategoryTheory.Groupoid.inv_eq_inv
+
+/-- `groupoid.inv` is involutive. -/
+@[simps]
+def Groupoid.invEquiv : (X ⟶ Y) ≃ (Y ⟶ X) :=
+  ⟨Groupoid.inv, Groupoid.inv, fun f => by simp, fun f => by simp⟩
+#align category_theory.groupoid.inv_equiv CategoryTheory.Groupoid.invEquiv
+
+instance (priority := 100) groupoidHasInvolutiveReverse : Quiver.HasInvolutiveReverse C
+    where
+  reverse' f := Groupoid.inv f
+  inv' f := by
+    dsimp [Quiver.reverse]
+    simp
+#align category_theory.groupoid_has_involutive_reverse CategoryTheory.groupoidHasInvolutiveReverse
+
+@[simp]
+theorem Groupoid.reverse_eq_inv (f : X ⟶ Y) : Quiver.reverse f = Groupoid.inv f :=
+  rfl
+#align category_theory.groupoid.reverse_eq_inv CategoryTheory.Groupoid.reverse_eq_inv
+
+instance functorMapReverse {D : Type _} [Groupoid D] (F : C ⥤ D) : F.toPrefunctor.MapReverse
+    where 
+      map_reverse' f := by
+        simp only [Quiver.reverse, Quiver.HasReverse.reverse', Groupoid.inv_eq_inv,
+          Functor.map_inv]
+#align category_theory.functor_map_reverse CategoryTheory.functorMapReverse
+
+variable (X Y)
+
+/-- In a groupoid, isomorphisms are equivalent to morphisms. -/
+def Groupoid.isoEquivHom : (X ≅ Y) ≃ (X ⟶ Y)
+    where
+  toFun := Iso.hom
+  invFun f := ⟨f, Groupoid.inv f, (by aesop_cat), (by aesop_cat)⟩
+  left_inv i := Iso.ext rfl
+  right_inv f := rfl
+#align category_theory.groupoid.iso_equiv_hom CategoryTheory.Groupoid.isoEquivHom
+
+variable (C)
+
+/-- The functor from a groupoid `C` to its opposite sending every morphism to its inverse. -/
+@[simps]
+noncomputable def Groupoid.invFunctor : C ⥤ Cᵒᵖ
+    where
+  obj := Opposite.op
+  map {X Y} f := (inv f).op
+#align category_theory.groupoid.inv_functor CategoryTheory.Groupoid.invFunctor
+
+end
+
+section
+
+variable {C : Type u} [Category.{v} C]
+
+/-- A category where every morphism `IsIso` is a groupoid. -/
+noncomputable def Groupoid.ofIsIso (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), IsIso f) : Groupoid.{v} C
+    where 
+      inv := fun f => CategoryTheory.inv f
+      comp_inv := by aesop_cat 
+      inv_comp := fun f => Classical.choose_spec (all_is_iso f).out|>.right  
+#align category_theory.groupoid.of_is_iso CategoryTheory.Groupoid.ofIsIso
+
+/-- A category with a unique morphism between any two objects is a groupoid -/
+def Groupoid.ofHomUnique (all_unique : ∀ {X Y : C}, Unique (X ⟶ Y)) : Groupoid.{v} C
+    where inv _ := all_unique.default
+#align category_theory.groupoid.of_hom_unique CategoryTheory.Groupoid.ofHomUnique
+
+end
+
+instance InducedCategory.groupoid {C : Type u} (D : Type u₂) [Groupoid.{v} D] (F : C → D) :
+    Groupoid.{v} (InducedCategory D F) :=
+  { InducedCategory.category F with
+    inv := fun f => Groupoid.inv f
+    inv_comp := fun f => Groupoid.inv_comp f
+    comp_inv := fun f => Groupoid.comp_inv f }
+#align category_theory.induced_category.groupoid CategoryTheory.InducedCategory.groupoid
+
+section
+
+instance groupoidPi {I : Type u} {J : I → Type u₂} [∀ i, Groupoid.{v} (J i)] :
+    Groupoid.{max u v} (∀ i : I, J i)
+    where 
+      inv f := fun i : I => Groupoid.inv (f i)
+      comp_inv := fun f => by funext i; apply Groupoid.comp_inv  
+      inv_comp := fun f => by funext i; apply Groupoid.inv_comp  
+#align category_theory.groupoid_pi CategoryTheory.groupoidPi
+
+instance groupoidProd {α : Type u} {β : Type v} [Groupoid.{u₂} α] [Groupoid.{v₂} β] :
+    Groupoid.{max u₂ v₂} (α × β)
+    where inv f := (Groupoid.inv f.1, Groupoid.inv f.2)
+#align category_theory.groupoid_prod CategoryTheory.groupoidProd
+
+end
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean
new file mode 100644
index 0000000000000..63f7c04605930
--- /dev/null
+++ b/Mathlib/CategoryTheory/Types.lean
@@ -0,0 +1,405 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl
+
+! This file was ported from Lean 3 source module category_theory.types
+! leanprover-community/mathlib commit 48085f140e684306f9e7da907cd5932056d1aded
+! 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.Functor.FullyFaithful
+import Mathlib.Logic.Equiv.Basic
+
+/-!
+# The category `Type`.
+
+In this section we set up the theory so that Lean's types and functions between them
+can be viewed as a `LargeCategory` in our framework.
+
+Lean can not transparently view a function as a morphism in this category, and needs a hint in
+order to be able to type check. We provide the abbreviation `asHom f` to guide type checking,
+as well as a corresponding notation `↾ f`. (Entered as `\upr `.) 
+
+We provide various simplification lemmas for functors and natural transformations valued in `Type`.
+
+We define `uliftFunctor`, from `Type u` to `Type (max u v)`, and show that it is fully faithful
+(but not, of course, essentially surjective).
+
+We prove some basic facts about the category `Type`:
+*  epimorphisms are surjections and monomorphisms are injections,
+* `Iso` is both `Iso` and `Equiv` to `Equiv` (at least within a fixed universe),
+* every type level `IsLawfulFunctor` gives a categorical functor `Type ⥤ Type`
+  (the corresponding fact about monads is in `Mathlib/CategoryTheory/Monad/Types.lean`).
+-/
+
+
+namespace CategoryTheory
+
+-- morphism levels before object levels. See note [category_theory universes].
+universe v v' w u u'
+
+/- The `@[to_additive]` attribute is just a hint that expressions involving this instance can
+  still be additivized. -/
+@[to_additive CategoryTheory.types]
+instance types : LargeCategory (Type u)
+    where
+  Hom a b := a → b
+  id a := id
+  comp f g := g ∘ f
+#align category_theory.types CategoryTheory.types
+
+theorem types_hom {α β : Type u} : (α ⟶ β) = (α → β) :=
+  rfl
+#align category_theory.types_hom CategoryTheory.types_hom
+
+theorem types_id (X : Type u) : 𝟙 X = id :=
+  rfl
+#align category_theory.types_id CategoryTheory.types_id
+
+theorem types_comp {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) : f ≫ g = g ∘ f :=
+  rfl
+#align category_theory.types_comp CategoryTheory.types_comp
+
+@[simp]
+theorem types_id_apply (X : Type u) (x : X) : (𝟙 X : X → X) x = x :=
+  rfl
+#align category_theory.types_id_apply CategoryTheory.types_id_apply
+
+@[simp]
+theorem types_comp_apply {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) :=
+  rfl
+#align category_theory.types_comp_apply CategoryTheory.types_comp_apply
+
+@[simp]
+theorem hom_inv_id_apply {X Y : Type u} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x :=
+  congr_fun f.hom_inv_id x
+#align category_theory.hom_inv_id_apply CategoryTheory.hom_inv_id_apply
+
+@[simp]
+theorem inv_hom_id_apply {X Y : Type u} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y :=
+  congr_fun f.inv_hom_id y
+#align category_theory.inv_hom_id_apply CategoryTheory.inv_hom_id_apply
+
+-- Unfortunately without this wrapper we can't use `CategoryTheory` idioms, such as `IsIso f`.
+/-- `asHom f` helps Lean type check a function as a morphism in the category `Type`. -/
+abbrev asHom {α β : Type u} (f : α → β) : α ⟶ β :=
+  f
+#align category_theory.as_hom CategoryTheory.asHom
+
+-- If you don't mind some notation you can use fewer keystrokes:
+/-- Type as \upr in VScode -/
+scoped notation "↾" f:200 => CategoryTheory.asHom f
+
+section
+
+-- We verify the expected type checking behaviour of `asHom`
+variable (α β γ : Type u) (f : α → β) (g : β → γ)
+
+example : α → γ :=
+  ↾f ≫ ↾g
+
+example [IsIso (↾f)] : Mono (↾f) := by infer_instance
+
+example [IsIso (↾f)] : ↾f ≫ inv (↾f) = 𝟙 α := by simp
+
+end
+
+namespace Functor
+
+variable {J : Type u} [Category.{v} J]
+
+/-- The sections of a functor `J ⥤ Type` are
+the choices of a point `u j : F.obj j` for each `j`,
+such that `F.map f (u j) = u j` for every morphism `f : j ⟶ j'`.
+
+We later use these to define limits in `Type` and in many concrete categories.
+-/
+def sections (F : J ⥤ Type w) : Set (∀ j, F.obj j) :=
+  { u | ∀ {j j'} (f : j ⟶ j'), F.map f (u j) = u j' }
+#align category_theory.functor.sections CategoryTheory.Functor.sections
+
+end Functor
+
+namespace FunctorToTypes
+
+variable {C : Type u} [Category.{v} C] (F G H : C ⥤ Type w) {X Y Z : C}
+
+variable (σ : F ⟶ G) (τ : G ⟶ H)
+
+@[simp]
+theorem map_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) :
+    (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) := by simp [types_comp]
+#align category_theory.functor_to_types.map_comp_apply CategoryTheory.FunctorToTypes.map_comp_apply
+
+@[simp]
+theorem map_id_apply (a : F.obj X) : (F.map (𝟙 X)) a = a := by simp [types_id]
+#align category_theory.functor_to_types.map_id_apply CategoryTheory.FunctorToTypes.map_id_apply
+
+theorem naturality (f : X ⟶ Y) (x : F.obj X) : σ.app Y ((F.map f) x) = (G.map f) (σ.app X x) :=
+  congr_fun (σ.naturality f) x
+#align category_theory.functor_to_types.naturality CategoryTheory.FunctorToTypes.naturality
+
+@[simp]
+theorem comp (x : F.obj X) : (σ ≫ τ).app X x = τ.app X (σ.app X x) :=
+  rfl
+#align category_theory.functor_to_types.comp CategoryTheory.FunctorToTypes.comp
+
+variable {D : Type u'} [𝒟 : Category.{u'} D] (I J : D ⥤ C) (ρ : I ⟶ J) {W : D}
+
+@[simp]
+theorem hcomp (x : (I ⋙ F).obj W) : (ρ ◫ σ).app W x = (G.map (ρ.app W)) (σ.app (I.obj W) x) :=
+  rfl
+#align category_theory.functor_to_types.hcomp CategoryTheory.FunctorToTypes.hcomp
+
+@[simp]
+theorem map_inv_map_hom_apply (f : X ≅ Y) (x : F.obj X) : F.map f.inv (F.map f.hom x) = x :=
+  congr_fun (F.mapIso f).hom_inv_id x
+#align category_theory.functor_to_types.map_inv_map_hom_apply CategoryTheory.FunctorToTypes.map_inv_map_hom_apply
+
+@[simp]
+theorem map_hom_map_inv_apply (f : X ≅ Y) (y : F.obj Y) : F.map f.hom (F.map f.inv y) = y :=
+  congr_fun (F.mapIso f).inv_hom_id y
+#align category_theory.functor_to_types.map_hom_map_inv_apply CategoryTheory.FunctorToTypes.map_hom_map_inv_apply
+
+@[simp]
+theorem hom_inv_id_app_apply (α : F ≅ G) (X) (x) : α.inv.app X (α.hom.app X x) = x :=
+  congr_fun (α.hom_inv_id_app X) x
+#align category_theory.functor_to_types.hom_inv_id_app_apply CategoryTheory.FunctorToTypes.hom_inv_id_app_apply
+
+@[simp]
+theorem inv_hom_id_app_apply (α : F ≅ G) (X) (x) : α.hom.app X (α.inv.app X x) = x :=
+  congr_fun (α.inv_hom_id_app X) x
+#align category_theory.functor_to_types.inv_hom_id_app_apply CategoryTheory.FunctorToTypes.inv_hom_id_app_apply
+
+end FunctorToTypes
+
+/-- The isomorphism between a `Type` which has been `ulift`ed to the same universe,
+and the original type.
+-/
+def uliftTrivial (V : Type u) : ULift.{u} V ≅ V where 
+  hom a := a.1
+  inv a := .up a  
+  hom_inv_id := by aesop_cat 
+  inv_hom_id := by aesop_cat 
+#align category_theory.ulift_trivial CategoryTheory.uliftTrivial
+
+/-- The functor embedding `Type u` into `Type (max u v)`.
+Write this as `uliftFunctor.{5 2}` to get `Type 2 ⥤ Type 5`.
+-/
+def uliftFunctor : Type u ⥤ Type max u v
+    where
+  obj X := ULift.{v} X
+  map {X} {Y} f := fun x : ULift.{v} X => ULift.up (f x.down)
+#align category_theory.ulift_functor CategoryTheory.uliftFunctor
+
+@[simp]
+theorem uliftFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : ULift.{v} X) :
+    uliftFunctor.map f x = ULift.up (f x.down) :=
+  rfl
+#align category_theory.ulift_functor_map CategoryTheory.uliftFunctor_map
+
+instance uliftFunctorFull : Full.{u} uliftFunctor where preimage f x := (f (ULift.up x)).down
+#align category_theory.ulift_functor_full CategoryTheory.uliftFunctorFull
+
+instance uliftFunctor_faithful : Faithful uliftFunctor
+    where map_injective {_X} {_Y} f g p :=
+    funext fun x =>
+      congr_arg ULift.down (congr_fun p (ULift.up x) : ULift.up (f x) = ULift.up (g x))
+#align category_theory.ulift_functor_faithful CategoryTheory.uliftFunctor_faithful
+
+/-- The functor embedding `Type u` into `Type u` via `ulift` is isomorphic to the identity functor.
+ -/
+def uliftFunctorTrivial : uliftFunctor.{u, u} ≅ 𝟭 _ :=
+  NatIso.ofComponents uliftTrivial (by aesop_cat)
+#align category_theory.ulift_functor_trivial CategoryTheory.uliftFunctorTrivial
+
+-- TODO We should connect this to a general story about concrete categories
+-- whose forgetful functor is representable.
+/-- Any term `x` of a type `X` corresponds to a morphism `punit ⟶ X`. -/
+def homOfElement {X : Type u} (x : X) : PUnit ⟶ X := fun _ => x
+#align category_theory.hom_of_element CategoryTheory.homOfElement
+
+theorem homOfElement_eq_iff {X : Type u} (x y : X) : homOfElement x = homOfElement y ↔ x = y :=
+  ⟨fun H => congr_fun H PUnit.unit, by aesop⟩  
+#align category_theory.hom_of_element_eq_iff CategoryTheory.homOfElement_eq_iff
+
+/-- A morphism in `Type` is a monomorphism if and only if it is injective.
+
+See <https://stacks.math.columbia.edu/tag/003C>.
+-/
+theorem mono_iff_injective {X Y : Type u} (f : X ⟶ Y) : Mono f ↔ Function.Injective f := by
+  constructor
+  · intro H x x' h
+    skip
+    rw [← homOfElement_eq_iff] at h⊢
+    exact (cancel_mono f).mp h
+  · exact fun H => ⟨fun g g' h => H.comp_left h⟩
+#align category_theory.mono_iff_injective CategoryTheory.mono_iff_injective
+
+theorem injective_of_mono {X Y : Type u} (f : X ⟶ Y) [hf : Mono f] : Function.Injective f :=
+  (mono_iff_injective f).1 hf
+#align category_theory.injective_of_mono CategoryTheory.injective_of_mono
+
+/-- A morphism in `Type` is an epimorphism if and only if it is surjective.
+
+See <https://stacks.math.columbia.edu/tag/003C>.
+-/
+theorem epi_iff_surjective {X Y : Type u} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f := by
+  constructor
+  · rintro ⟨H⟩
+    refine' Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => _
+    rw [← Equiv.ulift.symm.injective.comp_left.eq_iff]
+    apply H
+    change ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f
+    rw [hg]
+  · exact fun H => ⟨fun g g' h => H.injective_comp_right h⟩
+#align category_theory.epi_iff_surjective CategoryTheory.epi_iff_surjective
+
+theorem surjective_of_epi {X Y : Type u} (f : X ⟶ Y) [hf : Epi f] : Function.Surjective f :=
+  (epi_iff_surjective f).1 hf
+#align category_theory.surjective_of_epi CategoryTheory.surjective_of_epi
+
+section
+
+/-- `ofTypeFunctor m` converts from Lean's `Type`-based `Category` to `CategoryTheory`. This
+allows us to use these functors in category theory. -/
+def ofTypeFunctor (m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m] : Type u ⥤ Type v
+    where
+  obj := m
+  map f := Functor.map f  
+  map_id := fun α => by funext X; apply id_map  /- Porting note: original proof is via 
+  `fun α => _root_.Functor.map_id` but I cannot get Lean to find this. Reproduced its 
+  original proof -/
+  map_comp f g := funext fun a => LawfulFunctor.comp_map f g _
+#align category_theory.of_type_functor CategoryTheory.ofTypeFunctor
+
+variable (m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m]
+
+@[simp]
+theorem ofTypeFunctor_obj : (ofTypeFunctor m).obj = m :=
+  rfl
+#align category_theory.of_type_functor_obj CategoryTheory.ofTypeFunctor_obj
+
+@[simp]
+theorem ofTypeFunctor_map {α β} (f : α → β) :
+    (ofTypeFunctor m).map f = (Functor.map f : m α → m β) :=
+  rfl
+#align category_theory.of_type_functor_map CategoryTheory.ofTypeFunctor_map
+
+end
+
+end CategoryTheory
+
+-- Isomorphisms in Type and equivalences.
+namespace Equiv
+
+universe u
+
+variable {X Y : Type u}
+
+/-- Any equivalence between types in the same universe gives
+a categorical isomorphism between those types.
+-/
+def toIso (e : X ≃ Y) : X ≅ Y where
+  hom := e.toFun
+  inv := e.invFun
+  hom_inv_id := funext e.left_inv
+  inv_hom_id := funext e.right_inv
+#align equiv.to_iso Equiv.toIso
+
+@[simp]
+theorem toIso_hom {e : X ≃ Y} : e.toIso.hom = e :=
+  rfl
+#align equiv.to_iso_hom Equiv.toIso_hom
+
+@[simp]
+theorem toIso_inv {e : X ≃ Y} : e.toIso.inv = e.symm :=
+  rfl
+#align equiv.to_iso_inv Equiv.toIso_inv
+
+end Equiv
+
+universe u
+
+namespace CategoryTheory.Iso
+
+open CategoryTheory
+
+variable {X Y : Type u}
+
+/-- Any isomorphism between types gives an equivalence.
+-/
+def toEquiv (i : X ≅ Y) : X ≃ Y where
+  toFun := i.hom
+  invFun := i.inv
+  left_inv x := congr_fun i.hom_inv_id x
+  right_inv y := congr_fun i.inv_hom_id y
+#align category_theory.iso.to_equiv CategoryTheory.Iso.toEquiv
+
+@[simp]
+theorem toEquiv_fun (i : X ≅ Y) : (i.toEquiv : X → Y) = i.hom :=
+  rfl
+#align category_theory.iso.to_equiv_fun CategoryTheory.Iso.toEquiv_fun
+
+@[simp]
+theorem toEquiv_symm_fun (i : X ≅ Y) : (i.toEquiv.symm : Y → X) = i.inv :=
+  rfl
+#align category_theory.iso.to_equiv_symm_fun CategoryTheory.Iso.toEquiv_symm_fun
+
+@[simp]
+theorem toEquiv_id (X : Type u) : (Iso.refl X).toEquiv = Equiv.refl X :=
+  rfl
+#align category_theory.iso.to_equiv_id CategoryTheory.Iso.toEquiv_id
+
+@[simp]
+theorem toEquiv_comp {X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z) :
+    (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv :=
+  rfl
+#align category_theory.iso.to_equiv_comp CategoryTheory.Iso.toEquiv_comp
+
+end CategoryTheory.Iso
+
+namespace CategoryTheory
+
+/-- A morphism in `Type u` is an isomorphism if and only if it is bijective. -/
+theorem isIso_iff_bijective {X Y : Type u} (f : X ⟶ Y) : IsIso f ↔ Function.Bijective f :=
+  Iff.intro (fun _ => (asIso f : X ≅ Y).toEquiv.bijective) fun b =>
+    IsIso.of_iso (Equiv.ofBijective f b).toIso
+#align category_theory.is_iso_iff_bijective CategoryTheory.isIso_iff_bijective
+
+instance : SplitEpiCategory (Type u)
+    where isSplitEpi_of_epi f hf :=
+    IsSplitEpi.mk' <|
+      { section_ := Function.surjInv <| (epi_iff_surjective f).1 hf
+        id := funext <| Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf }
+
+end CategoryTheory
+
+-- We prove `equivIsoIso` and then use that to sneakily construct `equivEquivIso`.
+-- (In this order the proofs are handled by `obviously`.)
+/-- Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms
+of types. -/
+@[simps]
+def equivIsoIso {X Y : Type u} : X ≃ Y ≅ X ≅ Y
+    where
+  hom e := e.toIso
+  inv i := i.toEquiv
+#align equiv_iso_iso equivIsoIso
+
+/-- Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms
+of types. -/
+def equivEquivIso {X Y : Type u} : X ≃ Y ≃ (X ≅ Y) :=
+  equivIsoIso.toEquiv
+#align equiv_equiv_iso equivEquivIso
+
+@[simp]
+theorem equivEquivIso_hom {X Y : Type u} (e : X ≃ Y) : equivEquivIso e = e.toIso :=
+  rfl
+#align equiv_equiv_iso_hom equivEquivIso_hom
+
+@[simp]
+theorem equivEquivIso_inv {X Y : Type u} (e : X ≅ Y) : equivEquivIso.symm e = e.toEquiv :=
+  rfl
+#align equiv_equiv_iso_inv equivEquivIso_inv
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"