Transitive leq_card. Proof. intros a b c. strip_truncations. intros Hab Hbc. strip_truncations. destruct Hab as [iab Hab]. destruct Hbc as [ibc Hbc]. apply tr. exists (ibc ∘ iab). intros x y Hxy. apply Hab. apply Hbc. apply Hxy. Defined.
Require Import HoTT.Universes.TruncType. Require Import HoTT.Classes.interfaces.abstract_algebra.