search

UniMath / Schools

77 stars 21 forks source link

Exercises on category theory #22

Closed nmvdw closed 5 years ago

nmvdw commented 5 years ago

I modified exercise 2, and I also gave the solution for this one.

benediktahrens commented 5 years ago

@nmvdw :

make[2]: Entering directory `/home/travis/build/UniMath/Schools/2019-04-Birmingham/Part6_Category_Theory'
COQC category_theory_exercises.v
File "./category_theory_exercises.v", line 92, characters 8-24:
Error: The reference dirprod_disp_cat was not found in the current
environment.
benediktahrens commented 5 years ago

@nmvdw: 

COQC category_theory_exercises.v
File "./category_theory_exercises.v", line 112, characters 7-13:
Error:
In environment
X : pointed_operation_set
The term "pr12 X" has type "pointed_disp_cat (pr1 X)"
while it is expected to have type "pr1hSet (carrier X)".
benediktahrens commented 5 years ago

Great, thanks a lot!