`{Univalence} (BCf : { B : Type_ O1 & { C : Type_ O2 & C -> O2 B }}) : fracture_unglue (fracture_glue_uncurried BCf) = BCf. Proof. destruct BCf as [B [C f]]. assert (IsEquiv (O_rec ((to O2 B)^*' f))). { apply isequiv_O_rec_O_inverts. apply O_inverts_conn_map, conn_map_pullback'. intros ob; apply isconnectedo1_ino2. rapply mapinO_between_inO. } assert (IsEquiv (O_rec (f^* (to O2 B)))). { apply isequiv_O_rec_O_inverts. apply O_inverts_conn_map, conn_map_pullback; exact _. } simple refine (path_sigma' _ _ _). { apply path_TypeO; unfold ".1", ".2". refine (path_universe (O_rec ((to O2 B)^*' f))). } refine (transport_sigma' _ _ @ _); unfold ".1", ".2". simple refine (path_sigma' _ _ _). { apply path_TypeO; unfold ".1", ".2". refine (path_universe (O_rec (f^* (to O2 B)))). } apply path_arrow; intros c. refine (transport_arrow_toconst _ _ _ @ _). refine (transport_arrow_fromconst (C := fun X:Type_ O1 => O2 X) _ _ _ @ _). refine (transport_compose O2 (TypeO_pr1 O1) _ _ @ _). refine (transport_compose idmap O2 _ _ @ _). transitivity (transport idmap (ap O2 (path_universe (O_rec ((to O2 B)^*' f)))) (O_functor O2 (to O1 (Pullback f (to O2 B))) ((O_rec (f^* (to O2 B)))^-1 c))); [ apply ap11; repeat apply ap | transitivity (O_functor O2 (O_rec ((to O2 B)^*' f)) (O_functor O2 (to O1 (Pullback f (to O2 B))) ((O_rec (f^* (to O2 B)))^-1 c))) ]. + refine (pr1_path_sigma_uncurried _ @ eisretr pr1 _). + refine (transport_compose idmap (TypeO_pr1 O2) (path_TypeO O2 (O2 (Pullback f (to O2 B)); _) C _)^ c @ _). refine (ap (fun p => transport idmap p c) (ap_V _ _) @ _). refine (ap (fun p => transport idmap p^ c) (pr1_path_sigma_uncurried _ @ eisretr pr1 _) @ _). refine (transport_path_universe_V _ _). + refine (ap (fun p => transport idmap p _) (ap_O_path_universe O2 _) @ _). refine (transport_path_universe _ _). + refine ((O_functor_compose O2 _ _ _)^ @ _). refine (O_functor_homotopy O2 _ _ (O_rec_beta _) _ @ _). revert c; equiv_intro (O_rec (f^* (to O2 B))) x. refine (ap _ (eissect _ _) @ _). revert x; apply O_indpaths; intros x. refine (to_O_natural O2 _ x @ _). refine (_ @ ap f (O_rec_beta _ _)^). destruct x as [a [b q]]; exact (q^). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.