proposition: Lemma sect_id_isomorphic : (@isomorphic_id σ A B) o id_isomorphic == idmap.
proof: Proof. intro F. apply path_hset_isomorphic. rewrite path_def_isomorphic_id_transport_cod. funext s x. rewrite !transport_forall_constant. rewrite path_ap_carriers_path_algebra. transport_path_forall_hammer. apply transport_path_universe. Qed.
imports: HoTT.Classes.theory.ua_homomorphism HoTT.Types HoTT.Tactics