proposition: Theorem TorsorIso_rect {G:gr} {X Y : Torsor G} (P : ActionIso X Y -> UU) : (∏ e : X = Y, P (torsor_univalence e)) -> ∏ f, P f.
proof: Proof. intros ih ?. set (p := ih (invmap torsor_univalence f)). set (h := homotweqinvweq torsor_univalence f). exact (transportf P h p). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Combinatorics.OrderedSets