Constructing the category of categories

Miscellaneous
1

[Posting in Misc since this is more of a mathematics question than a Rocq-specific question.]

This is an excerpt of a development of a “theory of categories”, where I get stuck at defining the category of categories, aka the category Cat.

What (minimal, possibly) axiom/principle am I missing here to prove the needed properties? (E.g. I cannot think of any extensionality axiom that would help here.)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Strongly Strict Implicit.
Unset Contextual Implicit.
Unset Reversible Pattern Implicit.
Unset Printing Implicit Defensive.

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Cumulativity Weak Constraints.
Unset Universe Minimization ToSet.

From Coq Require Import Program.


(** The type of "categories". *)
Structure Cat@{i o} : Type@{o} :=
  mkCat {
    Ob : Type@{i};
    Hom : Ob -> Ob -> Type@{i};
    ident : forall x,
      Hom x x;
    comp : forall x y z,  (* diagrammatic *)
      Hom x y ->
      Hom y z ->
      Hom x z;
    comp_unitL : forall x y,
      forall (f : Hom x y),
        comp (ident x) f = f;
    comp_unitR : forall x y,
      forall (f : Hom x y),
        comp f (ident y) = f;
    comp_assoc : forall w x y z,
      forall (f : Hom w x),
      forall (g : Hom x y),
      forall (h : Hom y z),
        comp f (comp g h) = comp (comp f g) h;
  } as C.
Arguments Hom : clear implicits.


(** The type of "functors" from [B] to [C]. *)
Structure Fun@{i o} (B C : Cat@{i o}) : Type@{o} :=
  mkFun {
    fOb : Ob B -> Ob C;
    fHom : forall x y,
      Hom B x y -> Hom C (fOb x) (fOb y);
    fident_prop : forall x,
      fHom (ident x) = ident (fOb x);
    fcomp_prop : forall x y z,
      forall (f : Hom B x y),
      forall (g : Hom B y z),
        fHom (comp f g) = comp (fHom f) (fHom g);
  } as F.


(** Constructs the "identity functor" at [C]. *)
Definition mkFunIdent@{i o} C : Fun@{i o} C C :=
  {|
    fOb x := x;
    fHom _ _ f := f;
    fident_prop _ := eq_refl;
    fcomp_prop _ _ _ _ _ := eq_refl;
  |}.

(** Constructs the "functor composition" [F] then [G]. *)
Program Definition mkFunComp@{i o} A B C :
    forall (F : Fun A B) (G : Fun B C), Fun@{i o} A C :=
  fun F G => {|
    fOb x := fOb G (fOb F x);
    fHom _ _ f := fHom G (fHom F f);
  |}.
Next Obligation.  (* fident_prop *)
  rewrite 2 fident_prop. reflexivity.
Defined.
Next Obligation.  (* fcomp_prop *)
  rewrite 2 fcomp_prop. reflexivity.
Defined.


(** Constructs the "category Cat" of cats and functors. *)
Program Definition mkCatCat@{i n o} : Cat@{n o} :=
  {|
    Ob := Cat@{i n};
    Hom B C := Fun@{i n} B C;
    ident C := mkFunIdent C;
    comp _ _ _ F G := mkFunComp F G;
  |}.
Next Obligation.  (* comp_unitL *)
  rename x into B, y into C, f into F.
  unfold mkFunComp; cbn.
  unfold mkFunComp_obligation_1;
  unfold mkFunComp_obligation_2; cbn.
  destruct F; cbn.

  (* These are immediate by eta-expansion *)
  change (fOb0) with (fun x => fOb0 x) at 30.
  change (fHom0) with (fun x y f => fHom0 x y f) at 10.

  (* But what then? *)

(Please don’t mind too much my use of universes: I am still finding my way. But if you have any suggestions to improve on that or other, you are indeed welcome.)

2

The “classical” proof in 1-category theory relies (at least implicitly) on function extensionality and uniqueness of identity proofs: first show an extensionality lemma for functors, stating that two functors F,G with same domain and codomains are equal whenever 1) for any object x in the domain F x = G x and 2) for any morphism f : x -> y in the domain, F f = G f as morphisms of the codomain.

1 Like
3

No need for UIP for Julio’s proof, just funext. With

Axiom funext : forall {A B} {f g : forall x:A, B x} (e:forall x, f x = g x), f = g.

the proof can be finished with

  f_equal.
  - apply funext. intros.
    destruct (fident_prop0 _).
    reflexivity.
  - repeat (apply funext;intros).
    destruct (fcomp_prop0 _ _ _ _ _).
    reflexivity.
