(A : Type) : (U -> Contr A) <-> IsEquiv (fun a:A => push (inr a) : Join U A). Proof. split. - intros uac. simple refine (isequiv_adjointify _ _ _ _). * simple refine (Pushout_rec A _ _ _). + intros u; pose (uac u); exact (center A). + intros a; assumption. + intros [u a]. simpl. pose (uac u). apply contr. * intros z. pattern z. simple refine (Pushout_ind _ _ _ _ z). + intros u. pose (contr_inhabited_hprop U u). apply path_contr. + intros a; reflexivity. + intros [u a]; pose (contr_inhabited_hprop U u). apply path_contr. * intros a. reflexivity. - intros ? u. refine (contr_equiv (Join U A) (fun a:A => push (inr a))^-1). pose (contr_inhabited_hprop U u). exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible Nullification Lex Topological. Require Import Colimits.Pushout Homotopy.Join.Core.