forall `{Choice}, Choice_type.
From HoTT Require Import ExcludedMiddle canonical_names. From HoTT Require Import HIT.unique_choice. From HoTT Require Import Spaces.Card. From HoTT.Sets Require Import Ordinals.