Conversation
| - exact is_precategory_malg. | ||
| Defined. | ||
|
|
||
| Definition malg_cat : category. |
There was a problem hiding this comment.
To define/construct this category, you have that your objects are functors with structure and your morphisms are natural transformations with structure/properties.
In particular, you've used the composition of natural transformations, the identity natural transformations, etc.
In essence, you've used here that functors and natural transformations form a category (a functor category).
Functor categories are defined in "CategoryTheory/FunctorCategory.v"
If you want to be more optimal, you can define malg_cat as a displayed category over functor_category(C,C). Or more precisely, you can define malg_cat as the total category of that displayed category.
(An analogous trick has been used CategoryTheory/Monoidal/FunctorCategories.v)
There was a problem hiding this comment.
Thanks for the tips once again, I applied the changes, it really made the code more concise and easy to follow.
| - exact is_precategory_pos_fib. | ||
| Defined. | ||
|
|
||
| Definition pos_fib_cat : category. |
There was a problem hiding this comment.
The comment made for malg (regarding displayed categories over functor categories) applies here as well.
| ∏ x : C, C ⟦ x, Ω ⟧ → α x = α x). | ||
| Proof. | ||
| apply isapropdirprod. | ||
| + unfold disp_nat_trans. unfold disp_nat_trans_data. apply isofhleveltotal2. |
There was a problem hiding this comment.
Here, you've started subgoals with a +, as you've done everywhere else, try to start with a -.
The general hierarchy is: -,+,*,--,++, etc.
|
Some smaller general comments:
|
This PR is created just for visibility, it is not yet complete.
This PR contains the following definitions:
(a) Category of Monotone F-algebras
(b) Category of fibered fucntors fixed for the domain fibration.
They are part of https://doi.org/10.1016/j.entcs.2020.09.002 and will be used to prove an isomorphism between the two. Before the PR is finished, definitions related to monadic liftings and their relation to weakest preconditions will be implemented.