proposition: Lemma univalence_func_natural_equiv `{Univalence} : forall (C : Type -> Type) (all_contr : forall A, Contr (C A -> C A)) (g : forall A, C A -> A) {A : Type} (e : A <~> A), e o (g A) = (g A).
proof: Proof. intros C all_contr g A e. apply path_forall. intros x. pose (p := path_universe_uncurried e). refine (concat (happly (transport_idmap_path_universe_uncurried e)^ (g A x)) _). refine (concat (ap _ (ap _ (happly (@path_contr _ (all_contr A) idmap (transport _ p^)) x))) _). refine (concat (@transport_arrow _ (fun A => C A) idmap _ _ p (g A) x)^ _). exact (happly (apD g p) x). 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)