(@isomorphic_id σ A B) o id_isomorphic == idmap. 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.
Require Import Import isomorphic_notations.