proposition: Lemma sip_helper 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: Proof. split. - intros; path_induction; split; apply reflexivity. - intros [H0 H1]; path_induction; simpl in *. apply antisymmetry_structure; assumption. Defined.
imports: Category.Core Category.Univalent Category.Morphisms Structure.Core Types.Sigma Trunc Equivalences Basics.Tactics