search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.24k stars 187 forks source link

(c * (c * c)) doesn't unify with (c * c * c) for categories. #957

Closed Alizter closed 5 years ago

Alizter commented 5 years ago

So we set up a coq file in HoTT like this:

Require Import Categories.

Local Open Scope category_scope.

Context {c : PreCategory}.

Then we run Check (c*c*c). and we get

c * c * c
     : Core.PreCategory

Next we run Check ((c*c)*c). and we get

c * c * c
     : Core.PreCategory

Finally we run Check (c*(c*c)). However this time we get

c * (c * c)
     : Core.PreCategory

This stops c * c * c and c*(c*c) from unifying. I presume this stems from assocativity not working for the product of categories.

JasonGross commented 5 years ago

I presume this stems from assocativity not working for the product of categories.

I'm not sure what you mean by this. There's a way in which this stems from the fact that (T * (T * T))%type and ((T * T) * T)%type don't unify as types, and has nothing to do with categories.

Alizter commented 5 years ago

OK then I am serverly misunderstanding how product types work in Coq. Is there some sort of coercion I can have such that coq can unify them?

I was under the impression that Coq unifed (a,(b,c)) with ((a,b),c)

I am trying to write the associator for a monoidal category however this requires me to have (C x C) x C and C x (C x C) to be the same thing.

In my mind the following should work:

Require Import Categories.
Require Import Categories.Functor.
Require Import Categories.FunctorCategory.Morphisms.
Require Import Categories.Functor.Prod.

Local Open Scope category_scope.
Local Open Scope morphism_scope.
Local Open Scope functor_scope.

Context {c : PreCategory}.
  Context {tensor : Functor (c * c) c}.
  Context {unit : c}.
  Context {associator : NaturalIsomorphism
                          (tensor o (1, tensor)) 
                          (tensor o (tensor, 1)) }.
mikeshulman commented 5 years ago

I am not aware of any foundation for mathematics in which A x (B x C) and (A x B) x C are definitionally equal. The best you can get is that with univalence they are typally equal, i.e. related by an identification = element of Id_Type.

mikeshulman commented 5 years ago

Mathematicians often pretend that they are the same when writing informally, which officially means transporting along the canonical isomorphism between them. In particular, to be fully precise, the associator of a monoidal category has to be an isomorphism between two functors C x (C x C) --> C (or the other one, it doesn't matter which), where one of the functors is defined by first applying the isomorphism C x (C x C) \cong (C x C) x C and then multiplying.

Alizter commented 5 years ago

To me this seems like the kind of thing a proof assistant should do automatically. Does coq have any functionality that allows things like this to be done?

On the other hand I have defined a functor like this (perhaps it can be made more compact?)

Definition pa {A B C : PreCategory} : Functor (A * B * C) (A * (B * C)).
Proof.
  simple refine (Build_Functor _ _ _ _ _ _).
  + intros; destruct X, fst; refine (fst, (snd0, snd)).
  + intros; destruct X, fst; refine (fst, (snd0, snd)).
  + auto.
  + auto.
Defined.

Now precomposing with my first argument of the natural transformation in associator makes it work.

spitters commented 5 years ago

There is a plugin for Coq that does associative-commutative rewriting, but I don't think it works for HoTT. As Mike points out, there is higher structure here. https://github.com/coq-community/aac-tactics

mikeshulman commented 5 years ago

There are many things that it seems to the average mathematician that a proof assistant "should" do automatically that proof assistants can't yet do automatically. This is one of the reasons I think it will be a fairly long time until all mathematics is formalized.

spitters commented 5 years ago

There's a new generation of mathematicians being educated...

On Sun, Sep 9, 2018 at 3:58 PM Mike Shulman notifications@github.com wrote:

There are many things that it seems to the average mathematician that a proof assistant "should" do automatically that proof assistants can't yet do automatically. This is one of the reasons I think it will be a fairly long time until all mathematics is formalized.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HoTT/HoTT/issues/957#issuecomment-419717812, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zhSGimzIQt2LRwcFK3LzS-ELYQw8ks5uZR6RgaJpZM4WfiOi .