feat(category/equiv_functor): type-level functoriality w.r.t. equiv (#2255)

* feat(data/equiv/functor): bifunctor.map_equiv

* start

* sketch of equiv_functor

* update

* removing unimpressive inhabited example; easier later

* omit

* revert unnecessary change

* fix doc-string

* fix names

* finish fix

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: kim-em

src/category/equiv_functor.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Scott Morrison
+-/
+
+import category_theory.category
+import data.equiv.functor
+
+/-!
+# Functions functorial with respect to equivalences
+
+An `equiv_functor` is a function from `Type → Type` equipped with the additional data of
+coherently mapping equivalences to equivalences.
+
+In categorical language, it is an endofunctor of the "core" of the category `Type`.
+-/
+
+universes u₀ u₁ u₂ v₀ v₁ v₂
+
+open function
+
+/--
+An `equiv_functor` is only functorial with respect to equivalences.
+
+To construct an `equiv_functor`, it suffices to supply just the function `f α → f β` from
+an equivalence `α ≃ β`, and then prove the functor laws. It's then a consequence that
+this function is part of an equivalence, provided by `equiv_functor.map_equiv`.
+-/
+class equiv_functor (f : Type u₀ → Type u₁) :=
+(map : Π {α β}, (α ≃ β) → (f α → f β))
+(map_refl' : Π α, map (equiv.refl α) = @id (f α) . obviously)
+(map_trans' : Π {α β γ} (k : α ≃ β) (h : β ≃ γ),
+  map (k.trans h) = (map h) ∘ (map k) . obviously)
+
+restate_axiom equiv_functor.map_refl'
+restate_axiom equiv_functor.map_trans'
+attribute [simp] equiv_functor.map_refl
+
+namespace equiv_functor
+
+section
+variables (f : Type u₀ → Type u₁) [equiv_functor f] {α β : Type u₀} (e : α ≃ β)
+
+/-- An `equiv_functor` in fact takes every equiv to an equiv. -/
+def map_equiv :
+  f α ≃ f β :=
+{ to_fun := equiv_functor.map e,
+  inv_fun := equiv_functor.map e.symm,
+  left_inv := λ x, begin convert (congr_fun (equiv_functor.map_trans f e e.symm) x).symm, simp, end,
+  right_inv := λ y, begin convert (congr_fun (equiv_functor.map_trans f e.symm e) y).symm, simp, end, }
+
+@[simp] lemma map_equiv_apply (x : f α) :
+  map_equiv f e x = equiv_functor.map e x := rfl
+
+@[simp] lemma map_equiv_symm_apply (y : f β) :
+  (map_equiv f e).symm y = equiv_functor.map e.symm y := rfl
+end
+
+@[priority 100]
+instance of_is_lawful_functor
+  (f : Type u₀ → Type u₁) [functor f] [is_lawful_functor f] : equiv_functor f :=
+{ map := λ α β e, functor.map e,
+  map_refl' := λ α, by { ext, apply is_lawful_functor.id_map, },
+  map_trans' := λ α β γ k h, by { ext x, apply (is_lawful_functor.comp_map k h x), } }
+
+-- TODO Include more examples here;
+-- once `equiv_rw` is available these are hopefully easy to construct,
+-- and in turn make `equiv_rw` more powerful.
+instance equiv_functor_unique : equiv_functor unique :=
+{ map := λ α β e, equiv.unique_congr e, }
+
+end equiv_functor

src/category_theory/core.lean

@@ -6,6 +6,8 @@ Authors: Scott Morrison
 
 import category_theory.groupoid
 import category_theory.whiskering
+import category.equiv_functor
+import category_theory.types
 
 namespace category_theory
 
@@ -47,4 +49,24 @@ def functor_to_core (F : G ⥤ C) : G ⥤ core C :=
 def forget_functor_to_core : (G ⥤ core C) ⥤ (G ⥤ C) := (whiskering_right _ _ _).obj inclusion
 end core
 
+omit 𝒞
+
+/--
+`of_equiv_functor m` lifts a type-level `equiv_functor`
+to a categorical functor `core (Type u₁) ⥤ core (Type u₂)`.
+-/
+def of_equiv_functor (m : Type u₁ → Type u₂) [equiv_functor m] :
+  core (Type u₁) ⥤ core (Type u₂) :=
+{ obj       := m,
+  map       := λ α β f, (equiv_functor.map_equiv m f.to_equiv).to_iso,
+  -- These are not very pretty.
+  map_id' := λ α, begin ext, exact (congr_fun (equiv_functor.map_refl _ _) x), end,
+  map_comp' := λ α β γ f g,
+  begin
+    ext,
+    simp only [equiv_functor.map_equiv_apply, equiv.to_iso_hom,
+      function.comp_app, core.comp_hom, types_comp],
+    erw [iso.to_equiv_comp, equiv_functor.map_trans],
+  end, }
+
 end category_theory

src/category_theory/types.lean

@@ -160,6 +160,7 @@ def to_iso (e : X ≃ Y) : X ≅ Y :=
 end equiv
 
 namespace category_theory.iso
+open category_theory
 
 universe u
 
@@ -174,6 +175,10 @@ def to_equiv (i : X ≅ Y) : X ≃ Y :=
 @[simp] lemma to_equiv_fun (i : X ≅ Y) : (i.to_equiv : X → Y) = i.hom := rfl
 @[simp] lemma to_equiv_symm_fun (i : X ≅ Y) : (i.to_equiv.symm : Y → X) = i.inv := rfl
 
+@[simp] lemma to_equiv_id (X : Type u) : (iso.refl X).to_equiv = equiv.refl X := rfl
+@[simp] lemma to_equiv_comp {X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z) :
+  (f ≪≫ g).to_equiv = f.to_equiv.trans (g.to_equiv) := rfl
+
 end category_theory.iso
 
 

src/data/equiv/basic.lean

@@ -298,7 +298,7 @@ calc (false → α) ≃ (empty → α) : arrow_congr false_equiv_empty (equiv.re
 
 end
 
-@[congr] def prod_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ :β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂ :=
+@[congr] def prod_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂ :=
 ⟨λp, (e₁ p.1, e₂ p.2), λp, (e₁.symm p.1, e₂.symm p.2),
    λ ⟨a, b⟩, show (e₁.symm (e₁ a), e₂.symm (e₂ b)) = (a, b), by rw [symm_apply_apply, symm_apply_apply],
    λ ⟨a, b⟩, show (e₁ (e₁.symm a), e₂ (e₂.symm b)) = (a, b), by rw [apply_symm_apply, apply_symm_apply]⟩

src/logic/unique.lean

@@ -3,11 +3,13 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
+import tactic.ext
 
 universes u v w
 
 variables {α : Sort u} {β : Sort v} {γ : Sort w}
 
+@[ext]
 structure unique (α : Sort u) extends inhabited α :=
 (uniq : ∀ a:α, a = default)