feat(category_theory): make defining groupoids easier (#2360)

The point of this PR is to lower the burden of proof in showing that a category is a groupoid. Rather than constructing well-defined two-sided inverses everywhere, with `groupoid.of_trunc_split_mono` you'll only need to show that every morphism has some retraction. This makes defining the free groupoid painless. There the retractions are defined by recursion on a quotient, so this saves the work of showing that all the retractions agree.

I used `trunc` instead of `nonempty` to avoid choice / noncomputability.

I don't understand why the @'s are needed: it seems Lean doesn't know what category structure C has without specifying it?

src/category_theory/epi_mono.lean

@@ -116,6 +116,18 @@ instance split_mono.mono {X Y : C} (f : X ⟶ Y) [split_mono f] : mono f :=
 instance split_epi.epi {X Y : C} (f : X ⟶ Y) [split_epi f] : epi f :=
 { left_cancellation := λ Z g h w, begin replace w := section_ f ≫= w, simpa using w, end }
 
+/-- Every split mono whose retraction is mono is an iso. -/
+def is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f]
+  : is_iso f :=
+{ inv := retraction f,
+  inv_hom_id' := (cancel_mono_id $ retraction f).mp (by simp) }
+
+/-- Every split epi whose section is epi is an iso. -/
+def is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f]
+  : is_iso f :=
+{ inv := section_ f,
+  hom_inv_id' := (cancel_epi_id $ section_ f).mp (by simp) }
+
 section
 variables {D : Type u₂} [𝒟 : category.{v₂} D]
 include 𝒟

src/category_theory/groupoid.lean

@@ -1,11 +1,12 @@
 /-
 Copyright (c) 2018 Reid Barton All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Reid Barton
+Authors: Reid Barton, Scott Morrison, David Wärn
 -/
 
 import category_theory.category
 import category_theory.isomorphism
+import category_theory.epi_mono
 import data.equiv.basic
 
 namespace category_theory
@@ -48,4 +49,27 @@ def groupoid.iso_equiv_hom : (X ≅ Y) ≃ (X ⟶ Y) :=
 
 end
 
+section
+
+variables {C : Type u} [𝒞 : category.{v} C]
+include 𝒞
+
+/-- A category where every morphism `is_iso` is a groupoid. -/
+def groupoid.of_is_iso (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), is_iso.{v} f) : groupoid.{v} C :=
+{ inv := λ X Y f, (all_is_iso f).inv }
+
+/-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
+def groupoid.of_trunc_split_mono
+  (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono.{v} f)) :
+  groupoid.{v} C :=
+begin
+  apply groupoid.of_is_iso,
+  intros X Y f,
+  trunc_cases all_split_mono f,
+  trunc_cases all_split_mono (retraction f),
+  apply is_iso.of_mono_retraction,
+end
+
+end
+
 end category_theory

src/tactic/basic.lean

@@ -29,5 +29,6 @@ import
   tactic.simps
   tactic.split_ifs
   tactic.squeeze
+  tactic.trunc_cases
   tactic.where
   tactic.hint