proposition: Theorem univalence_isequiv_postcompose `{H0 : IsEquiv A B w} C : IsEquiv (fun (g:C->A) => w o g).
proof: Proof. unfold Univalence_type in *. refine (isequiv_adjointify (fun (g:C->A) => w o g) (fun (g:C->B) => w^-1 o g) _ _); intro; pose (Build_Equiv _ _ w _) as w'; change H0 with (@equiv_isequiv _ _ w'); change w with (@equiv_fun _ _ w'); clearbody w'; clear H0 w; rewrite <- (@eisretr _ _ (@equiv_path A B) (ua A B) w'); generalize ((@equiv_inv _ _ (equiv_path A B) (ua A B)) w'); intro p; clear w'; destruct p; reflexivity. Defined.
imports: HoTT.Basics Types.Universe Metatheory.Core Metatheory.FunextVarieties