inO_paths@{i} (S : Type@{i}) {S_inO : In O S} (x y : S) : In O (x=y). Proof. simple refine (inO_to_O_retract@{i} _ _ _); intro u. - assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). { refine (O_indpaths _ _ _); simpl. intro v; exact v. } exact (p u). - simpl. rewrite O_indpaths_beta; reflexivity. 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.