Zulip Chat Archive

Stream: new members

Topic: extensionality for functors


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Eric Wieser (Mar 23 2021 at 20:44):

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

view this post on Zulip Justus Springer (Mar 23 2021 at 20:50):

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

view this post on Zulip 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?

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Mar 23 2021 at 21:25):

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

view this post on Zulip Adam Topaz (Mar 23 2021 at 21:27):

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

view this post on Zulip Eric Wieser (Mar 23 2021 at 21:45):

How does Coq handle heq?

view this post on Zulip Mario Carneiro (Mar 24 2021 at 00:00):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 24 2021 at 06:58):

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

view this post on Zulip 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?

view this post on Zulip 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