## Stream: new members

### Topic: extensionality for functors

#### Justus Springer (Mar 23 2021 at 20:21):

Hi,
correct me if I'm wrong: In mathlib, there seems to be no extensionality Lemma for functors.
Moreover, I noticed that I can't even state extensionality for functors without getting a type error:

import category_theory.functor

open category_theory

variables (C D : Type*) [category C] [category D]

--doesn't even typecheck
example (F G : C ⥤ D) (h₁ : F.obj = G.obj) (h₂ : F.map = G.map) : F = G := sorry


and it makes sense, because the types of F.map and G.map are a priori different, but of course they actually aren't because I'm requiring F.obj = G.obj as a hypothesis as well. I remember seeing issues like this in a CS class on Coq once, where because of dependently typed hypothesis, we couldn't even state a particular Lemma. Unfortunately, I don't remember how we worked around this problem, if we did...

Is there a workaround? And how can I prove that two functors are equal, or is this something that we shouldn't even do in mathlib?

#### Markus Himmel (Mar 23 2021 at 20:33):

We actually do have docs#category_theory.functor.ext, which uses docs#category_theory.eq_to_hom to work around the problem you described. As you already guessed, this is rarely a good idea. In the vast majority of cases, it is much better to instead provide a natural isomorphism between the two functors.

#### Markus Himmel (Mar 23 2021 at 20:38):

More generally, unless your category is some kind of partial order, the moment when you start talking about equality of objects, it is probably a good idea to think about whether there is a better approach that avoids this (and talks about isomorphisms instead).

#### Eric Wieser (Mar 23 2021 at 20:44):

Note that you can state the lemma by using docs#heq (==) between the maps

#### Justus Springer (Mar 23 2021 at 20:50):

Oh, I didn't see that one, thanks!

#### Justus Springer (Mar 23 2021 at 20:56):

Markus Himmel said:

More generally, unless your category is some kind of partial order, the moment when you start talking about equality of objects, it is probably a good idea to think about whether there is a better approach that avoids this (and talks about isomorphisms instead).

If we are talking about paper-math, I 100% agree with this statement. But I thought since Lean doesn't have univalence, isomorphisms would be a pain to work with, since we can't rewrite with them. Is this not the case?

#### Justus Springer (Mar 23 2021 at 20:57):

I don't have any experience with isomorphisms in Lean yet, so any additional information about how to properly use them would be nice :)

#### Markus Himmel (Mar 23 2021 at 21:03):

They're not exactly fun to work with, but I would argue that dealing with heq or eq_to_hom is even worse. In my experience, with well-chosen simp lemmas, many isomorphisms that could potentially be annoying are almost invisible.

#### Adam Topaz (Mar 23 2021 at 21:25):

We also have docs#category_theory.functor.hext if you REALLY want to worry about heq

#### Adam Topaz (Mar 23 2021 at 21:27):

These are not marked with @[ext] because you should think twice about using them :wink:

#### Eric Wieser (Mar 23 2021 at 21:45):

How does Coq handle heq?

#### Mario Carneiro (Mar 24 2021 at 00:00):

Not very well, because it doesn't have proof irrelevance

#### Mario Carneiro (Mar 24 2021 at 00:01):

It's possible to define, of course, but it doesn't have a lot of the properties you would want. It's better to use pathovers as in HoTT

#### Mario Carneiro (Mar 24 2021 at 00:05):

inductive path {α} (F : α → Type) {a} (fa : F a) : ∀ {b}, F b → a = b → Prop
| refl : path fa rfl

notation a =[F;p] b := path F a b p


#### Eric Wieser (Mar 24 2021 at 06:53):

I remember seeing a thread about paths a while ago; has it been concluded they're less convenient to work with than heq, or has no one really tried them out seriously in lean?

#### Mario Carneiro (Mar 24 2021 at 06:57):

No one has tried them out seriously. I think they would be better than heq, but not as good as avoiding them entirely using sigma-type encodings

#### Mario Carneiro (Mar 24 2021 at 06:58):

One problem with pathovers is that you eventually find yourself needing pathoverovers too

#### Eric Wieser (Mar 24 2021 at 07:04):

Is path F a b p different to eq.rec a p = b other than having F explicit unlike the C of docs#eq.rec?

#### Eric Wieser (Mar 24 2021 at 10:26):

I tried out using eq.rec instead of ==, but the elaborator makes it harder for me than I'd like:

/-- With heq -/
example {α : Sort*} {β : α → Sort*} {γ : Π a, β a → Sort*}
(x y : Σ a b, γ a b) (h1 : x.1 = y.1) (h2 : x.2.1 == y.2.1) (h3 : x.2.2 == y.2.2) :
x = y :=
begin
cases x, cases y, cases x_snd, cases y_snd, cases h1, cases h2, cases h3, refl
end

@[ext]
def sigma_ext_rec {α : Sort*} {β : α → Sort*} :
∀ {x y : Σ a, β a} (h1 : x.fst = y.fst) (h2 : h1.rec x.2 = y.2), x = y
| ⟨x1, x2⟩ ⟨y1, xy⟩ rfl rfl := rfl

/-- With eq.rec -/
example {α : Sort*} {β : α → Sort*} {γ : Π a, β a → Sort*}
(x y : Σ a b, γ a b)
(h1 : x.1 = y.1)
-- (h1.rec x.2).1 = y.2.1 isn't accepted by the elaborator
(h2 : (eq.rec x.2 h1 : Σ a, γ y.1 a).1 = y.2.1)
-- h2.rec (h1.rec x.2).2 = y.2.2 isn't accepted by the elaborator
(h3 : (eq.rec (eq.rec x.2 h1 : Σ a, γ y.1 a).2 h2 : γ y.1 y.2.1) = y.2.2) :
x = y :=
begin
-- the previous proof would work too
ext, exact h3,
end


Last updated: May 14 2021 at 06:16 UTC