UniMath Category theory basics · Coq users

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)...

Ali Caglayan (Mar 13 2023 at 13:55):

Benedikt Ahrens (Mar 13 2023 at 14:02):

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

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)

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.

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).

Benedikt Ahrens (Mar 13 2023 at 14:17):

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...

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?

Stream: Coq users

Topic: UniMath Category theory basics