## Stream: Coq users

### Topic: UniMath Category theory basics

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

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

cc @Benedikt Ahrens

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

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

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

Thanks @Ali Caglayan for cc'ing me.

#### 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?

Last updated: Oct 04 2023 at 23:01 UTC