proposition: Lemma path_def_isomorphic_id_transport_dom (p : A = B) : def_isomorphic (isomorphic_id p) = transport (λ C, ∀ s, C s → B s) (ap carriers p)^ (hom_id B).
proof: Proof. by path_induction. Defined.
imports: HoTT.Classes.theory.ua_homomorphism HoTT.Types HoTT.Tactics