{A} (x : A) (K : axiomK A) : K x (idpath x) = idpath (idpath x). Proof. pose (T1A := @istrunc_succ _ A (@hset_axiomK A K)). exact (@hset_path2 (x=x) (T1A x x) _ _ _ _). Defined.
Require Import Basics. Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.