Qed.
2 Likes
4

Thank you, that will be very helpful down the line…

Thank you: with your help, I have managed to complete the definition, but I don’t know what is happening with those destruct. Indeed, I can replace some with rewrite, which I can understand (those hypotheses specialize to proofs of equality, at least “morally”: I cannot use specialize directly [actually, those hypotheses return proofs of equality]), but not all of them, see my code below.

Could you please explain what destruct is doing there?

(** Type-theoretic "functional extensionality". *)
Axiom funext@{o} :
  forall (A : Type@{o}) (B : A -> Type@{o}),
    forall (f g : forall x : A, B x),
      (forall x, f x = g x) -> f = g.

(** Constructs the "category Cat" of cats and functors. *)
Program Definition mkCatCat@{i n o} : Cat@{n o} :=
  {|
    Ob := Cat@{i n};
    Hom B C := Fun@{i n} B C;
    ident C := mkFunIdent C;
    comp _ _ _ F G := mkFunComp F G;
  |}.
Next Obligation.  (* comp_unitL *)
  rename x into B, y into C, f into F.
  unfold mkFunComp;
  unfold mkFunComp_obligation_1;
  unfold mkFunComp_obligation_2; cbn.
  destruct F; cbn.
  f_equal.
  - apply funext; intro.
    rewrite fident_prop0.
    reflexivity.
  - repeat (apply funext; intro).
    rewrite fcomp_prop0.
    reflexivity.
Defined.
Next Obligation.  (* comp_unitR *)
  rename x into B, y into C, f into F.
  unfold mkFunComp;
  unfold mkFunComp_obligation_1;
  unfold mkFunComp_obligation_2; cbn.
  destruct F; cbn.
  f_equal.
  - apply funext; intro.
    rewrite fident_prop0.
    reflexivity.
  - repeat (apply funext; intro).
    rewrite fcomp_prop0.
    reflexivity.
Defined.
Next Obligation.  (* comp_assoc *)
  rename w into A, x into B, y into C, z into D;
  rename f into F, g into G, h into H.
  unfold mkFunComp;
  unfold mkFunComp_obligation_1;
  unfold mkFunComp_obligation_2; cbn.
  destruct F, G, H; cbn.
  f_equal.
  - apply funext; intro.
    destruct fident_prop2.
    destruct fident_prop1.
    rewrite fident_prop0.
    reflexivity.
  - repeat (apply funext; intro).
    destruct fcomp_prop2.
    destruct fcomp_prop1.
    rewrite fcomp_prop0.
    reflexivity.
Defined.
5

If you have arbitrary terms (not necessarily hypotheses) v1 v2 and e : v1 = v2, destruct e will try to change the goal to (fun y (H:v1 = y) => ...) v2 e (with v2 and e not appearing in …) ie abstract over v2 and e, then replace the goal with (fun y (H:v1=y) => ...) v1 eq_refl then beta normalize.

So for instance if the goal is f v2, it changes to (fun y _ => f y) v2 e, is replaced by (fun y _ => f y) v1 eq_refl, then is beta normalized to f v1, so destruct e is like rewrite <-e.

When e appears in the goal or when I will use the proof (ie non Qed proof) I prefer to use destruct because I’m thinking of equality as an inductive type rather than it terms of rewrite, but rewrite can handle it too (at least for your code the destructs on equalities can be replaced be rewrite <-).

There may be differences in how destruct and rewrite do unification. Also if v2 (and e) appear in other hypotheses you may need to revert them before using rewrite, but destruct will auto revert and reintroduce. And if e or v2 are an hypothesese destruct will clear them.

1 Like
6

Also why do I get syntax highlighting on my code blocks but I don’t see any on yours?

Definition foo := 0. (* comment *)

(I used ``` not ```coq so it’s not because you omitted the language)

7

Ah, thanks very much, that explains: now I see what’s happening in my proof :), in fact I can start envisioning a pattern to these proofs, combined with @kyod’s suggestion.

why do I get syntax highlighting on my code blocks but I don’t see any on yours?

I have fixed the posts by adding the language tag. No clue why, but I had seen that before, and I have/had a vague hunch it might have to do with the length of the code block(s).

8

I think your explanation is helpful because understanding that this requires abstraction helps to understand these sophisticated dependent typing errors that say “Error, if I abstract this term, this expression is no longer well-typed.”

