proposition: Theorem qinv_univalence_isequiv_postcompose {A B : Type} {w : A -> B} `{H0 : IsEquiv A B w} C : IsEquiv (fun (g:C->A) => w o g).
proof: Proof. unfold QInv_Univalence_type in *. pose (w' := qinv_isequiv w). refine (isequiv_adjointify (fun (g:C->A) => w o g) (fun (g:C->B) => w^-1 o g) _ _); intros g; first [ change ((fun x => w'.1 ( w'.2.1 (g x))) = g) | change ((fun x => w'.2.1 ( w'.1 (g x))) = g) ]; clearbody w'; clear H0 w; rewrite <- (@eisretr _ _ (@qinv_path A B) (isequiv_qinv (qua A B)) w'); generalize ((@equiv_inv _ _ (qinv_path A B) (isequiv_qinv (qua A B))) w'); intro p; clear w'; destruct p; reflexivity. Defined.
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)