fact: Definition inO_retract_inO (A B : Type) `{In O B} (s : A -> B) (r : B -> A) (K : r o s == idmap) : In O A.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout