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

...

cc @Benedikt Ahrens

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

statements?

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

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

Thanks @Ali Caglayan for cc'ing me.

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

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