proposition: Lemma sect_isomorphic_id : id_isomorphic o (@isomorphic_id σ A B) == idmap.
proof: Proof. intro p. destruct p. apply path_path_isomorphism_hom_id_hset. exact _. Qed.
imports: HoTT.Classes.theory.ua_homomorphism HoTT.Types HoTT.Tactics