chore(category/equivalence): cleanup (#3164)

Previously some "shorthands" like
```
@[simp] def unit (e : C ≌ D) : 𝟭 C ⟶ e.functor ⋙ e.inverse := e.unit_iso.hom
```
had been added in `equivalence.lean`.

These were a bit annoying, as even though they were marked as `simp` sometimes the syntactic difference between `e.unit` and `e.unit_iso.hom` would get in the way of tactics working.

This PR turns these into abbreviations.

This comes at a slight cost: apparently expressions like `{ X := X }.Y` won't reduce when `.Y` is an abbreviation for `.X.Z`, so we add some `@[simp]` lemmas back in to achieve this.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/closed/cartesian.lean

@@ -335,14 +335,14 @@ def cartesian_closed_of_equiv (e : C ≌ D) [h : cartesian_closed C] : cartesian
               by simpa [←prod_map_id_comp, prod_map_id_id]⟩, },
       { intros Y Z g,
         simp only [prod_comparison, inv_prod_comparison_map_fst, inv_prod_comparison_map_snd,
-                  prod.lift_map, equivalence.unit_inv, functor.comp_map,
-                  prod_functor_obj_map, assoc, comp_id, iso.trans_hom, as_iso_hom],
+          prod.lift_map, functor.comp_map, prod_functor_obj_map, assoc, comp_id,
+          iso.trans_hom, as_iso_hom],
         apply prod.hom_ext,
         { rw [assoc, prod.lift_fst, prod.lift_fst, ←functor.map_comp,
             limits.prod.map_fst, comp_id], },
         { rw [assoc, prod.lift_snd, prod.lift_snd, ←functor.map_comp_assoc, limits.prod.map_snd],
-          simp only [equivalence.unit, equivalence.unit_inv, nat_iso.hom_inv_id_app, assoc,
-            equivalence.inv_fun_map, functor.map_comp, comp_id],
+          simp only [nat_iso.hom_inv_id_app, assoc, equivalence.inv_fun_map,
+            functor.map_comp, comp_id],
           erw comp_id, }, },
       { have : is_left_adjoint (e.functor ⋙ prod_functor.obj X ⋙ e.inverse) :=
           by exactI adjunction.left_adjoint_of_nat_iso this.symm,

src/category_theory/equivalence.lean

@@ -36,22 +36,28 @@ variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D
 
 namespace equivalence
 
-@[simp] def unit (e : C ≌ D) : 𝟭 C ⟶ e.functor ⋙ e.inverse := e.unit_iso.hom
-@[simp] def counit (e : C ≌ D) : e.inverse ⋙ e.functor ⟶ 𝟭 D := e.counit_iso.hom
-@[simp] def unit_inv (e : C ≌ D) : e.functor ⋙ e.inverse ⟶ 𝟭 C := e.unit_iso.inv
-@[simp] def counit_inv (e : C ≌ D) : 𝟭 D ⟶ e.inverse ⋙ e.functor := e.counit_iso.inv
-
-lemma unit_def (e : C ≌ D) : e.unit_iso.hom = e.unit := rfl
-lemma counit_def (e : C ≌ D) : e.counit_iso.hom = e.counit := rfl
-lemma unit_inv_def (e : C ≌ D) : e.unit_iso.inv = e.unit_inv := rfl
-lemma counit_inv_def (e : C ≌ D) : e.counit_iso.inv = e.counit_inv := rfl
-
-@[simp] lemma functor_unit_comp (e : C ≌ D) (X : C) : e.functor.map (e.unit_iso.hom.app X) ≫
-  e.counit_iso.hom.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
+abbreviation unit (e : C ≌ D) : 𝟭 C ⟶ e.functor ⋙ e.inverse := e.unit_iso.hom
+abbreviation counit (e : C ≌ D) : e.inverse ⋙ e.functor ⟶ 𝟭 D := e.counit_iso.hom
+abbreviation unit_inv (e : C ≌ D) : e.functor ⋙ e.inverse ⟶ 𝟭 C := e.unit_iso.inv
+abbreviation counit_inv (e : C ≌ D) : 𝟭 D ⟶ e.inverse ⋙ e.functor := e.counit_iso.inv
+
+/- While these abbreviations are convenient, they also cause some trouble,
+preventing structure projections from unfolding. -/
+@[simp] lemma equivalence_mk'_unit (functor inverse unit_iso counit_iso f) :
+  (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit = unit_iso.hom := rfl
+@[simp] lemma equivalence_mk'_counit (functor inverse unit_iso counit_iso f) :
+  (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit = counit_iso.hom := rfl
+@[simp] lemma equivalence_mk'_unit_inv (functor inverse unit_iso counit_iso f) :
+  (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit_inv = unit_iso.inv := rfl
+@[simp] lemma equivalence_mk'_counit_inv (functor inverse unit_iso counit_iso f) :
+  (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit_inv = counit_iso.inv := rfl
+
+@[simp] lemma functor_unit_comp (e : C ≌ D) (X : C) : e.functor.map (e.unit.app X) ≫
+  e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
 e.functor_unit_iso_comp X
 
 @[simp] lemma counit_inv_functor_comp (e : C ≌ D) (X : C) :
-  e.counit_iso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unit_iso.inv.app X) = 𝟙 (e.functor.obj X) :=
+  e.counit_inv.app (e.functor.obj X) ≫ e.functor.map (e.unit_inv.app X) = 𝟙 (e.functor.obj X) :=
 begin
   erw [iso.inv_eq_inv
     (e.functor.map_iso (e.unit_iso.app X) ≪≫ e.counit_iso.app (e.functor.obj X)) (iso.refl _)],
@@ -69,11 +75,11 @@ by { erw [←iso.hom_comp_eq_id (e.functor.map_iso (e.unit_iso.app X)), functor_
 /-- The other triangle equality. The proof follows the following proof in Globular:
   http://globular.science/1905.001 -/
 @[simp] lemma unit_inverse_comp (e : C ≌ D) (Y : D) :
-  e.unit_iso.hom.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit_iso.hom.app Y) = 𝟙 (e.inverse.obj Y) :=
+  e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y) :=
 begin
   rw [←id_comp (e.inverse.map _), ←map_id e.inverse, ←counit_inv_functor_comp, map_comp,
       ←iso.hom_inv_id_assoc (e.unit_iso.app _) (e.inverse.map (e.functor.map _)),
-      app_hom, app_inv, unit_def, unit_inv_def],
+      app_hom, app_inv],
   slice_lhs 2 3 { erw [e.unit.naturality] },
   slice_lhs 1 2 { erw [e.unit.naturality] },
   slice_lhs 4 4
@@ -90,7 +96,7 @@ begin
 end
 
 @[simp] lemma inverse_counit_inv_comp (e : C ≌ D) (Y : D) :
-  e.inverse.map (e.counit_iso.inv.app Y) ≫ e.unit_iso.inv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) :=
+  e.inverse.map (e.counit_inv.app Y) ≫ e.unit_inv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) :=
 begin
   erw [iso.inv_eq_inv
     (e.unit_iso.app (e.inverse.obj Y) ≪≫ e.inverse.map_iso (e.counit_iso.app Y)) (iso.refl _)],
@@ -253,6 +259,15 @@ is_equivalence.inverse F
 instance is_equivalence_inv (F : C ⥤ D) [is_equivalence F] : is_equivalence F.inv :=
 is_equivalence.of_equivalence F.as_equivalence.symm
 
+@[simp] lemma as_equivalence_functor (F : C ⥤ D) [is_equivalence F] :
+  F.as_equivalence.functor = F := rfl
+
+@[simp] lemma as_equivalence_inverse (F : C ⥤ D) [is_equivalence F] :
+  F.as_equivalence.inverse = inv F := rfl
+
+@[simp] lemma inv_inv (F : C ⥤ D) [is_equivalence F] :
+  inv (inv F) = F := rfl
+
 def fun_inv_id (F : C ⥤ D) [is_equivalence F] : F ⋙ F.inv ≅ 𝟭 C :=
 is_equivalence.unit_iso.symm
 
@@ -267,6 +282,24 @@ is_equivalence.of_equivalence (equivalence.trans (as_equivalence F) (as_equivale
 
 end functor
 
+namespace equivalence
+
+@[simp]
+lemma functor_inv (E : C ≌ D) : E.functor.inv = E.inverse := rfl
+
+@[simp]
+lemma inverse_inv (E : C ≌ D) : E.inverse.inv = E.functor := rfl
+
+@[simp]
+lemma functor_as_equivalence (E : C ≌ D) : E.functor.as_equivalence = E :=
+by { cases E, congr, }
+
+@[simp]
+lemma inverse_as_equivalence (E : C ≌ D) : E.inverse.as_equivalence = E.symm :=
+by { cases E, congr, }
+
+end equivalence
+
 namespace is_equivalence
 
 @[simp] lemma fun_inv_map (F : C ⥤ D) [is_equivalence F] (X Y : D) (f : X ⟶ Y) :