Stream: Coq users

Topic: UniMath Category theory basics


view this post on Zulip Dennis H (Mar 13 2023 at 13:23):

I'm currently looking into the category theory module in UniMath, but I am running into some problems. I'm trying to follow the tutorial in the UniMath school (found here), but even the solution wont be correctly interpreted. Basically, I am looking at this

  Definition nat_category_ob_mor : precategory_ob_mor.
  Proof.
    use make_precategory_ob_mor.
    - exact nat.
    - intros m n.
      (* Rather than functions {1,…,m}->{1,…,n} we consider functions {0,…,m-1}->{0,…,n-1},
         so that we can use stnset from the Combinatorics package. *)
      exact (stnset m  stnset n).
  Defined.

  Definition nat_category_data : precategory_data.
  Proof.
    unfold precategory_data.
    exists nat_category_ob_mor.
    split.
    - intro n.
      exact (idfun (stnset n)).
    - intros k l m f g.
      exact  n, g(f n)).
  Defined.

but when stepping through the proof, I am asked to prove nat_category_ob_mor ⟦ n, n ⟧ after intro n in the second proof. Tracing back the definition, this should boil down to finding (stnset n) -> (stnset n), which indeed should be idfun (stnset n). However, on this line, coqtop tells me that n has type ob nat_category_ob_mor, which as far as I can tell is just the Record field ob, which should be nat, as defined in the proof above. Doing unfold ob in n does indeed give me pr1 nat_category_ob_mor (which should also just be nat), but I can't unfold pr1 in n (it just does nothing). I am not very familiar with Record types, but can someone explain how I could fix this?

Also, the second point asks me to prove something of the form precategory_morphisms nat_category_ob_mor, or pr2 nat_category_ob_mor, but again here, I cannot seem to unfold pr2 to turn my goal into stnset(k) -> stnset(l)...

view this post on Zulip Ali Caglayan (Mar 13 2023 at 13:55):

cc @Benedikt Ahrens

view this post on Zulip Benedikt Ahrens (Mar 13 2023 at 14:02):

Hi @Dennis H , could you post your complete file, with all the Require statements?

view this post on Zulip Dennis H (Mar 13 2023 at 14:05):

unimath6.v @Benedikt Ahrens it should basically just be the solutions file in the Schools repo (Cortona 2022)

view this post on Zulip Benedikt Ahrens (Mar 13 2023 at 14:15):

@Dennis H : You need to finish the definition of nat_category_ob_mor with Defined., not Qed.. The latter makes the definition opaque, preventing any unfolding from happening.

So, do

Definition nat_category_ob_mor : precategory_ob_mor.
  Proof.
    use make_precategory_ob_mor.
    - exact nat.
    - intros m n.
      exact (stnset m -> stnset n).
  Defined.

Please let me know if that does not solve the problem (or gives rise to another problem).

view this post on Zulip Benedikt Ahrens (Mar 13 2023 at 14:17):

Thanks @Ali Caglayan for cc'ing me.

view this post on Zulip Dennis H (Mar 13 2023 at 14:31):

I see, that works, thanks! Still, kind of unrelatedly, is it possible to unfold the definition of the record field pr2 and pr1 as well? The proof works like this, but I may find it easier in the future to be able to do this...

view this post on Zulip Benedikt Ahrens (Mar 13 2023 at 15:03):

If you use simpl in n., then n : nat_category_ob_mor will be simplified to n : nat. In the goal, it works similarly. Is that what you are trying to achieve?


Last updated: Jun 16 2024 at 02:41 UTC