(A : Type) := { OA : Type & { Ou : A -> OA & ((In O OA) * (O_inverts Ou)) }}. Global Instance contr_typeof_O_unit `{Univalence} (A : Type) : Contr ( A). Proof. apply (Build_Contr _ (O A ; (to O A ; (_ , _)))). intros [OA [Ou [? ?]]]. pose (f := O_rec Ou : O A -> OA). pose (g := (O_functor Ou)^-1 o to O OA : (OA -> O A)). assert (IsEquiv f). { refine (isequiv_adjointify f g _ _). - apply O_functor_faithful_inO; intros x. rewrite O_functor_idmap. rewrite O_functor_compose. unfold g. rewrite (O_functor_compose (to O OA) (O_functor Ou)^-1). rewrite O_functor_wellpointed. rewrite (to_O_natural (O_functor Ou)^-1 x). refine (to_O_natural f _ @ _). set (y := (O_functor Ou)^-1 x). transitivity (O_functor Ou y); [ | apply eisretr]. unfold f, O_functor. apply O_rec_postcompose. - refine (O_indpaths _ _ _); intros x. unfold f. rewrite O_rec_beta. unfold g. apply moveR_equiv_V. symmetry; apply to_O_natural. } simple refine (path_sigma _ _ _ _ _); cbn. - exact (path_universe f). - rewrite transport_sigma. simple refine (path_sigma _ _ _ _ _); cbn; [ | apply path_ishprop]. apply path_arrow; intros x. rewrite transport_arrow_fromconst. rewrite transport_path_universe. unfold f; apply O_rec_beta. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.