(A : Type) `{Decidable (O A)} : O (Decidable A). Proof. destruct (dec (O A)) as [y|n]. - exact (O_functor inl y). - refine (O_functor inr _). apply to; intros a. exact (n (to O A a)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.