x y (p : x = y) (a : P x) (b : P y) : transport P p a = b <-> is_structure_homomorphism P _ _ (idtoiso X p) a b * is_structure_homomorphism P _ _ (idtoiso X p)^-1 b a. Proof. split. - intros; path_induction; split; apply reflexivity. - intros [H0 H1]; path_induction; simpl in *. apply antisymmetry_structure; assumption. Defined.
Require Import Category.Core Category.Univalent Category.Morphisms. Require Import Structure.Core. Require Import Types.Sigma Trunc Equivalences. Require Import Basics.Iff Basics.Tactics.