Definition Action_univalence_prelim_comp {G:gr} {X Y:Action G} (p:X = Y) : Action_univalence_prelim p = path_to_ActionIso p. Proof. intros. destruct p. apply (maponpaths (tpair _ _)). apply funextsec; intro g. apply funextsec; intro x. apply setproperty. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets. Import UniMath.MoreFoundations.PartA.