proposition: Lemma axiomK_idpath {A} (x : A) (K : axiomK A) : K x (idpath x) = idpath (idpath x).
proof: Proof. pose (T1A := @istrunc_succ _ A (@hset_axiomK A K)). exact (@hset_path2 (x=x) (T1A x x) _ _ _ _). Defined.
imports: Basics Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow