From c61c5af95ca05a2b8848d71809923cb458d8e2b4 Mon Sep 17 00:00:00 2001
From: prakol16 <praneeth.kolichala@gmail.com>
Date: Thu, 17 Mar 2022 01:38:15 +0000
Subject: [PATCH] feat(category_theory/punit): A groupoid is equivalent to
 punit iff it has a unique arrow between any two objects (#12726)

In terms of topology, when this is used with the fundamental groupoid, it means that a space is simply connected (we still need to define this) if and only if any two paths between the same points are homotopic, and contractible spaces are simply connected.
---
 src/category_theory/groupoid.lean |  4 ++++
 src/category_theory/punit.lean    | 27 ++++++++++++++++++++++++++-
 2 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/category_theory/groupoid.lean b/src/category_theory/groupoid.lean
index d94cabd6b9938..73b3692f5381b 100644
--- a/src/category_theory/groupoid.lean
+++ b/src/category_theory/groupoid.lean
@@ -81,6 +81,10 @@ noncomputable
 def groupoid.of_is_iso (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), is_iso f) : groupoid.{v} C :=
 { inv := λ X Y f, inv f }
 
+/-- A category with a unique morphism between any two objects is a groupoid -/
+def groupoid.of_hom_unique (all_unique : ∀ {X Y : C}, unique (X ⟶ Y)) : groupoid.{v} C :=
+{ inv := λ X Y f, all_unique.default }
+
 end
 
 instance induced_category.groupoid {C : Type u} (D : Type u₂) [groupoid.{v} D] (F : C → D) :
diff --git a/src/category_theory/punit.lean b/src/category_theory/punit.lean
index ba2f6f9af8efd..834a3f78b5fd4 100644
--- a/src/category_theory/punit.lean
+++ b/src/category_theory/punit.lean
@@ -17,9 +17,9 @@ and construct the equivalence `(discrete punit ⥤ C) ≌ C`.
 universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
+variables (C : Type u) [category.{v} C]
 
 namespace functor
-variables (C : Type u) [category.{v} C]
 
 /-- The constant functor sending everything to `punit.star`. -/
 @[simps]
@@ -70,4 +70,29 @@ def equiv : (discrete punit ⥤ C) ≌ C :=
 
 end functor
 
+/-- A category being equivalent to `punit` is equivalent to it having a unique morphism between
+  any two objects. (In fact, such a category is also a groupoid; see `groupoid.of_hom_unique`) -/
+theorem equiv_punit_iff_unique :
+  nonempty (C ≌ discrete punit) ↔ (nonempty C) ∧ (∀ x y : C, nonempty $ unique (x ⟶ y)) :=
+begin
+  split,
+  { rintro ⟨h⟩,
+    refine ⟨⟨h.inverse.obj punit.star⟩, λ x y, nonempty.intro _⟩,
+    apply (unique_of_subsingleton _), swap,
+    { have hx : x ⟶ h.inverse.obj punit.star := by convert h.unit.app x,
+      have hy : h.inverse.obj punit.star ⟶ y := by convert h.unit_inv.app y,
+      exact hx ≫ hy, },
+    have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unit_inv.app y,
+    { intro z, simpa using congr_arg (≫ (h.unit_inv.app y)) (h.unit.naturality z), },
+    apply subsingleton.intro,
+    intros a b,
+    rw [this a, this b],
+    simp only [functor.comp_map], congr, },
+  { rintro ⟨⟨p⟩, h⟩,
+    haveI := λ x y, (h x y).some,
+    refine nonempty.intro (category_theory.equivalence.mk
+      ((functor.const _).obj punit.star) ((functor.const _).obj p) _ (by apply functor.punit_ext)),
+    exact nat_iso.of_components (λ _, { hom := default, inv := default }) (λ _ _ _, by tidy), },
+end
+
 end category_theory