proposition: Lemma TRRGhomo_frompath (X Y : hSet) (G : TRRGraphData X) (H : TRRGraphData Y) (p : X = Y) : transportf (λ x : hSet, TRRGraphData x) p G = H → @isTRRGhomo (X ,, G) (Y ,, H) (pr1weq (hSet_univalence _ _ p)).
proof: Proof. simpl. induction p. simpl. unfold isTRRGhomo. intros q. split. - intros x y. rewrite -> idpath_transportf in q. split. rewrite -> q. intros P ; apply P. rewrite -> q. intros P ; apply P. - rewrite -> idpath_transportf in q. induction q. reflexivity. Qed.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions