jwiegley / category-theory Goto Github PK

Lib/Foundation.v defines notations for ∀ , ∃, and λ

If user code imports both Category.Lib and Utf8 from the Coq standard library, we get the following error message

Error: Notation "∀ _ .. _ , _" is already defined at level 200 with arguments
binder, constr at level 200 while it is now required to be at level 10
with arguments binder, constr at level 200.

The following patch seems enough to work around this issue: I confirmed category-theory compiles and so does my code.
Before proposing a pull request, I am curious about your feedback on this. I must admit my patch is pretty arbitrary, it ressembles the notation definition from the Coq standard library to avoid conflicts.

diff --git a/Lib/Foundation.v b/Lib/Foundation.v
index 82f7455..560a8c2 100644
--- a/Lib/Foundation.v
+++ b/Lib/Foundation.v
@@ -31,7 +31,7 @@ Arguments Basics.arrow _ _ /.
 Arguments Datatypes.id {_} _ /.
 
 Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)
-  (at level 200, x binder, y binder, right associativity) :
+  (at level 10, x binder, y binder, P at level 200, right associativity) :
   category_theory_scope.
 
 Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
@@ -40,7 +40,7 @@ Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
   category_theory_scope.
 
 Notation "∃  x .. y , P" := (exists x, .. (exists y, P) ..)
-  (at level 200, x binder, y binder, right associativity) :
+  (at level 10, x binder, y binder, P at level 200, right associativity) :
   category_theory_scope.
 
 Notation "x → y" := (x -> y)
@@ -55,5 +55,5 @@ Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.
 Infix "∨" := sum (at level 85, right associativity) : category_theory_scope.
 
 Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
-  (at level 200, x binder, y binder, right associativity) :
+  (at level 10, x binder, y binder, t at level 200, right associativity) :
   category_theory_scope.

Thanks,

This library and HoTT/HoTT have similar design for their central Category classes. However, they export a nice constructor that fills in the equivalent of comp_assoc_sym automagically.

This definition:

Class Setoid A := {
  equiv : crelation A;
  setoid_equiv :> Equivalence equiv
}.

is identical to the one from the standard library:

Class Setoid A := {
  equiv : relation A ;
  setoid_equiv :> Equivalence equiv }.

Is there any reason not to use the standard library's definition?

Tl; dr: The category Cat is defined "incorrectly", in particular its setoid hom equivalence relation is wrong (it does not agree with the ZFC definition of equality between functors). I propose that we redefine the category Cat with the "correct" setoid hom equivalence relation defined in StrictCat. This would be a long term project as obviously the category Cat is used in many places in the library.

Longer version:
As it stands, most of the library is consistent with ZFC-style classical mathematics. It does not use the law of excluded middle or UIP, so it admits interpretations in other theories such as homotopy type theory, etc. (Although due to technical issues with the propositional erasure in the extraction backend, the univalence axiom is not compatible with use of the sort Prop, so it would require a substantial and fairly unrealistic rewrite of the library to assume that axiom.)

In interpreting this library in the context of ZFC, you would generally quotient out by the setoid relation on the homsets of a category, because ZFC can prove function extensionality. This is why we want to use setoid homs, because Coq lacks function extensionality. Thus, when defining any concrete category whose objects are types with additional structure and whose morphisms are functions, we would generally want the setoid equivalence relationship on morphisms to be given by f \approx g := \forall x. f x = g x.
Indeed this is the case for most concrete categories in the library. An exception is the category Cat, where we identify two functors if they are naturally isomorphic. This is inconsistent with equality of functors in ZFC. The ZFC definition of equality between functors would be that two functors F, G are equal if Fx = Gx for all objects and F(f) = G(f) for all morphisms, appropriately transported along equalities.
In homotopy type theory this would be an acceptable definition for univalent categories but because we are not assuming the univalence axiom we do not get any benefits from defining things this way, so there is no good reason to appeal to homotopy type theory principles here. The downside is that it becomes impossible to define functors from the category Cat into any other category if it does not send naturally isomorphic functors to setoid-equivalent morphisms.
In a previous PR I gave an example of such a functor, namely the functor Cat -> Graph which sends each category to its underlying directed graph and sends each functor to its graph isomorphism. This is a well defined functor in ZFC but is not a well-defined functor in the current library, because it does not respect natural isomorphism of functors, which is why I created the alternative category StrictCat of categories and functors satisfying strict equality.

the commit seems to indicate the library would work for 8.12 but it doesn't work for me:

File "./Theory/Isomorphism.v", line 89, characters 29-33:
Error:
 (in proof isomorphism_equiv_equivalence_obligation_2): Attempt to save an incomplete proof

Makefile.coq:715: recipe for target 'Theory/Isomorphism.vo' failed
make[2]: *** [Theory/Isomorphism.vo] Error 1
File "./Lib/MapDecide.v", line 333, characters 29-30:
Error:
Syntax error: [constr:operconstr level 200] expected after '[' (in [constr:operconstr]).

coqc -v
The Coq Proof Assistant, version 8.12.0 (September 2020)
compiled on Sep 1 2020 1:01:58 with OCaml 4.07.1

