{A} `{axiomK A} : IsHSet A. Proof. apply istrunc_S; intros x y. apply @hprop_allpath. intros p q. by induction p. Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.