feat(algebraic_topology/fundamental_groupoid): Fundamental groupoid o…

…f punit (#12757)

Proves the equivalence of the fundamental groupoid of punit and punit

src/algebraic_topology/fundamental_groupoid/punit.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Praneeth Kolichala
+-/
+import algebraic_topology.fundamental_groupoid.induced_maps
+import category_theory.punit
+
+/-!
+# Fundamental groupoid of punit
+
+The fundamental groupoid of punit is naturally isomorphic to `category_theory.discrete punit`
+-/
+
+noncomputable theory
+
+open category_theory
+universes u v
+
+namespace path
+
+instance : subsingleton (path punit.star punit.star) := ⟨λ x y, by ext⟩
+
+end path
+
+namespace fundamental_groupoid
+
+instance {x y : fundamental_groupoid punit} : subsingleton (x ⟶ y) :=
+begin
+  convert_to subsingleton (path.homotopic.quotient punit.star punit.star),
+  { congr; apply punit_eq_star, },
+  apply quotient.subsingleton,
+end
+
+/-- Equivalence of groupoids between fundamental groupoid of punit and punit -/
+def punit_equiv_discrete_punit : fundamental_groupoid punit.{u+1} ≌ discrete punit.{v+1} :=
+equivalence.mk (functor.star _) ((category_theory.functor.const _).obj punit.star)
+  (nat_iso.of_components (λ _, eq_to_iso dec_trivial) (λ _ _ _, dec_trivial))
+  (functor.punit_ext _ _)
+
+end fundamental_groupoid