which Coq version works for you?

So here is some code in Category.v
Class Category := {
ob : Type;
uhom := Type : Type;
hom : ob → ob → uhom where "a ~> b" := (hom a b);
...

what will happend if hom is ob -> ob -> Type instead, why wont universe polymorphism work?

I suggest some reorganization and renaming in Structure/Monoidal/Cartesian.v and Structure/Monoidal/Cartesian/Cartesian.v.

There are two relations between monoidal products and Cartesian products:

1. Every Cartesian product is a monoidal product.
2. A monoidal product which is both semicartesian and relevant is a Cartesian product, this is the result by by Heunen and Vicary proven in Structure/Monoidal/Cartesian.v.

The second theorem is important and interesting, but I don't expect it to be actually heavily used by users of the library. Instead, I suspect that if a user wants to prove that their category is Cartesian, they will show that for each pair of objects x, y there is an object z with the universal property of the Cartesian product. I have never personally needed or used theorem 2 to prove that a concrete category has a Cartesian product.

On the other hand, 1. is obviously very important, because it allows us to prove theorems about general monoidal products which automatically hold for Cartesian products. I'm not aware of a proof of 1. in the library at this moment. It should be added. I can try to do this when I get a chance.

I also suggest reorganizing things to deemphasize the proof of theorem 2 in order to make it easier to find the proof of theorem 1. I think a file named Monoidal/Cartesian.v which contains a typeclass called "CartesianMonoidal" and proves that a "CartesianMonoidal" product is Cartesian is likely to be misleading to readers who are looking for a proof that a Cartesian category is also a monoidal category. Furthermore it is defined as a typeclass which is probably unnecessary as, realistically, this theorem is applied rarely enough that it doesn't need typeclass resolution.

I would suggest we simply delete the typeclass CartesianMonoidal and just prove the result by separately assuming the two typeclasses RelevantMonoidal and Semicartesian. A pair of only two assumptions does not need to be bundled together, and the choice of bundle name pollutes the library namespace. We should also rename the files "Monoidal/Cartesian.v" and "Monoidal/Cartesian/Cartesian.v" to something that does less overloading of the heavily used terms "Monoidal" and "Cartesian" such as, for example, "Heunen_Vicary.v".

The page http://newartisans.com/2017/05/monads-are-monoids/ contains three broken links to two URLs:

• https://github.com/jwiegley/category-theory/blob/master/Isomorphism/Monoid/Monad.v#L22
• https://github.com/jwiegley/category-theory/blob/master/Isomorphism/Adjunction/Monad.v#L23

Hi guys! I ran make and got the following error:

File "./Structure/Limit/Kan/Extension.v", line 65, characters 17-19:
Error: The reference X0 was not found in the current environment.

Coq version is 8.9.0.

Best regards,
Vladimir.

Any plans to release this on OPAM? :)

Sorry to ask a stupid question but I just can't build from master branch. I am wonder how am I supposed to build? I am using Coq 8.8.1 and equations, but it keeps fail to build with follow messages:

NOT IN _CoqProject: Instance/LambdaOld.v
NOT IN _CoqProject: Instance/Lambda/Lec1.v
NOT IN _CoqProject: Instance/Lambda/Connect.v
NOT IN _CoqProject: Instance/Lambda/Nominal.v
NOT IN _CoqProject: Instance/Lambda/Lemmas.v
NOT IN _CoqProject: Instance/Lambda/Definitions.v
NOT IN _CoqProject: Instance/Lambda/Lec3.v
NOT IN _CoqProject: Instance/Lambda/Lec2.v
make -j -f Makefile.coq  # TIMECMD=time
make[1]: Entering directory '/home/hu/projects/category-theory'
make[2]: *** No rule to make target 'Instance/Lambda/Definitions.vo', needed by 'Instance/Lambda.vo'.  Stop.
COQC Lib/Datatypes.v
make[2]: *** Waiting for unfinished jobs....
File "./Lib/Datatypes.v", line 212, characters 0-4:
Error:
Illegal application: 
The term "list_equivalence_obligation_1" of type
 "∀ (A : Type) (H : Setoid A), Reflexive list_equiv"
cannot be applied to the terms
 "A" : "Type"
 "H" : "Setoid A"
The 1st term has type "Type@{Category.Lib.Datatypes.1007}"
which should be coercible to "Type@{Category.Lib.Datatypes.1020}".

Makefile.coq:656: recipe for target 'Lib/Datatypes.vo' failed
make[2]: *** [Lib/Datatypes.vo] Error 1
Makefile.coq:317: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/hu/projects/category-theory'
Makefile:2: recipe for target 'all' failed
make: *** [all] Error 2

Even if I added those missing files to _CoqProject, it still fails to build, not to mention the universe inconsistency. How should I proceed?

Also, it seems Lambda depends on Metalib, which is not stated as dependency in README. Can I just skip Lambda entirely?

With Printing Universes enabled, the full definition is as follows:

