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