[Merged by Bors] - fix: Fix FundamentalGroupoid being reducible.

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -266,35 +266,77 @@ end Homotopy
 
 end Path
 
-/-- The fundamental groupoid of a space `X` is defined to be a type synonym for `X`, and we
+/-- The fundamental groupoid of a space `X` is defined to be a wrapper around `X`, and we
 subsequently put a `CategoryTheory.Groupoid` structure on it. -/
-def FundamentalGroupoid (X : Type u) := X
+@[ext]
+structure FundamentalGroupoid (X : Type u) where
+  /-- View a term of `FundamentalGroupoid X` as a term of `X`.-/
+  as : X
 #align fundamental_groupoid FundamentalGroupoid
 
 namespace FundamentalGroupoid
 
-instance {X : Type u} [h : Inhabited X] : Inhabited (FundamentalGroupoid X) := h
-
-attribute [reducible] FundamentalGroupoid
+/-- The equivalence between `X` and the underlying type of its fundamental groupoid.
+  This is useful for transferring constructions (instances, etc.)
+  from `X` to `πₓ X`. -/
+@[simps]
+def equiv (X : Type*) : FundamentalGroupoid X ≃ X where
+  toFun x := x.as
+  invFun x := .mk x
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp]
+lemma isEmpty_iff (X : Type*) :
+    IsEmpty (FundamentalGroupoid X) ↔ IsEmpty X :=
+  equiv _ |>.isEmpty_congr
+
+instance (X : Type*) [IsEmpty X] :
+    IsEmpty (FundamentalGroupoid X) :=
+  equiv _ |>.isEmpty
+
+@[simp]
+lemma nonempty_iff (X : Type*) :
+    Nonempty (FundamentalGroupoid X) ↔ Nonempty X :=
+  equiv _ |>.nonempty_congr
+
+instance (X : Type*) [Nonempty X] :
+    Nonempty (FundamentalGroupoid X) :=
+  equiv _ |>.nonempty
+
+@[simp]
+lemma subsingleton_iff (X : Type*) :
+    Subsingleton (FundamentalGroupoid X) ↔ Subsingleton X :=
+  equiv _ |>.subsingleton_congr
+
+instance (X : Type*) [Subsingleton X] :
+    Subsingleton (FundamentalGroupoid X) :=
+  equiv _ |>.subsingleton
+
+-- TODO: It seems that `Equiv.nontrivial_congr` doesn't exist.
+-- Once it is added, please add the corresponding lemma and instance.
+
+instance {X : Type u} [Inhabited X] : Inhabited (FundamentalGroupoid X) :=
+  ⟨⟨default⟩⟩
 
 attribute [local instance] Path.Homotopic.setoid
 
 instance : CategoryTheory.Groupoid (FundamentalGroupoid X) where
-  Hom x y := Path.Homotopic.Quotient x y
-  id x := ⟦Path.refl x⟧
+  Hom x y := Path.Homotopic.Quotient x.as y.as
+  id x := ⟦Path.refl x.as⟧
   comp {x y z} := Path.Homotopic.Quotient.comp
   id_comp {x y} f :=
     Quotient.inductionOn f fun a =>
-      show ⟦(Path.refl x).trans a⟧ = ⟦a⟧ from Quotient.sound ⟨Path.Homotopy.reflTrans a⟩
+      show ⟦(Path.refl x.as).trans a⟧ = ⟦a⟧ from Quotient.sound ⟨Path.Homotopy.reflTrans a⟩
   comp_id {x y} f :=
     Quotient.inductionOn f fun a =>
-      show ⟦a.trans (Path.refl y)⟧ = ⟦a⟧ from Quotient.sound ⟨Path.Homotopy.transRefl a⟩
+      show ⟦a.trans (Path.refl y.as)⟧ = ⟦a⟧ from Quotient.sound ⟨Path.Homotopy.transRefl a⟩
   assoc {w x y z} f g h :=
     Quotient.inductionOn₃ f g h fun p q r =>
       show ⟦(p.trans q).trans r⟧ = ⟦p.trans (q.trans r)⟧ from
         Quotient.sound ⟨Path.Homotopy.transAssoc p q r⟩
   inv {x y} p :=