Sets_Terminal@{u} = 
{|
  Terminal.terminal_obj := {| carrier := poly_unit@{Set}; is_setoid := Unit_Setoid@{Set} |};
  Terminal.one :=
    λ x : obj[Sets@{Set Set u Set Set}],
    {| morphism := λ _ : x, ttt@{Set}; proper_morphism := Sets.Sets_Terminal_obligation_1@{u} x |};
  Terminal.one_unique :=
    λ (x : obj[Sets@{Set Set u Set Set}])
    (f
     g : x ~{ Sets@{Set Set u Set Set}
         }~> {| carrier := poly_unit@{Set}; is_setoid := Unit_Setoid@{Set} |}),
    Sets.Sets_Terminal_obligation_2@{u} x f g
|}
     : Terminal.Terminal@{u Set}
(* u |= Set < u *)

This imposes a lot of unnecessary constraints on various universes to be Set, which then quickly propagates throughout the code from wherever Sets_Terminal is used.

Hi, I'm trying to update the version of this library in nixpkgs, but when I add the following lines to the default.nix there:

    "8.8" = {
      version = "20180705";
      rev = "2685dc91f528dc3e82f17a1c32804a94d2ee8ed7";
      sha256 = "0ll22lfzjglnvvf4p0vwk8crwn2c5lkawd85wr3qzcrwnpp5dc43";
    };

and

    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ];

I get this error when building:

File "./Lib/Nomega.v", line 92, characters 2-21:
Warning: Nge is N.ge [compatibility-notation,deprecated]
COQC Lib/Tactics.v
COQC Lib/Datatypes.v
COQC Lib/Equality.v
Closed under the global context
     = tt
     : typeD (fun _ : type => unit) Ty
     = 5
     : typeD (fun _ : type => nat) Ty
File "./Lib/Datatypes.v", line 212, characters 0-4:
Error:
Illegal application:
The term "list_equivalence_obligation_1" of type
 "∀ (A : Type) (H : Setoid A), Reflexive list_equiv"
cannot be applied to the terms
 "A" : "Type"
 "H" : "Setoid A"
The 1st term has type "Type@{Category.Lib.Datatypes.1007}"
which should be coercible to "Type@{Category.Lib.Datatypes.1020}".

Is this library compatible with Coq 8.8?

From Theory/Functor.v -

Class Full `(F : C ⟶ D) := {
  prefmap {x y} (g : F x ~> F y) : x ~> y;

  prefmap_respects {x y} : Proper (equiv ==> equiv) (@prefmap x y);

  prefmap_id : ∀ x, @prefmap x x id ≈ id;
  prefmap_comp : ∀ x y z (f : F y ~> F z) (g : F x ~> F y),
    prefmap (f ∘ g) ≈ prefmap f ∘ prefmap g;

  fmap_sur {x y} (g : F x ~> F y) : fmap[F] (prefmap g) ≈ g
}.

This definition of 'full' is nonstandard. Do you have a motivation/justification for this choice of definition?

I would advocate instead

Class Full `(F : C ⟶ D) := {
  prefmap {x y} (g : F x ~> F y) : x ~> y;
  fmap_sur {x y} (g : F x ~> F y) : fmap[F] (prefmap g) ≈ g
}.

Or for modularity, define what it means for a map of setoids to be surjective and use that definition.

The question of whether prefmap should respect equality is more an issue of constructive mathematics than of category theory but in Bishop-style constructive math you do not require existence to respect equality.

Hi, I came across your repo and tried to get to the pdf file mentioned. However it is not active anymore. Is it possible to include it in the repo itself? Thanks for your help.

Hi John,

I proved the characterization of an adjunction as comma categories. Cheers.

comma-adjunction.pdf

Regards,
Sven

Hi, the file defines identity isos and iso composition. The equivalence relation for isos defines the same isos for reflexivity and transitivity. You can remove one of these definitions.
Best,
Sven

The definition of Poset in Instance/Poset.v currently is:

Definition Poset {C : Category} `{R : relation C}
           `(P : PreOrder C R) `{Asymmetric C R} : Category := Proset P.

I think there are two issues:

1. C should only be a Type and not a category (the morphism structure isn't used anywhere as far as I can see)
2. The relation R should be Antisymmetric instead of Asymmetric.

This second issue implies that all inhabitants of Poset are empty, i.e. any element of a poset leads to a contradiction:

Require Import Category.Lib.
Require Import Category.Theory.Category.
Require Import Category.Instance.Proset.

Require Import Coq.Classes.Equivalence.
Require Import Coq.Relations.Relation_Definitions.

Generalizable All Variables.
Set Implicit Arguments.

Definition Poset {C : Type} `{R : relation C}
           `(P : PreOrder C R) `{Asymmetric C R} : Category := Proset P.

Theorem there_is_no_poset
  {C : Type} `(P : PreOrder C R) `{Asymmetric C R} :
  Poset P -> False.
Proof.
  intro x.
  simpl in *.
  destruct P as [refl _].
  eapply H; unshelve apply (refl x); apply (refl x).
Qed.

I assume the definition should be revised as follows:

Definition Poset {C : Type} `{R : relation C}
           `(P : PreOrder C R) `{Antisymmetric C R} : Category := Proset P.

If there aren't any further subtleties that I missed, I can prepare a PR.