Ralph Matthes
Ralph Matthes
currently builds on PR #1532 dialgebras of monoidal functors F and G (F strong and G lax) can be turned into a monoidal category (by way of a displayed monoidal...
(final section of paper with Benedikt and Anders) The basic situation is now developed in CommaCategories.v, with the equation being a special case of the one for comma categories -...
This was discussed for PR #1516. See in particular [its conclusion](https://github.com/UniMath/UniMath/pull/1516#discussion_r898908818). This issue ought to be resolved before generalizing whiskered monoidal categories to actions (in whiskered style).
There was a partial migration within the move from iso to z_iso (PR #1507). `is_disp_functor_cat_z_iso_iff_pointwise_z_iso` is the analogue of the former `is_disp_functor_cat_iso_iff_pointwise_iso`. Before finally commenting out this part, it depended...
One can add `-f build/CoqMakefile.make` to the command line for making a single .vo file given by its path. Otherwise, if the .vo file is not present, make will not...
The issue is how to find the right value for N in make -jN when compiling the UniMath library (and maybe to choose an appropriate computer for bearable compilation time)....
this comes from the use of (binary) product categories; most of the time, the projections of a pair do not want to reduce to the components This is not a...
CAT = the bicategory of categories This means, without taking univalent categories (UCAT) but just precategories with homsets. The new files are simple adaptations of the respective files without "WithoutUnivalence"...
only first steps to fix definitions and to detect shortcomings of the UniMath library
tries to build on the code that was there for technical purposes of proof management only the code is unduly scattered for the moment the bicategorical scenario will be compared...