-    Quotient.lift (fun l : Path x y => ⟦l.symm⟧)
+    Quotient.lift (fun l : Path x.as y.as => ⟦l.symm⟧)
       (by
         rintro a b ⟨h⟩
         simp only
@@ -303,24 +345,24 @@ instance : CategoryTheory.Groupoid (FundamentalGroupoid X) where
       p
   inv_comp {x y} f :=
     Quotient.inductionOn f fun a =>
-      show ⟦a.symm.trans a⟧ = ⟦Path.refl y⟧ from
+      show ⟦a.symm.trans a⟧ = ⟦Path.refl y.as⟧ from
         Quotient.sound ⟨(Path.Homotopy.reflSymmTrans a).symm⟩
   comp_inv {x y} f :=
     Quotient.inductionOn f fun a =>
-      show ⟦a.trans a.symm⟧ = ⟦Path.refl x⟧ from
+      show ⟦a.trans a.symm⟧ = ⟦Path.refl x.as⟧ from
         Quotient.sound ⟨(Path.Homotopy.reflTransSymm a).symm⟩
 
 theorem comp_eq (x y z : FundamentalGroupoid X) (p : x ⟶ y) (q : y ⟶ z) : p ≫ q = p.comp q := rfl
 #align fundamental_groupoid.comp_eq FundamentalGroupoid.comp_eq
 
-theorem id_eq_path_refl (x : FundamentalGroupoid X) : 𝟙 x = ⟦Path.refl x⟧ := rfl
+theorem id_eq_path_refl (x : FundamentalGroupoid X) : 𝟙 x = ⟦Path.refl x.as⟧ := rfl
 #align fundamental_groupoid.id_eq_path_refl FundamentalGroupoid.id_eq_path_refl
 
 /-- The functor sending a topological space `X` to its fundamental groupoid. -/
 def fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd where
   obj X := { α := FundamentalGroupoid X }
   map f :=
-    { obj := f
+    { obj := fun x => ⟨f x.as⟩
       map := fun {X Y} p => by exact Path.Homotopic.Quotient.mapFn p f
       map_id := fun X => rfl
       map_comp := fun {x y z} p q => by
@@ -356,26 +398,29 @@ theorem map_eq {X Y : TopCat} {x₀ x₁ : X} (f : C(X, Y)) (p : Path.Homotopic.
 /-- Help the typechecker by converting a point in a groupoid back to a point in
 the underlying topological space. -/
 @[reducible]
-def toTop {X : TopCat} (x : πₓ X) : X := x
+def toTop {X : TopCat} (x : πₓ X) : X := x.as
 #align fundamental_groupoid.to_top FundamentalGroupoid.toTop
 
 /-- Help the typechecker by converting a point in a topological space to a
 point in the fundamental groupoid of that space. -/
 @[reducible]
-def fromTop {X : TopCat} (x : X) : πₓ X := x
+def fromTop {X : TopCat} (x : X) : πₓ X := ⟨x⟩
 #align fundamental_groupoid.from_top FundamentalGroupoid.fromTop
 
 /-- Help the typechecker by converting an arrow in the fundamental groupoid of
 a topological space back to a path in that space (i.e., `Path.Homotopic.Quotient`). -/
 -- Porting note: Added `(X := X)` to the type.
 @[reducible]
-def toPath {X : TopCat} {x₀ x₁ : πₓ X} (p : x₀ ⟶ x₁) : Path.Homotopic.Quotient (X := X) x₀ x₁ := p
+def toPath {X : TopCat} {x₀ x₁ : πₓ X} (p : x₀ ⟶ x₁) :
+    Path.Homotopic.Quotient (X := X) x₀.as x₁.as :=
+  p
 #align fundamental_groupoid.to_path FundamentalGroupoid.toPath
 
 /-- Help the typechecker by converting a path in a topological space to an arrow in the
 fundamental groupoid of that space. -/
 @[reducible]
-def fromPath {X : TopCat} {x₀ x₁ : X} (p : Path.Homotopic.Quotient x₀ x₁) : x₀ ⟶ x₁ := p
+def fromPath {X : TopCat} {x₀ x₁ : X} (p : Path.Homotopic.Quotient x₀ x₁) :
+    FundamentalGroupoid.mk x₀ ⟶ FundamentalGroupoid.mk x₁ := p
 #align fundamental_groupoid.from_path FundamentalGroupoid.fromPath
 
 end FundamentalGroupoid

Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

@@ -32,7 +32,7 @@ open CategoryTheory
 /-- The fundamental group is the automorphism group (vertex group) of the basepoint
 in the fundamental groupoid. -/
 def FundamentalGroup (X : Type u) [TopologicalSpace X] (x : X) :=
-  @Aut (FundamentalGroupoid X) _ x
+  @Aut (FundamentalGroupoid X) _ ⟨x⟩
 #align fundamental_group FundamentalGroup
 
 instance (X : Type u) [TopologicalSpace X] (x : X) : Group (FundamentalGroup X x) := by
@@ -65,7 +65,8 @@ def fundamentalGroupMulEquivOfPathConnected [PathConnectedSpace X] :
 #align fundamental_group.fundamental_group_mul_equiv_of_path_connected FundamentalGroup.fundamentalGroupMulEquivOfPathConnected
 
 /-- An element of the fundamental group as an arrow in the fundamental groupoid. -/
-abbrev toArrow {X : TopCat} {x : X} (p : FundamentalGroup X x) : x ⟶ x :=
+abbrev toArrow {X : TopCat} {x : X} (p : FundamentalGroup X x) :
+    FundamentalGroupoid.mk x ⟶ FundamentalGroupoid.mk x :=
   p.hom
 #align fundamental_group.to_arrow FundamentalGroup.toArrow
 
@@ -75,7 +76,9 @@ abbrev toPath {X : TopCat} {x : X} (p : FundamentalGroup X x) : Path.Homotopic.Q
 #align fundamental_group.to_path FundamentalGroup.toPath
 
 /-- An element of the fundamental group, constructed from an arrow in the fundamental groupoid. -/
-abbrev fromArrow {X : TopCat} {x : X} (p : x ⟶ x) : FundamentalGroup X x where
+abbrev fromArrow {X : TopCat} {x : X}
+    (p : FundamentalGroupoid.mk x ⟶ FundamentalGroupoid.mk x) :
+    FundamentalGroup X x where
   hom := p
   inv := CategoryTheory.Groupoid.inv p
 #align fundamental_group.from_arrow FundamentalGroup.fromArrow

Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

@@ -79,11 +79,12 @@ section Casts
 
 /-- Abbreviation for `eqToHom` that accepts points in a topological space -/
 abbrev hcast {X : TopCat} {x₀ x₁ : X} (hx : x₀ = x₁) : fromTop x₀ ⟶ fromTop x₁ :=
-  eqToHom hx
+  eqToHom <| FundamentalGroupoid.ext _ _ hx
 #align continuous_map.homotopy.hcast ContinuousMap.Homotopy.hcast
 
 @[simp]
-theorem hcast_def {X : TopCat} {x₀ x₁ : X} (hx₀ : x₀ = x₁) : hcast hx₀ = eqToHom hx₀ :=
+theorem hcast_def {X : TopCat} {x₀ x₁ : X} (hx₀ : x₀ = x₁) :
+    hcast hx₀ = eqToHom (FundamentalGroupoid.ext _ _ hx₀) :=
   rfl
 #align continuous_map.homotopy.hcast_def ContinuousMap.Homotopy.hcast_def
 
@@ -103,7 +104,9 @@ private theorem end_path : f x₁ = g x₃ := by convert hfg 1 <;> simp only [Pa
 theorem eq_path_of_eq_image :
     (πₘ f).map ⟦p⟧ = hcast (start_path hfg) ≫ (πₘ g).map ⟦q⟧ ≫ hcast (end_path hfg).symm := by
   rw [Functor.conj_eqToHom_iff_heq
-    ((πₘ f).map ⟦p⟧) ((πₘ g).map ⟦q⟧) (start_path hfg) (end_path hfg)]
+    ((πₘ f).map ⟦p⟧) ((πₘ g).map ⟦q⟧)
+    (FundamentalGroupoid.ext _ _ <| start_path hfg)
+    (FundamentalGroupoid.ext _ _ <| end_path hfg)]
   exact heq_path_of_eq_image hfg
 #align continuous_map.homotopy.eq_path_of_eq_image ContinuousMap.Homotopy.eq_path_of_eq_image
 
@@ -152,7 +155,7 @@ theorem ulift_apply (i : ULift.{u} I) (x : X) : H.uliftMap (i, x) = H (i.down, x
  typechecker. In particular, the first path should be on the ulifted unit interval. -/
 abbrev prodToProdTopI {a₁ a₂ : TopCat.of (ULift I)} {b₁ b₂ : X} (p₁ : fromTop a₁ ⟶ fromTop a₂)
     (p₂ : fromTop b₁ ⟶ fromTop b₂) :=
-  (prodToProdTop (TopCat.of <| ULift I) X).map (X := (a₁, b₁)) (Y := (a₂, b₂)) (p₁, p₂)
+  (prodToProdTop (TopCat.of <| ULift I) X).map (X := (⟨a₁⟩, ⟨b₁⟩)) (Y := (⟨a₂⟩, ⟨b₂⟩)) (p₁, p₂)
 set_option linter.uppercaseLean3 false in
 #align continuous_map.homotopy.prod_to_prod_Top_I ContinuousMap.Homotopy.prodToProdTopI
 
@@ -188,9 +191,11 @@ theorem apply_one_path : (πₘ g).map p = hcast (H.apply_one x₀).symm ≫
 
 /-- Proof that `H.evalAt x = H(0 ⟶ 1, x ⟶ x)`, with the appropriate casts -/
 theorem evalAt_eq (x : X) : ⟦H.evalAt x⟧ = hcast (H.apply_zero x).symm ≫
-    (πₘ H.uliftMap).map (prodToProdTopI uhpath01 (𝟙 x)) ≫ hcast (H.apply_one x).symm.symm := by
+    (πₘ H.uliftMap).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫
+      hcast (H.apply_one x).symm.symm := by
   dsimp only [prodToProdTopI, uhpath01, hcast]
-  refine' (@Functor.conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _ (H.apply_one x).symm).mpr _
+  refine' (@Functor.conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _
+    (FundamentalGroupoid.ext _ _ <| H.apply_one x).symm).mpr _
   simp only [id_eq_path_refl, prodToProdTop_map, Path.Homotopic.prod_lift, map_eq, ←
     Path.Homotopic.map_lift]
   apply Path.Homotopic.hpath_hext; intro; rfl
@@ -225,7 +230,7 @@ variable {X Y : TopCat.{u}} {f g : C(X, Y)} (H : ContinuousMap.Homotopy f g)
 functors `f` and `g` -/
 -- Porting note: couldn't use category arrow `\hom` in statement, needed to expand
 def homotopicMapsNatIso : @Quiver.Hom _ Functor.category.toQuiver (πₘ f) (πₘ g) where
-  app x := ⟦H.evalAt x⟧
+  app x := ⟦H.evalAt x.as⟧
   -- Porting note: Turned `rw` into `erw` in the line below
   naturality x y p := by erw [(H.eq_diag_path p).1, (H.eq_diag_path p).2]
 #align fundamental_groupoid_functor.homotopic_maps_nat_iso FundamentalGroupoidFunctor.homotopicMapsNatIso

Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean

@@ -36,7 +36,9 @@ instance {x y : FundamentalGroupoid PUnit} : Subsingleton (x ⟶ y) := by
 
 /-- Equivalence of groupoids between fundamental groupoid of punit and punit -/
 def punitEquivDiscretePUnit : FundamentalGroupoid PUnit.{u + 1} ≌ Discrete PUnit.{v + 1} :=
-  CategoryTheory.Equivalence.mk (Functor.star _) ((CategoryTheory.Functor.const _).obj PUnit.unit)
+  CategoryTheory.Equivalence.mk
+    (Functor.star _)
+    ((CategoryTheory.Functor.const _).obj ⟨PUnit.unit⟩)
     -- Porting note: was `by decide`
     (NatIso.ofComponents fun _ => eqToIso (by simp))
     (Functor.punitExt _ _)

Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

@@ -54,18 +54,15 @@ theorem proj_map (i : I) (x₀ x₁ : πₓ (TopCat.of (∀ i, X i))) (p : x₀
   rfl
 #align fundamental_groupoid_functor.proj_map FundamentalGroupoidFunctor.proj_map
 
--- Porting note: losing the instance with a concrete category again
-instance : (i : I) → TopologicalSpace (πₓ (X i)).α := fun i => TopCat.topologicalSpace_coe (X i)
-
 /-- The map taking the pi product of a family of fundamental groupoids to the fundamental
 groupoid of the pi product. This is actually an isomorphism (see `piIso`)
 -/
 @[simps]
 def piToPiTop : (∀ i, πₓ (X i)) ⥤ πₓ (TopCat.of (∀ i, X i)) where
-  obj g := g
+  obj g := ⟨fun i => (g i).as⟩
   map p := Path.Homotopic.pi p
   map_id x := by
-    change (Path.Homotopic.pi fun i => 𝟙 (x i)) = _
+    change (Path.Homotopic.pi fun i => ⟦_⟧) = _
     simp only [FundamentalGroupoid.id_eq_path_refl, Path.Homotopic.pi_lift]
     rfl
   map_comp f g := (Path.Homotopic.comp_pi_eq_pi_comp f g).symm
@@ -167,7 +164,7 @@ of the two topological spaces. This is in fact an isomorphism (see `prodIso`).
 -/
 @[simps obj]
 def prodToProdTop : πₓ A × πₓ B ⥤ πₓ (TopCat.of (A × B)) where
-  obj g := g
+  obj g := ⟨g.fst.as, g.snd.as⟩
   map {x y} p :=
     match x, y, p with
     | (x₀, x₁), (y₀, y₁), (p₀, p₁) => @Path.Homotopic.prod _ _ (_) (_) _ _ _ _ p₀ p₁
@@ -205,7 +202,7 @@ def prodIso : CategoryTheory.Grpd.of (πₓ A × πₓ B) ≅ πₓ (TopCat.of (
   inv_hom_id := by
     change (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 _
     apply CategoryTheory.Functor.hext
-    · intros; apply Prod.ext <;> simp <;> rfl
+    · intros; apply FundamentalGroupoid.ext; apply Prod.ext <;> simp <;> rfl
     rintro ⟨x₀, x₁⟩ ⟨y₀, y₁⟩ f
     have := Path.Homotopic.prod_projLeft_projRight f
     -- Porting note: was simpa but TopSpace instances might be getting in the way

Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

@@ -42,7 +42,10 @@ class SimplyConnectedSpace (X : Type*) [TopologicalSpace X] : Prop where
 theorem simply_connected_iff_unique_homotopic (X : Type*) [TopologicalSpace X] :
     SimplyConnectedSpace X ↔
       Nonempty X ∧ ∀ x y : X, Nonempty (Unique (Path.Homotopic.Quotient x y)) := by
-  rw [simply_connected_def, equiv_punit_iff_unique]; rfl
+  simp only [simply_connected_def, equiv_punit_iff_unique,
+    FundamentalGroupoid.nonempty_iff X, and_congr_right_iff, Nonempty.forall]
+  intros
+  exact ⟨fun h _ _ => h _ _, fun h _ _ => h _ _⟩
 #align simply_connected_iff_unique_homotopic simply_connected_iff_unique_homotopic
 
 namespace SimplyConnectedSpace