Necessary truncations on formalizing cardinal arithmetic

[ElifUskuplu]

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:

add-card :
  {l1 l2 : Level} → cardinal l1 → cardinal l2 → cardinal (l1 ⊔ l2)
add-card {l1} {l2} =
  map-universal-property-trunc-Set
    ( hom-Set (cardinal-Set l2) (cardinal-Set (l1 ⊔ l2)))
    ( λ A →
      ( map-universal-property-trunc-Set
        ( cardinal-Set (l1 ⊔ l2))
        ( λ B → cardinality (coprod-Set A B))))

I defined zero cardinal as:

zero-card : cardinal lzero
zero-card = unit-trunc-Set empty-Set

One of the obvious results would be

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