Definition Action_univalence_prelim {G:gr} {X Y:Action G} : (X = Y) ≃ (ActionIso X Y). Proof. intros. simple refine (weqcomp (total2_paths_equiv (ActionStructure G) X Y) _). simple refine (weqbandf _ _ _ _). { apply hSet_univalence. } simpl. intro p. simple refine (weqcomp (is_equivariant_identity p) _). exact (eqweqmap (maponpaths (λ f, hProptoType (is_equivariant f)) (pr1_eqweqmap (maponpaths pr1hSet p)))). 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.