Reflexive leq_card. Proof. intro x. strip_truncations. apply tr. exists idmap. refine (fun _ _ => idmap). Defined.
Require Import HoTT.Universes.TruncType. Require Import HoTT.Classes.interfaces.abstract_algebra.