fact: Definition qinv_id A : qinv A A := (fun x => x; (fun x => x ; (fun x => 1, fun x => 1))).
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)