`{Univalence} : Card -> Card -> HProp. Proof. refine (Trunc_rec (fun a => _)). refine (Trunc_rec (fun b => _)). exact (hexists (fun (i : a -> b) => IsInjective i)). Defined.
Require Import HoTT.Universes.TruncType. Require Import HoTT.Classes.interfaces.abstract_algebra.