You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi, I would like to finish my initial goal about cardinalities in Set Theory directory. It means the completion of Section 10.2 of HoTT book. I just need to remember necessary truncation rules and universal properties in the library. For example, I defined the addition as:
right-unit-law-add-card :
{l : Level} → (A : cardinal l) → add-card A zero-card = A
I think I can use the fact
right-unit-law-coprod : (A + empty) ≃ A
But I'm not sure which universal property rule is suitable to obtain this. If I solve this issue, I believe I can handle the rest. Any suggestion would be great <3
The text was updated successfully, but these errors were encountered:
Hi, I would like to finish my initial goal about cardinalities in Set Theory directory. It means the completion of Section 10.2 of HoTT book. I just need to remember necessary truncation rules and universal properties in the library. For example, I defined the addition as:
I defined zero cardinal as:
One of the obvious results would be
I think I can use the fact
But I'm not sure which universal property rule is suitable to obtain this. If I solve this issue, I believe I can handle the rest. Any suggestion would be great <3
The text was updated successfully, but these errors were encountered: