(X : Type) `{IsEquiv _ _ (to_plus X)} : In Meet X. Proof. split. - apply (inO_equiv_inO (Plus X) (to_plus X)^-1). - srapply inO_to_O_retract. + exact ((to_plus X)^-1 o (to L (O X))). + intros x; apply (eissect (to_plus X)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.