proposition: Lemma global_element_fixpoint_inverse : is_inverse_in_precat (C := HSET) (a := global_element) (b := fixpoint_set) global_element_to_fixpoint fixpoint_to_global_element.
proof: Proof. split. - apply funextfun. intro f. use monoid_action_morphism_eq. intro t. now induction t. - apply funextfun. intro a. refine (subtypePath _ _). { intro. apply impred_isaprop. intro. apply setproperty. } apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total