But I also think it’s important to mention that destruct also does pattern matching on the goal. In each branch of a pattern match, we get to use the arguments of the associated constructor, and the goal type becomes specialized based on the indices of the constructor. So, for example,

Goal forall (A : Type)(x y:A ), x = y -> y = x.
Proof.
  intros A x y p.
  destruct p.
  Show Proof.
  (* (fun (A : Type) (x y : A) (p : x = y) =>
 match p in (_ = a) return (a = x) with
 | eq_refl => ?Goal
 end) *)

Dependent pattern matching is pretty complicated but there are some resources. I learned from
the MoreDep chapter in Adam Chlipala’s “Certified Programming with Dependent Types” book.

I have written my own tutorial here to explain in my own words, the first one works with the more familiar inductive type of natural numbers and the second treats equality.

1 Like
9

Dependent pattern matching is pretty complicated but there are some resources.

(I find it easy “on paper”, the “magic” of specifying a return type for the match, but being competent at it is another matter, where that magic starts and where it ends exactly. Anyway, the whole chapter of what to learn and how to learn it is indeed crucial, including what should or should not be in a “refman”, to the point that I’d propose we leave it to separate and dedicated discussion(s).)

Meanwhile, after also reading your explanation, I am thinking: “destruct → case analysis → pattern matching”, of course! In fact, (roughly speaking) with rewrite we get an eq_ind which unfolds to just the same match! So great, that’s what we are doing… except, is it?

Indeed, on the other hand, I understand Gaëtan’s explanation of the detail of what destruct is doing in my proof as an application of “eta” then “beta” rules; to the goal: i.e. even the direction seems different, backward as opposed to forward reasoning.

Could you or Gaëtan please combine/reconcile the two pictures?

10

Turning the goal into (fun y (H:v1 = y) => F) v2 e (I guess what you call eta, but it’s actually a backward beta) is because fun y H => F is then used as the return of the pattern matching (ie match e as H in _ = y return F with eq_refl => ?newgoal end).
After doing the pattern matching we beta normalize to get the goal to look like the user expects.

1 Like
11

And here are some checks that give me confidence (is it misplaced?) about the faithfulness of the formalization, at least as far as a theory of “elementary 1-categories” goes (and I hope it is going to be straightforward to extend this to 2-categories, then I’d think we are essentially done as for an elementary theory [**], as for extent: of course, within it, there are many more things to construct, up to a notion of universality, or whatever categories are essentially about: I am still digging…).

(** The category Cat is an object of itself
    (so to speak, i.e. modulo stratification). *)
Check mkCatCat : Ob mkCatCat.

(** Every category is an object of the category Cat. *)
Check fun (C : Cat) => C : Ob mkCatCat.

(** Every functor is a morphism in the category Cat. *)
Check fun B C (F : Fun B C) => F : Hom mkCatCat B C.

(** Not every type is an object of the category Cat. *)
Fail Check fun (C : Type) => C : Ob mkCatCat.

BTW, the issue of equality I am not seeing as an issue, not as for an elementary theory (in particular, not internal nor enriched), as long as mathematically what we are really interested in when we say “up to equivalence/isomorphism” is the ability to “substitute equivalents for equivalents” (right?), emphasis on substitution-ability, which in this setting (Rocq’s) is in fact directly expressed by definitional equality as convertibility of terms… [*]

Special categories coming with a specific notion of “equivalence” then just need a law that “transports” that equivalence to equality. [I suppose another way to say that is that it works out of the box if assuming Univalence.]

Which possibly opens the door to inconsistencies in plain Rocq (I am not sure about the details), but could be used with “strict discipline”, i.e. keeping the obtained equalities internal to the categoric discourse: which in turn could be helped by encapsulating things into a DSL…

(I am still a rookie, I might be misspeaking at various places: I hope the picture/idea is clear enough. Keeping in mind the present topic is primarily about “mathematics in Rocq”, formalization(s) of category theory in particular, any feedback on the ideas and reasons given above is very welcome.)

[*] P.S. To be fully explicit about equality, the next step could be considering a formulation in terms not of hom-objects but of one type of morphisms plus the two projections “dom” and “cod”: then, looking back at composition of hom-objects, it becomes evident that already when above we are matching objects, we are relying on unification-by-convertibility as baked in…

[**] P.P.S. There is in fact (at least) one thing that my formalization does not capture: akin to in a theory of sets everything is a set, in a theory of categories everything must be a category, while my Ob and Hom are in Type. But I still can’t figure out what that concretely looks like…